Skip to content

fix: run @[init] declarations in declaration order#10217

Merged
Kha merged 2 commits intoleanprover:masterfrom
Kha:push-oqxwusqytpmo
Sep 10, 2025
Merged

fix: run @[init] declarations in declaration order#10217
Kha merged 2 commits intoleanprover:masterfrom
Kha:push-oqxwusqytpmo

Conversation

@Kha
Copy link
Copy Markdown
Member

@Kha Kha commented Sep 2, 2025 •
edited
Loading

This PR ensures @[init] declarations such as from initialize are run in the order they were declared on import.

Fixes #10175

@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 Sep 2, 2025
@ghost
Copy link
Copy Markdown

ghost commented Sep 2, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d63d1188cc03eccc6d0d81546eaad333c3d5aa35 --onto c4e5f575121d508e02c82edd603f3c2808bdb5bc. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-02 13:40:59)
  • ✅ Mathlib branch lean-pr-testing-10217 has successfully built against this PR. (2025-09-02 15:40:40) View Log
  • 💥 Mathlib branch lean-pr-testing-10217 build failed against this PR. (2025-09-03 08:27:35) View Log
  • ✅ Mathlib branch lean-pr-testing-10217 has successfully built against this PR. (2025-09-03 17:50:27) View Log
  • ✅ Mathlib branch lean-pr-testing-10217 has successfully built against this PR. (2025-09-10 10:08:45) View Log

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Sep 2, 2025 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase d63d1188cc03eccc6d0d81546eaad333c3d5aa35 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-02 13:41:00)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-08-31 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-09-02 14:33:32)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-09-09 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-09-10 09:02:38)

@Kha Kha force-pushed the push-oqxwusqytpmo branch from fd9a5a2 to cfa0cf8 Compare September 2, 2025 13:47
@Kha
Copy link
Copy Markdown
Member Author

Kha commented Sep 2, 2025

@Rob23oba Could you check whether this resolves the issue?

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Sep 2, 2025
Update lean-toolchain for testing leanprover/lean4#10217
39ac934
ghost pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 2, 2025
Update lean-toolchain for testing leanprover/lean4#10217
7925fda
Rob23oba
Rob23oba reviewed Sep 2, 2025
View reviewed changes
@ghost ghost added the builds-mathlib CI has verified that Mathlib builds against this PR label Sep 2, 2025
@Kha Kha force-pushed the push-oqxwusqytpmo branch from cfa0cf8 to e8a8ab2 Compare September 3, 2025 07:31
@Kha
Copy link
Copy Markdown
Member Author

Kha commented Sep 3, 2025

!bench

Rob23oba
Rob23oba reviewed Sep 3, 2025
View reviewed changes
src/Lean/Attributes.lean Outdated
Comment on lines +245 to +246
let r : Array (Name × α) := m.foldl (fun a n p => a.push (n, p)) #[]
r.qsort (fun a b => Name.quickLt a.1 b.1)
Copy link
Copy Markdown
Contributor

@Rob23oba Rob23oba Sep 3, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
let r : Array (Name × α) := m.foldl (fun a n p => a.push (n, p)) #[]
r.qsort (fun a b => Name.quickLt a.1 b.1)
-- The elements are already ordered by `Name.quickCmp`, no need to sort them
(m : TreeMap Name α Name.quickCmp).toArray

That's what I meant with the "why not just fun m => m.toArray" thing. I suppose this is really an unrelated change though. Otherwise I think this fixes the problem in pretty much all cases; but for example doesn't help against:

def a_init : IO Nat :=
  pure 5

@[noinline]
opaque a : Nat

def b_init : IO Nat :=
  pure (a + 7)

@[init b_init]
opaque b : Nat

attribute [init a_init] a

but maybe we should just simply forbid that case? Regardless it would be nice to see how this impacts memory and performance.

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Sep 3, 2025

Here are the benchmark results for commit e8a8ab2.
There were significant changes against commit c4e5f57:

  Benchmark                   Metric           Change
  =============================================================
+ bv_decide_inequality.lean   maxrss            -1.4% (-27.0 σ)
+ lake build clean            task-clock        -1.2% (-70.3 σ)
- phashmap.lean               instructions       1.2% (202.6 σ)
+ stdlib                      grind linarith   -16.8% (-24.3 σ)

@Rob23oba
Copy link
Copy Markdown
Contributor

Rob23oba commented Sep 3, 2025 •
edited
Loading

Huh; I assume not iterating through all constants is making the difference here?
Edit: Wait but which modules even contain @[init] declarations? Lake?

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Sep 3, 2025
Update lean-toolchain for leanprover/lean4#10217
84c8021
ghost pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 3, 2025
Update lean-toolchain for leanprover/lean4#10217
16329a2
@ghost ghost added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Sep 3, 2025
@Kha
Copy link
Copy Markdown
Member Author

Kha commented Sep 3, 2025

I'm not sure how significant any of that is but the phashmap, which is a bit surprising

@Rob23oba
Copy link
Copy Markdown
Contributor

Rob23oba commented Sep 3, 2025

Maybe it has to do with the @[specialize] attribute?

@Kha
Copy link
Copy Markdown
Member Author

Kha commented Sep 3, 2025

I don't really see how

@Rob23oba
Copy link
Copy Markdown
Contributor

Rob23oba commented Sep 3, 2025 •
edited
Loading

Yeah this was basically the only parametric attribute I could find that might be used more frequently; although I don't know either how such a difference would happen; maybe this is just noise? Maybe try merging nightly-with-mathlib and !benching again?

@ghost ghost 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 Sep 3, 2025
@Kha
Copy link
Copy Markdown
Member Author

Kha commented Sep 10, 2025

!bench

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Sep 10, 2025
Update lean-toolchain for leanprover/lean4#10217
35fa640
ghost pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 10, 2025
Update lean-toolchain for leanprover/lean4#10217
3cc70ad
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Sep 10, 2025

Here are the benchmark results for commit dfcd414.
There were significant changes against commit c75d37f:

  Benchmark      Metric          Change
  =====================================
- channel.lean   unbounded_seq     1.3%

@Kha Kha marked this pull request as ready for review September 10, 2025 09:50
@Kha Kha enabled auto-merge September 10, 2025 09:50
@Kha Kha added this pull request to the merge queue Sep 10, 2025
Merged via the queue into leanprover:master with commit de2e935 Sep 10, 2025
23 of 25 checks passed
@Kha Kha deleted the push-oqxwusqytpmo branch September 10, 2025 10:51
kim-em added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 15, 2025
@leanprover-community-bot-assistant @Rob23oba
@kim-em @Vierkantor @tydeu @datokrat @nomeata @kmill
chore: adaptations for nightly-2025-09-15 (#63)
4244037 
* fix deprecations

* remove upstreamed defs

* two fixes

* fix merge

* fix merge

* revert sqrt changes

* ugh

* fix from nightly-testing

* fix merge

* remove test deleted on master

* fix test

* note about test

* .

* Update lean-toolchain for leanprover/lean4#10194

* chore: bump to nightly-2025-09-02

* adjust to upstream changes

* fix

* fix

* long line

* Use Mathlib's nightly toolchain to run docgen in the nightly test

* simpNF linter

* whitespace

* Update lean-toolchain for testing leanprover/lean4#10217

* Correct the working directory: should be 'docbuild'

* Rework the grind regression report as a nightly-testing regression report

It should still report the same things, but now as one message for all regression kinds

* feat(Cache): download speeds & more info on errors

* fix(Cache): add base download failure message

* fixes

* turn off linter

* adaptation note

* turn off linter.nightlyRegressionSet

* chore: adaptations for nightly-2025-09-02

* Update lean-toolchain for testing leanprover/lean4#10059

* Update lean-toolchain for leanprover/lean4#10217

* chore: bump to nightly-2025-09-03

* Remove the erroring nightly regression report, we'll develop this on another branch.

* fixes

* update LibraryRewrite test

* Update lean-toolchain for leanprover/lean4#10059

* chore: bump to nightly-2025-09-04

* fix

* chore: bump to nightly-2025-09-05

* chore: adaptations for nightly-2025-09-05

* chore: bump to nightly-2025-09-06

* Update lean-toolchain for testing leanprover/lean4#10271

* Adapt to leanprover/lean4#10271

* Bump batteries

* Update lean-toolchain for leanprover/lean4#10271

* chore: bump to nightly-2025-09-07

* nolint unusedArguments

* Merge master into nightly-testing

* chore: bump to nightly-2025-09-08

* fixes

* chore: bump to nightly-2025-09-09

* fix thing

* Update lean-toolchain for testing leanprover/lean4#10306

* temporarily remove test

* adaptation note

* master version of Cache/Requests.lean

* chore: bump to nightly-2025-09-10

* adaptation note

* chore: adaptations for nightly-2025-09-10

* merge lean-pr-testing-10059

* bump toolchain manually??

* restore test

* chore: bump to nightly-2025-09-11

* lake update

* fix

* adaptations for leanprover/lean4#10307

* remove validateDocComment in ToAdditive

* remove upstreamed Function.Injective

* update assert_not_exists

* oops

* comment out DeriveTraversable

* chore: replace some grind attibutes with grind_pattern, to be robust for future heuristic changes

* suggestions from Rob23oba

* lshake --fix

* fix bad shake

* shake --update

* .

* chore: adaptations for nightly-2025-09-11

* chore: bump to nightly-2025-09-12

* Revert "oops"

This reverts commit 517b832.

* Revert "comment out DeriveTraversable"

This reverts commit 0460eb8.

* fix DeriveTraversable

* add `binders` fields

* fix

* fixes

* update manifest

* fixes

* fixes

* fixes

* chore: bump to nightly-2025-09-13

* fixes

* fixes

* fixes

* fixes

* fixes

* fixes

* fixes

* remove adaptation note

* Update lean-toolchain for testing leanprover/lean4#10373

* fixes

* chore: bump to nightly-2025-09-14

* Update lean-toolchain for testing leanprover/lean4#10377

* fix

* fix

* fix

* fix emrge

* update batteries

* chore: adaptations for nightly-2025-09-14

* Merge master into nightly-testing

* Update Mathlib/Data/List/Basic.lean

* Merge master into nightly-testing

* chore: adaptations for nightly-2025-09-14

* chore: bump to nightly-2025-09-15

---------

Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

@zwarich zwarich Awaiting requested review from zwarich

1 more reviewer

@Rob23oba Rob23oba Rob23oba left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-other 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.

@[init] declarations are sometimes run in the wrong order

3 participants

@Kha @leanprover-bot @Rob23oba