chore: initial port to the module system

.github/build.in.yml

@@ -73,7 +73,7 @@ jobs:
           # Recall that on the `leanprover-community/mathlib4-nightly-testing` repository,
           # we don't maintain a `master` branch at all.
           # For PRs and pushes to this repository, we will use `nightly-testing` instead.
-          ref: ${{ github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing' || 'master' }}
+          ref: modulize  # TODO
           path: master-branch
 
       # Checkout the PR branch into a subdirectory
@@ -463,7 +463,7 @@ jobs:
         id: test
         run: |
           cd pr-branch
-          lake --iofail test
+          lake test
       - name: end gh-problem-match-wrap for test step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
         with:
@@ -590,13 +590,13 @@ jobs:
       - name: verify that everything was available in the cache
         run: |
           echo "::group::{verify Mathlib cache}"
-          lake build --no-build -v Mathlib
+          lake build --no-build --rehash -v Mathlib
           echo "::endgroup::"
           echo "::group::{verify Archive cache}"
-          lake build --no-build -v Archive
+          lake build --no-build --rehash -v Archive
           echo "::endgroup::"
           echo "::group::{verify Counterexamples cache}"
-          lake build --no-build -v Counterexamples
+          lake build --no-build --rehash -v Counterexamples
           echo "::endgroup::"
 
       - name: check declarations in db files

.github/workflows/bors.yml

@@ -83,7 +83,7 @@ jobs:
           # Recall that on the `leanprover-community/mathlib4-nightly-testing` repository,
           # we don't maintain a `master` branch at all.
           # For PRs and pushes to this repository, we will use `nightly-testing` instead.
-          ref: ${{ github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing' || 'master' }}
+          ref: modulize  # TODO
           path: master-branch
 
       # Checkout the PR branch into a subdirectory
@@ -473,7 +473,7 @@ jobs:
         id: test
         run: |
           cd pr-branch
-          lake --iofail test
+          lake test
       - name: end gh-problem-match-wrap for test step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
         with:
@@ -600,13 +600,13 @@ jobs:
       - name: verify that everything was available in the cache
         run: |
           echo "::group::{verify Mathlib cache}"
-          lake build --no-build -v Mathlib
+          lake build --no-build --rehash -v Mathlib
           echo "::endgroup::"
           echo "::group::{verify Archive cache}"
-          lake build --no-build -v Archive
+          lake build --no-build --rehash -v Archive
           echo "::endgroup::"
           echo "::group::{verify Counterexamples cache}"
-          lake build --no-build -v Counterexamples
+          lake build --no-build --rehash -v Counterexamples
           echo "::endgroup::"
 
       - name: check declarations in db files

.github/workflows/build.yml

@@ -90,7 +90,7 @@ jobs:
           # Recall that on the `leanprover-community/mathlib4-nightly-testing` repository,
           # we don't maintain a `master` branch at all.
           # For PRs and pushes to this repository, we will use `nightly-testing` instead.
-          ref: ${{ github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing' || 'master' }}
+          ref: modulize  # TODO
           path: master-branch
 
       # Checkout the PR branch into a subdirectory
@@ -480,7 +480,7 @@ jobs:
         id: test
         run: |
           cd pr-branch
-          lake --iofail test
+          lake test
       - name: end gh-problem-match-wrap for test step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
         with:
@@ -607,13 +607,13 @@ jobs:
       - name: verify that everything was available in the cache
         run: |
           echo "::group::{verify Mathlib cache}"
-          lake build --no-build -v Mathlib
+          lake build --no-build --rehash -v Mathlib
           echo "::endgroup::"
           echo "::group::{verify Archive cache}"
-          lake build --no-build -v Archive
+          lake build --no-build --rehash -v Archive
           echo "::endgroup::"
           echo "::group::{verify Counterexamples cache}"
-          lake build --no-build -v Counterexamples
+          lake build --no-build --rehash -v Counterexamples
           echo "::endgroup::"
 
       - name: check declarations in db files

.github/workflows/build_fork.yml

@@ -42,7 +42,7 @@ permissions:
 
 jobs:
   build:
-    if: github.event.pull_request.head.repo.fork
+    if: github.event.pull_request.head.repo.fork FORK_CONDITIONFORK_CONDITION github.repository != 'leanprover-community/mathlib4-nightly-testing'
     name: Build (fork)
     runs-on: pr
     outputs:
@@ -87,7 +87,7 @@ jobs:
           # Recall that on the `leanprover-community/mathlib4-nightly-testing` repository,
           # we don't maintain a `master` branch at all.
           # For PRs and pushes to this repository, we will use `nightly-testing` instead.
-          ref: ${{ github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing' || 'master' }}
+          ref: modulize  # TODO
           path: master-branch
 
       # Checkout the PR branch into a subdirectory
@@ -477,7 +477,7 @@ jobs:
         id: test
         run: |
           cd pr-branch
-          lake --iofail test
+          lake test
       - name: end gh-problem-match-wrap for test step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
         with:
@@ -547,7 +547,7 @@ jobs:
 
   post_steps:
     name: Post-Build Step (fork)
-    if: github.event.pull_request.head.repo.fork
+    if: github.event.pull_request.head.repo.fork FORK_CONDITIONFORK_CONDITION github.repository != 'leanprover-community/mathlib4-nightly-testing'
     needs: [build]
     runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
     steps:
@@ -604,13 +604,13 @@ jobs:
       - name: verify that everything was available in the cache
         run: |
           echo "::group::{verify Mathlib cache}"
-          lake build --no-build -v Mathlib
+          lake build --no-build --rehash -v Mathlib
           echo "::endgroup::"
           echo "::group::{verify Archive cache}"
-          lake build --no-build -v Archive
+          lake build --no-build --rehash -v Archive
           echo "::endgroup::"
           echo "::group::{verify Counterexamples cache}"
-          lake build --no-build -v Counterexamples
+          lake build --no-build --rehash -v Counterexamples
           echo "::endgroup::"
 
       - name: check declarations in db files
@@ -676,7 +676,7 @@ jobs:
 
   style_lint:
     name: Lint style (fork)
-    if: github.event.pull_request.head.repo.fork
+    if: github.event.pull_request.head.repo.fork FORK_CONDITIONFORK_CONDITION github.repository != 'leanprover-community/mathlib4-nightly-testing'
     runs-on: ubuntu-latest
     steps:
       - uses: leanprover-community/lint-style-action@a7e7428fa44f9635d6eb8e01919d16fd498d387a # 2025-08-18
@@ -687,7 +687,7 @@ jobs:
 
   final:
     name: Post-CI job (fork)
-    if: github.event.pull_request.head.repo.fork
+    if: github.event.pull_request.head.repo.fork FORK_CONDITIONFORK_CONDITION github.repository != 'leanprover-community/mathlib4-nightly-testing'
     needs: [style_lint, build, post_steps]
     runs-on: ubuntu-latest
     steps:

.github/workflows/mk_build_yml.sh

@@ -73,7 +73,7 @@ on:
 
 name: continuous integration (mathlib forks)
 EOF
-  include "github.event.pull_request.head.sha" pr "github.event.pull_request.head.repo.fork" " (fork)" ubuntu-latest
+  include "github.event.pull_request.head.sha" pr "github.event.pull_request.head.repo.fork && github.repository != 'leanprover-community\/mathlib4-nightly-testing'" " (fork)" ubuntu-latest
 }
 
 include() {

Cache/IO.lean

@@ -70,7 +70,7 @@ def CURLBIN :=
 
 /-- leantar version at https://github.com/digama0/leangz -/
 def LEANTARVERSION :=
-  "0.1.16-pre3"
+  "0.1.16-pre4"
 
 def EXE := if System.Platform.isWindows then ".exe" else ""
 
@@ -90,7 +90,7 @@ def getLeanTar : IO String := do
 /-- Bump this number to invalidate the cache, in case the existing hashing inputs are insufficient.
 It is not a global counter, and can be reset to 0 as long as the lean githash or lake manifest has
 changed since the last time this counter was touched. -/
-def rootHashGeneration : UInt64 := 3
+def rootHashGeneration : UInt64 := 4
 
 /--
 `CacheM` stores the following information: