chore: Add toml file for archive and counterexamples (#18388)

The end goal here is to surface these in doc-gen. For doc-gen to behave these need to be mutually importable. A step is added to the "test" run that verifies this by trying to import everything at the same time. For this new test to pass, some files need namespaces wrapped around their content. Probably we should be more principled about this namespace wrapping, but that can be left as future work, as all we really care about to start integrating with doc-gen is avoiding clashes.
leanprover-community · Feb 7, 2023 · 2d6f88c · 2d6f88c
1 parent bb37dbd
commit 2d6f88c
Show file tree

Hide file tree

Showing 16 changed files with 107 additions and 12 deletions.
diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -192,13 +192,26 @@ jobs:
 
       - name: install Python dependencies
         if: ${{ ! 1 }}
-        run: python3 -m pip install --upgrade pip pyyaml requests
+        run: python3 -m pip install --upgrade pip pyyaml requests mathlibtools
 
       - name: tests
         run: |
           set -o pipefail
           lean --json -T100000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py
 
+      - name: check archive and counterexample directories have unique identifiers
+        run: |
+          pip install mathlibtools
+          (cd archive && python -m mathlibtools.leanproject mk-all && mv all.lean archive_all.lean)
+          (cd counterexamples && python -m mathlibtools.leanproject mk-all && mv all.lean counterexamples_all.lean)
+          python -m mathlibtools.leanproject mk-all
+          echo "import all" >> all_all.lean
+          echo "import counterexamples_all" >> all_all.lean
+          echo "import archive_all" >> all_all.lean
+          echo "path ./archive" >> leanpkg.path
+          echo "path ./counterexamples" >> leanpkg.path
+          lean --json -T100000 --make all_all.lean | python3 scripts/detect_errors.py
+
       - uses: actions/setup-java@v2
         if: ${{ ! 1 }}
         with:

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -200,13 +200,26 @@ jobs:
 
       - name: install Python dependencies
         if: ${{ ! 1 }}
-        run: python3 -m pip install --upgrade pip pyyaml requests
+        run: python3 -m pip install --upgrade pip pyyaml requests mathlibtools
 
       - name: tests
         run: |
           set -o pipefail
           lean --json -T100000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py
 
+      - name: check archive and counterexample directories have unique identifiers
+        run: |
+          pip install mathlibtools
+          (cd archive && python -m mathlibtools.leanproject mk-all && mv all.lean archive_all.lean)
+          (cd counterexamples && python -m mathlibtools.leanproject mk-all && mv all.lean counterexamples_all.lean)
+          python -m mathlibtools.leanproject mk-all
+          echo "import all" >> all_all.lean
+          echo "import counterexamples_all" >> all_all.lean
+          echo "import archive_all" >> all_all.lean
+          echo "path ./archive" >> leanpkg.path
+          echo "path ./counterexamples" >> leanpkg.path
+          lean --json -T100000 --make all_all.lean | python3 scripts/detect_errors.py
+
       - uses: actions/setup-java@v2
         if: ${{ ! 1 }}
         with:

diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
@@ -178,13 +178,26 @@ jobs:
 
       - name: install Python dependencies
         if: ${{ ! IS_SELF_HOSTED }}
-        run: python3 -m pip install --upgrade pip pyyaml requests
+        run: python3 -m pip install --upgrade pip pyyaml requests mathlibtools
 
       - name: tests
         run: |
           set -o pipefail
           lean --json -T100000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py
 
+      - name: check archive and counterexample directories have unique identifiers
+        run: |
+          pip install mathlibtools
+          (cd archive && python -m mathlibtools.leanproject mk-all && mv all.lean archive_all.lean)
+          (cd counterexamples && python -m mathlibtools.leanproject mk-all && mv all.lean counterexamples_all.lean)
+          python -m mathlibtools.leanproject mk-all
+          echo "import all" >> all_all.lean
+          echo "import counterexamples_all" >> all_all.lean
+          echo "import archive_all" >> all_all.lean
+          echo "path ./archive" >> leanpkg.path
+          echo "path ./counterexamples" >> leanpkg.path
+          lean --json -T100000 --make all_all.lean | python3 scripts/detect_errors.py
+
       - uses: actions/setup-java@v2
         if: ${{ ! IS_SELF_HOSTED }}
         with:

diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
@@ -198,13 +198,26 @@ jobs:
 
       - name: install Python dependencies
         if: ${{ ! 0 }}
-        run: python3 -m pip install --upgrade pip pyyaml requests
+        run: python3 -m pip install --upgrade pip pyyaml requests mathlibtools
 
       - name: tests
         run: |
           set -o pipefail
           lean --json -T100000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py
 
+      - name: check archive and counterexample directories have unique identifiers
+        run: |
+          pip install mathlibtools
+          (cd archive && python -m mathlibtools.leanproject mk-all && mv all.lean archive_all.lean)
+          (cd counterexamples && python -m mathlibtools.leanproject mk-all && mv all.lean counterexamples_all.lean)
+          python -m mathlibtools.leanproject mk-all
+          echo "import all" >> all_all.lean
+          echo "import counterexamples_all" >> all_all.lean
+          echo "import archive_all" >> all_all.lean
+          echo "path ./archive" >> leanpkg.path
+          echo "path ./counterexamples" >> leanpkg.path
+          lean --json -T100000 --make all_all.lean | python3 scripts/detect_errors.py
+
       - uses: actions/setup-java@v2
         if: ${{ ! 0 }}
         with:

diff --git a/.gitignore b/.gitignore
@@ -1,6 +1,6 @@
 *.olean
 /_target
-/leanpkg.path
+leanpkg.path
 _cache
 __pycache__
 all.lean

diff --git a/archive/100-theorems-list/82_cubing_a_cube.lean b/archive/100-theorems-list/82_cubing_a_cube.lean
@@ -16,11 +16,12 @@ We follow the proof described here:
 http://www.alaricstephen.com/main-featured/2017/9/28/cubing-a-cube-proof
 -/
 
-
 open real set function fin
 
 noncomputable theory
 
+namespace «82»
+
 variable {n : ℕ}
 
 /-- Given three intervals `I, J, K` such that `J ⊂ I`,
@@ -517,3 +518,5 @@ begin
   exact @not_correct n s coe hfin.to_subtype h2.coe_sort
     ⟨hd.subtype _ _, (Union_subtype _ _).trans hU, hinj.injective, hn⟩
 end
+
+end «82»
diff --git a/archive/imo/imo1960_q1.lean b/archive/imo/imo1960_q1.lean
@@ -22,6 +22,8 @@ The strategy here is roughly brute force, checking the possible multiples of 11.
 
 open nat
 
+namespace imo1960_q1
+
 def sum_of_squares (L : list ℕ) : ℕ := (L.map (λ x, x * x)).sum
 
 def problem_predicate (n : ℕ) : Prop :=
@@ -98,5 +100,9 @@ Now we just need to prove the equivalence, for the precise problem statement.
 lemma left_direction (n : ℕ) (spn : solution_predicate n) : problem_predicate n :=
 by rcases spn with (rfl | rfl); norm_num [problem_predicate, sum_of_squares]
 
+end imo1960_q1
+
+open imo1960_q1
+
 theorem imo1960_q1 (n : ℕ) : problem_predicate n ↔ solution_predicate n :=
 ⟨right_direction, left_direction n⟩
diff --git a/archive/imo/imo1962_q1.lean b/archive/imo/imo1962_q1.lean
@@ -21,6 +21,8 @@ we define the problem as a predicate, and then prove a particular number is the
 of a set satisfying it.
 -/
 
+namespace imo1962_q1
+
 open nat
 
 def problem_predicate (n : ℕ) : Prop :=
@@ -154,5 +156,9 @@ begin
       exact h5.ge, }, },
 end
 
+end imo1962_q1
+
+open imo1962_q1
+
 theorem imo1962_q1 : is_least {n | problem_predicate n} 153846 :=
 ⟨satisfied_by_153846, no_smaller_solutions⟩
diff --git a/archive/imo/imo1964_q1.lean b/archive/imo/imo1964_q1.lean
@@ -24,6 +24,8 @@ integers which are a multiple of 3.
 
 open nat
 
+namespace imo1964_q1
+
 lemma two_pow_three_mul_mod_seven (m : ℕ) : 2 ^ (3 * m) ≡ 1 [MOD 7] :=
 begin
   rw pow_mul,
@@ -79,6 +81,10 @@ begin
     apply two_pow_three_mul_mod_seven }
 end
 
+end imo1964_q1
+
+open imo1964_q1
+
 theorem imo1964_q1b (n : ℕ) : ¬ (7 ∣ 2 ^ n + 1) :=
 begin
   let t := n % 3,

diff --git a/archive/imo/imo1969_q1.lean b/archive/imo/imo1969_q1.lean
@@ -17,6 +17,8 @@ the number $z = n^4 + a$ is not prime for any natural number $n$.
 
 open int nat
 
+namespace imo1969_q1
+
 /-- `good_nats` is the set of natural numbers satisfying the condition in the problem
 statement, namely the `a : ℕ` such that `n^4 + a` is not prime for any `n : ℕ`. -/
 def good_nats : set ℕ := {a : ℕ | ∀ n : ℕ, ¬ nat.prime (n^4 + a)}
@@ -67,6 +69,10 @@ in the `strict_mono` namespace. -/
 lemma a_choice_strict_mono : strict_mono a_choice :=
 ((strict_mono_id.const_add 2).nat_pow (dec_trivial : 0 < 4)).const_mul (dec_trivial : 0 < 4)
 
+end imo1969_q1
+
+open imo1969_q1
+
 /-- We conclude by using the fact that `a_choice` is an injective function from the natural numbers
 to the set `good_nats`. -/
 theorem imo1969_q1 : set.infinite {a : ℕ | ∀ n : ℕ, ¬ nat.prime (n^4 + a)} :=

diff --git a/archive/imo/imo1981_q3.lean b/archive/imo/imo1981_q3.lean
@@ -24,7 +24,7 @@ We first generalize the problem to `{1, 2, ..., N}` and specialize to `N = 1981`
 -/
 
 open int nat set
-section
+namespace imo1981_q3
 variable (N : ℕ) -- N = 1981
 
 @[mk_iff] structure problem_predicate (m n : ℤ) : Prop :=
@@ -189,7 +189,9 @@ theorem solution_greatest (H : problem_predicate N (fib K) (fib (K + 1))) :
   is_greatest (specified_set N) M :=
 ⟨⟨fib K, fib (K+1), by simp [HM], H⟩, λ k h, solution_bound HK HM h⟩
 
-end
+end imo1981_q3
+
+open imo1981_q3
 
 /-
 Now we just have to demonstrate that 987 and 1597 are in fact the largest Fibonacci

diff --git a/archive/leanpkg.toml b/archive/leanpkg.toml
@@ -0,0 +1,7 @@
+[package]
+name = "mathlib-archive"
+version = "0.1"
+path = "."
+
+[dependencies]
+mathlib = {path = ".."}
diff --git a/counterexamples/homogeneous_prime_not_prime.lean b/counterexamples/homogeneous_prime_not_prime.lean
@@ -74,7 +74,7 @@ lemma grading.mul_mem : ∀ ⦃i j : two⦄ {a b : (R × R)} (ha : a ∈ grading
 
 end
 
-notation `R` := zmod 4
+local notation `R` := zmod 4
 
 /-- `R² ≅ {(a, a) | a ∈ R} ⨁ {(0, b) | b ∈ R}` by `(x, y) ↦ (x, x) + (0, y - x)`. -/
 def grading.decompose : (R × R) →+ direct_sum two (λ i, grading R i) :=

diff --git a/counterexamples/leanpkg.toml b/counterexamples/leanpkg.toml
@@ -0,0 +1,7 @@
+[package]
+name = "mathlib-counterexamples"
+version = "0.1"
+path = "."
+
+[dependencies]
+mathlib = {path = ".."}
diff --git a/counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean b/counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean
@@ -32,7 +32,7 @@ instance inhabited : inhabited foo := ⟨zero⟩
 
 instance : has_zero foo := ⟨zero⟩
 instance : has_one foo := ⟨one⟩
-notation `ε` := eps
+local notation `ε` := eps
 
 /-- The order on `foo` is the one induced by the natural order on the image of `aux1`. -/
 def aux1 : foo → ℕ

diff --git a/counterexamples/map_floor.lean b/counterexamples/map_floor.lean
@@ -41,9 +41,9 @@ open_locale polynomial
 /-- The integers with infinitesimals adjoined. -/
 @[derive [comm_ring, nontrivial, inhabited]] def int_with_epsilon := ℤ[X]
 
-notation `ℤ[ε]` := int_with_epsilon
+local notation `ℤ[ε]` := int_with_epsilon
 
-notation `ε` := (X : ℤ[ε])
+local notation `ε` := (X : ℤ[ε])
 
 namespace int_with_epsilon