Skip to content

feat: module header keyword for enabling module system#8021

Merged
nomeata merged 4 commits intoleanprover:masterfrom
Kha:push-wpopyszzmuoz
Apr 21, 2025
Merged

feat: module header keyword for enabling module system#8021
nomeata merged 4 commits intoleanprover:masterfrom
Kha:push-wpopyszzmuoz

Conversation

@Kha
Copy link
Copy Markdown
Member

@Kha Kha commented Apr 18, 2025

Not yet enabled anywhere

@Kha Kha added the changelog-no Do not include this PR in the release changelog label Apr 18, 2025
@Kha Kha requested review from mhuisi and tydeu as code owners April 18, 2025 12:46
@Kha Kha changed the base branch from master to nightly-with-mathlib April 18, 2025 14:11
@Kha Kha marked this pull request as draft April 18, 2025 14:11
@Kha Kha force-pushed the push-wpopyszzmuoz branch from 6821c01 to 493a507 Compare April 18, 2025 14:53
@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 Apr 18, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 18, 2025
Update lean-toolchain for testing leanprover/lean4#8021
2115ed7
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 18, 2025
Update lean-toolchain for testing leanprover/lean4#8021
e3bc5b7
@ghost
Copy link
Copy Markdown

ghost commented Apr 18, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

  • 🟡 Mathlib branch lean-pr-testing-8021 build this PR didn't complete normally. (2025-04-18 15:23:08) View Log
  • 💥 Mathlib branch lean-pr-testing-8021 build failed against this PR. (2025-04-18 15:35:26) View Log
  • 💥 Mathlib branch lean-pr-testing-8021 build failed against this PR. (2025-04-18 16:50:27) View Log
  • 💥 Mathlib branch lean-pr-testing-8021 build failed against this PR. (2025-04-18 17:43:02) View Log
  • 💥 Mathlib branch lean-pr-testing-8021 build failed against this PR. (2025-04-20 15:23:02) View Log
  • ✅ Mathlib branch lean-pr-testing-8021 has successfully built against this PR. (2025-04-20 20:14:32) View Log
  • ✅ Mathlib branch lean-pr-testing-8021 has successfully built against this PR. (2025-04-21 11:26:20) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 11f6326102d4dd09468bec0defd4bc4344690426 --onto de27872f3ffee8f2eb13f36fbb8fec9bcdfe3b8c. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-21 15:24:40)

@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Apr 18, 2025
@Kha Kha force-pushed the push-wpopyszzmuoz branch 3 times, most recently from d32a7ce to 1564613 Compare April 20, 2025 18:58
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 20, 2025
Trigger CI for leanprover/lean4#8021
1def263
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 20, 2025
Trigger CI for leanprover/lean4#8021
e9586ec
@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 Apr 20, 2025
@Kha Kha force-pushed the push-wpopyszzmuoz branch from 1564613 to f833c9a Compare April 21, 2025 13:48
@Kha Kha marked this pull request as ready for review April 21, 2025 13:48
@Kha Kha force-pushed the push-wpopyszzmuoz branch from f833c9a to d27f162 Compare April 21, 2025 13:50
@Kha Kha force-pushed the push-wpopyszzmuoz branch from d27f162 to 40a13f3 Compare April 21, 2025 14:48
@Kha Kha requested review from TwoFX, kim-em and leodemoura as code owners April 21, 2025 14:48
@Kha Kha changed the base branch from nightly-with-mathlib to master April 21, 2025 16:22
@nomeata nomeata merged commit d6c30a8 into leanprover:master Apr 21, 2025
19 checks passed
@Kha Kha deleted the push-wpopyszzmuoz branch April 21, 2025 18:10
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request May 2, 2025
@kim-em @TwoFX
@Rob23oba @Kha @kmill @joelriou @Ruben-VandeVelde @jcommelin
chore: adaptations for nightly-2025-05-01 (#24524)
0ec9062 
* Trigger CI for leanprover/lean4#7971

* WIP

* WIP

* WIP

* Trigger CI for leanprover/lean4#7971

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

* Fix

* Trigger CI for leanprover/lean4#7971

* remove adaptation notes

* Fix

* Fix

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

* revert some stuff

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

* WIP

* Part one

* Part two

* lake update and fix

* Fix

* Trigger CI for leanprover/lean4#7983

* Shake

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

* lake update

* .

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

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

* fix

* fix: !bench after Lake path changes (#24143)

* fix

* fix

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

* Merge master into nightly-testing

* temporarirly disable sythorder checking for Grind.IsCharP instance

* shake

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

* fix

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

* make fix more robust

* fix test

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

* .

* sorries

* sorries

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

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

* fix

* not there yet

* comment out

* comment out

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

* bump batteries

* more

* hacky fix?

* add comment

* fix lint-style

* Fix shake: Parser.parseHeader returns TSyntax instead of Syntax after the new module system

* Clean up

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

* Lake update

* Fix

* Fix

* Fix

* Fix

* fix to Mathlib/Algebra/Homology/Embedding/Connect.lean

* Fix

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

* fix MinImports

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

* lake update

* fix

* fixes

* fix

* fix deprecations

* remove accidental files

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

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

* fixes

* cleanup adaptation note

* shake --fix

* cleanup

* .

* cleanup

* cleanup

* cleanup

* comments

* cleanuo

* move batteries back to nightly-testing

* fix

* fix build hopefully?

* fix build hopefully?

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

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

* lake update

* Fix

* fix grind instances

* shake

* Cleanup

* shake

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

* fix

* deprecation

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

* shake

* fix GrindInstances

* basic test for grind +ring

* fixes for leanprover/lean4#8161

* fixes

* chore: adaptations for nightly-2025-04-29

* Merge master into nightly-testing

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

* lake update

* fix

* fix merge

* fix merge

* Drop a few unnecessary changes

* fix test

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

* fix

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request May 5, 2025
@jcommelin @Rob23oba
@TwoFX @kim-em @Kha @kmill @joelriou @Ruben-VandeVelde
chore: adaptations for nightly-2025-05-03 (#24569)
4374ee0 
* chore: bump to nightly-2025-04-16

* revert some stuff

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

* WIP

* Part one

* Part two

* lake update and fix

* Fix

* Trigger CI for leanprover/lean4#7983

* Shake

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

* lake update

* .

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

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

* fix

* fix: !bench after Lake path changes (#24143)

* fix

* fix

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

* Merge master into nightly-testing

* temporarirly disable sythorder checking for Grind.IsCharP instance

* shake

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

* fix

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

* make fix more robust

* fix test

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

* .

* sorries

* sorries

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

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

* fix

* not there yet

* comment out

* comment out

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

* bump batteries

* more

* hacky fix?

* add comment

* fix lint-style

* Fix shake: Parser.parseHeader returns TSyntax instead of Syntax after the new module system

* Clean up

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

* Lake update

* Fix

* Fix

* Fix

* Fix

* fix to Mathlib/Algebra/Homology/Embedding/Connect.lean

* Fix

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

* fix MinImports

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

* lake update

* fix

* fixes

* fix

* fix deprecations

* remove accidental files

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

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

* fixes

* cleanup adaptation note

* shake --fix

* cleanup

* .

* cleanup

* cleanup

* cleanup

* comments

* cleanuo

* move batteries back to nightly-testing

* fix

* fix build hopefully?

* fix build hopefully?

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

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

* lake update

* Fix

* fix grind instances

* shake

* Cleanup

* shake

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

* fix

* deprecation

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

* shake

* fix GrindInstances

* basic test for grind +ring

* fixes for leanprover/lean4#8161

* fixes

* chore: adaptations for nightly-2025-04-29

* Merge master into nightly-testing

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

* lake update

* fix

* fix merge

* fix merge

* Drop a few unnecessary changes

* fix test

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

* fix

* Merge master into nightly-testing

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

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

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

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

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

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

@TwoFX TwoFX Awaiting requested review from TwoFX

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

@leodemoura leodemoura Awaiting requested review from leodemoura

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-no Do not include this PR in the release changelog 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.

2 participants

@Kha @nomeata