Skip to content

perf: Field.toEuclideanDomain fast_instance%#39293

Open
kbuzzard wants to merge 2 commits into
leanprover-community:masterfrom
kbuzzard:kbuzzard-euclideandomain-fastinstance
Open

perf: Field.toEuclideanDomain fast_instance%#39293
kbuzzard wants to merge 2 commits into
leanprover-community:masterfrom
kbuzzard:kbuzzard-euclideandomain-fastinstance

Conversation

@kbuzzard
Copy link
Copy Markdown
Member


Open in Gitpod

Just an experiment. Pulled this fast_instance% off #38087 to see if it makes a difference. Will then try it after #39263 to see if it still makes a difference.

@kbuzzard kbuzzard added the WIP Work in progress label May 13, 2026
@kbuzzard
Copy link
Copy Markdown
Member Author

!radar

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented May 13, 2026

Benchmark results for 0d7dd61 against bcb9e00 are in. No significant results found. @kbuzzard

  • build//instructions: -56.8G (-0.03%)

Small changes (6✅)

  • build/module/Mathlib.Algebra.Lie.Weights.Killing//instructions: -1.4G (-1.17%)
  • build/module/Mathlib.Algebra.Lie.Weights.RootSystem//instructions: -1.5G (-1.54%)
  • build/module/Mathlib.FieldTheory.Galois.NormalBasis//instructions: -473.2M (-1.77%)
  • build/module/Mathlib.FieldTheory.LinearDisjoint//instructions: -2.3G (-1.47%)
  • build/module/Mathlib.RingTheory.LaurentSeries//instructions: -4.7G (-1.87%)
  • build/module/Mathlib.RingTheory.Spectrum.Prime.Homeomorph//instructions: -455.4M (-1.70%)

@github-actions
Copy link
Copy Markdown

github-actions Bot commented May 13, 2026

PR summary 4529a2df72

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Algebra.EuclideanDomain.Field 184 185 +1 (+0.54%)
Import changes for all files
Files Import difference
Mathlib.Algebra.EuclideanDomain.Field 1

Declarations diff

+ instance (priority := 100) toEuclideanDomain : EuclideanDomain K := fast_instance%
- instance (priority := 100) toEuclideanDomain : EuclideanDomain K

You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.


No changes to strong technical debt.
No changes to weak technical debt.

@github-actions github-actions Bot added the t-algebra Algebra (groups, rings, fields, etc) label May 13, 2026
@kbuzzard
Copy link
Copy Markdown
Member Author

Master now has #39263 so let's see if that makes a different (I suspect it will)

!radar

@leanprover-radar
Copy link
Copy Markdown

Benchmarking 4529a2d against ec05634 (preliminary results).

React with 👀 to be notified when the results are in. The command author is always notified.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

t-algebra Algebra (groups, rings, fields, etc) WIP Work in progress

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants