From 2d6f88c296da8df484d7f5b9ee1d10910ab473a2 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 7 Feb 2023 01:58:42 +0000 Subject: [PATCH] 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. --- .github/workflows/bors.yml | 15 ++++++++++++++- .github/workflows/build.yml | 15 ++++++++++++++- .github/workflows/build.yml.in | 15 ++++++++++++++- .github/workflows/build_fork.yml | 15 ++++++++++++++- .gitignore | 2 +- archive/100-theorems-list/82_cubing_a_cube.lean | 5 ++++- archive/imo/imo1960_q1.lean | 6 ++++++ archive/imo/imo1962_q1.lean | 6 ++++++ archive/imo/imo1964_q1.lean | 6 ++++++ archive/imo/imo1969_q1.lean | 6 ++++++ archive/imo/imo1981_q3.lean | 6 ++++-- archive/leanpkg.toml | 7 +++++++ counterexamples/homogeneous_prime_not_prime.lean | 2 +- counterexamples/leanpkg.toml | 7 +++++++ .../linear_order_with_pos_mul_pos_eq_zero.lean | 2 +- counterexamples/map_floor.lean | 4 ++-- 16 files changed, 107 insertions(+), 12 deletions(-) create mode 100644 archive/leanpkg.toml create mode 100644 counterexamples/leanpkg.toml diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml index e43db8caf1548..e808ac75f1a2e 100644 --- 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 index 8296a49e4e11b..0656b61d919ae 100644 --- 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 index ffed44267c589..f17250cc6b119 100644 --- 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 index 3a093a8e654f4..8f12c3bc1f37d 100644 --- 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 index ed583e63ad380..a7798b842bb80 100644 --- 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 index 330a23188f703..ff662f64b69eb 100644 --- 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 index 7caef8294f29b..fa3ee7680092f 100644 --- 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 index 7bd2c6f015d7c..0afc5e6be6726 100644 --- 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 index ac90068a7afb6..fd987ba4f5f10 100644 --- 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 index a2ccb8cca33e6..3eee264d353ca 100644 --- 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 index ea34d76d03bf2..4b40612e5a873 100644 --- 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 new file mode 100644 index 0000000000000..a89c0e895b5f7 --- /dev/null +++ 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 index 8b9f1a9328952..8692774542313 100644 --- 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 new file mode 100644 index 0000000000000..814d73c4e45c1 --- /dev/null +++ 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 index 28298a847d2cc..6e08c5f9f847f 100644 --- 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 index 8c00769a84eaf..b1c262d6d780c 100644 --- 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