Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: omega to abstract its own proofs #5998

Merged
merged 19 commits into from
Mar 10, 2025
Merged

feat: omega to abstract its own proofs #5998

merged 19 commits into from
Mar 10, 2025

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Nov 7, 2024 •
edited
Loading

This PR lets omega always abstract its own proofs into an auxiliary definition. The size of the olean of Vector.Extract goes down from 20MB to 5MB with this, overall stdlib olean size and build instruction count go down 5%.

Needs #7362.

@nomeata
feat: omega to abstract its own proofs
14cc087 
This PR is an experiment.

Some experiments show that abstracting the proofs produced by omega can
speed up a particularly gnarly proof from 15s to 10s. Not a
game-changer, but still notable.

It seems this breaks the use of `omega` as a simp discharger. Are simp
dischargers not allowed to write auxillary definitions to the
environment?
@nomeata nomeata added the changelog-no Do not include this PR in the release changelog label Nov 7, 2024
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 7, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 7, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5998
e583e72
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 7, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5998
2156fb9
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Nov 7, 2024
@nomeata nomeata closed this Nov 8, 2024
@nomeata nomeata deleted the joachim/omega-abstract-proofs branch November 8, 2024 14:01
@nomeata nomeata restored the joachim/omega-abstract-proofs branch November 8, 2024 14:01
@nomeata nomeata reopened this Mar 4, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 4, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5998
892b200
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 4, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5998
41662bb
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 4, 2025 09:46 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 4, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5998
553cf58
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 4, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5998
1e466d1
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Mar 4, 2025 •
edited
Loading

Mathlib CI status (docs):

  • 💥 Mathlib branch lean-pr-testing-5998 build failed against this PR. (2025-03-04 10:00:14) View Log
  • 💥 Mathlib branch lean-pr-testing-5998 build failed against this PR. (2025-03-04 10:23:41) View Log
  • 💥 Mathlib branch lean-pr-testing-5998 build failed against this PR. (2025-03-04 11:33:34) View Log
  • 💥 Mathlib branch lean-pr-testing-5998 build failed against this PR. (2025-03-04 14:34:41) View Log
  • ✅ Mathlib branch lean-pr-testing-5998 has successfully built against this PR. (2025-03-04 17:29:59) View Log
  • ✅ Mathlib branch lean-pr-testing-5998 has successfully built against this PR. (2025-03-05 15:52:23) View Log
  • ✅ Mathlib branch lean-pr-testing-5998 has successfully built against this PR. (2025-03-06 10:09:23) View Log
  • 💥 Mathlib branch lean-pr-testing-5998 build failed against this PR. (2025-03-06 11:22:14) View Log
  • 💥 Mathlib branch lean-pr-testing-5998 build failed against this PR. (2025-03-06 12:37:03) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 20d191bc8e00c45573274a043e78c33f494daca4 --onto ca0d8226192e7c0cdcc71d6322c3226ad4f73f30. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-06 18:00:51)
    Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 20d191bc8e00c45573274a043e78c33f494daca4 --onto ca0d8226192e7c0cdcc71d6322c3226ad4f73f30. (2025-03-06 18:18:44)
  • 💥 Mathlib branch lean-pr-testing-5998 build failed against this PR. (2025-03-06 18:21:44) View Log
  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-03-07 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-07 13:34:31)
  • ✅ Mathlib branch lean-pr-testing-5998 has successfully built against this PR. (2025-03-10 10:53:36) View Log

@nomeata nomeata added changelog-language Language features, tactics, and metaprograms and removed changelog-no Do not include this PR in the release changelog labels Mar 4, 2025
@nomeata
Copy link
Collaborator Author

nomeata commented Mar 4, 2025

Builds good chunks of mathlib, but then fails with

error: ././././Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean:137:87: (kernel) constant has already been declared '_uniq.75570'

which probably means that somewhere in simp (or a tactic around simp) we are reverting the counter for fresh names, but not the environment.

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 4, 2025 10:50 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 4, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5998
8aae683
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 4, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5998
0b9a46b
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 4, 2025 14:03 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 4, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5998
b1fd050
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 6, 2025 11:40 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 6, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5998
7739897
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 6, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5998
10fb14a
@nomeata nomeata mentioned this pull request Mar 6, 2025
Closed
github-merge-queue bot pushed a commit that referenced this pull request Mar 6, 2025
@nomeata
fix: allow simp dischargers to add aux decls to the environment (#7362)
20d191b 
This PR allows simp dischargers to add aux decls to the environment.
This enables tactics like `native_decide` to be used here, and unblocks
improvements to omega in #5998.

Fixes #7318
@nomeata nomeata marked this pull request as ready for review March 6, 2025 16:54
@nomeata nomeata requested a review from kim-em as a code owner March 6, 2025 16:54
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 6, 2025 17:07 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 6, 2025 17:39 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 6, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5998
5182a46
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 6, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5998
82b60bb
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 7, 2025 13:21 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 10, 2025 09:49 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 10, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5998
ba5c35c
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 10, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5998
98b7b5b
@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Mar 10, 2025
@nomeata
Copy link
Collaborator Author

nomeata commented Mar 10, 2025

Finally the mathlib bench results with zetaDelta := true:
https://speed.lean-lang.org/mathlib4/compare/9148af87-77b2-48cf-8af2-82f0820a77f0/to/e37a9921-5b1f-4434-9a74-06c16feaa8b4

As expected much better, the regressions across the boards are gone. We still have a large regression in Algebra.Homology.DerivedCategory.Ext.ExactSequences. Maybe worth investigating at some point, but I’ll be content with this for now and merge.

File Instructions %
build -116.566⬝10⁹ (-0.06%)
lint -36.313⬝10⁹ (-0.44%)
Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences +174.460⬝10⁹ (+188.46%)
Batteries.Data.Nat.Bisect +3.199⬝10⁹ (+31.07%)
2 files, Instructions +2.0⬝10⁹
File Instructions %
Mathlib.RingTheory.Polynomial.Chebyshev +2.349⬝10⁹ (+1.93%)
Mathlib.Combinatorics.SimpleGraph.Path +2.125⬝10⁹ (+5.04%)
11 files, Instructions -2.0⬝10⁹
File Instructions %
Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence -1.35⬝10⁹ (-2.29%)
Mathlib.RingTheory.WittVector.MulCoeff -1.151⬝10⁹ (-3.64%)
Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit -1.175⬝10⁹ (-1.73%)
Mathlib.AlgebraicTopology.Quasicategory.StrictSegal -1.248⬝10⁹ (-9.22%)
Mathlib.AlgebraicTopology.DoldKan.Faces -1.339⬝10⁹ (-6.57%)
Mathlib.AlgebraicTopology.SimplicialSet.Horn -1.399⬝10⁹ (-6.41%)
Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass -1.436⬝10⁹ (-6.06%)
Mathlib.Data.Finset.Card -1.474⬝10⁹ (-5.79%)
Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction -1.487⬝10⁹ (-1.21%)
Mathlib.Algebra.Homology.HomotopyCategory.Triangulated -1.604⬝10⁹ (-1.24%)
Mathlib.Data.List.Cycle -1.678⬝10⁹ (-5.59%)
5 files, Instructions -3.0⬝10⁹
File Instructions %
Mathlib.Data.List.Triplewise -2.104⬝10⁹ (-24.73%)
Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal -2.311⬝10⁹ (-9.46%)
Mathlib.Algebra.Homology.HomotopyCategory.Shift -2.405⬝10⁹ (-4.33%)
Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated -2.600⬝10⁹ (-1.09%)
Mathlib.Order.RelSeries -2.864⬝10⁹ (-6.46%)
4 files, Instructions -4.0⬝10⁹
File Instructions %
Mathlib.Algebra.Homology.HomotopyCategory.HomComplex -3.121⬝10⁹ (-3.23%)
Mathlib.Algebra.Homology.HomotopyCategory.MappingCone -3.183⬝10⁹ (-3.35%)
Mathlib.Data.Fin.VecNotation -3.921⬝10⁹ (-26.32%)
Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic -3.950⬝10⁹ (-8.02%)
2 files, Instructions -5.0⬝10⁹
File Instructions %
Batteries.Data.BinaryHeap -4.46⬝10⁹ (-32.03%)
Mathlib.Algebra.Homology.ShortComplex.SnakeLemma -4.466⬝10⁹ (-3.99%)
2 files, Instructions -6.0⬝10⁹
File Instructions %
Mathlib.Data.List.Chain -5.4⬝10⁹ (-22.40%)
Mathlib.CategoryTheory.Shift.ShiftedHomOpposite -5.474⬝10⁹ (-20.19%)
2 files, Instructions -7.0⬝10⁹
File Instructions %
Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors -6.485⬝10⁹ (-16.48%)
Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift -6.980⬝10⁹ (-8.75%)
File Instructions %
Mathlib.Algebra.Homology.HomologySequence -7.353⬝10⁹ (-10.07%)
Mathlib.Algebra.Homology.HomotopyCategory.ShortExact -8.832⬝10⁹ (-17.92%)
Mathlib.CategoryTheory.Triangulated.Opposite.Basic -9.956⬝10⁹ (-22.32%)
Mathlib.RingTheory.AdicCompletion.AsTensorProduct -20.103⬝10⁹ (-8.96%)
Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four -23.314⬝10⁹ (-32.74%)
Mathlib.Algebra.Homology.ExactSequence -37.848⬝10⁹ (-56.16%)
Mathlib.Algebra.Homology.TotalComplexShift -44.219⬝10⁹ (-37.88%)
Mathlib.CategoryTheory.ComposableArrows -100.24⬝10⁹ (-32.16%)

@nomeata nomeata added this pull request to the merge queue Mar 10, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Mar 10, 2025
@nomeata nomeata added this pull request to the merge queue Mar 10, 2025
Merged via the queue into master with commit 754bab4 Mar 10, 2025
21 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@nomeata @leanprover-community-bot @leanprover-bot