From bb09c3bb034c1bdae55c66a7009688d6622ad684 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 6 Jan 2025 12:09:32 +0000 Subject: [PATCH] Switch to the new doc-gen setup --- .github/workflows/push_master.yml | 31 ++-- LeanCamCombi.lean | 1 - LeanCamCombi/GrowthInGroups/Chevalley.lean | 3 +- .../Algebra/Polynomial/Degree/Lemmas.lean | 10 -- docbuild/lake-manifest.json | 142 ++++++++++++++++++ docbuild/lakefile.toml | 13 ++ docbuild/lean-toolchain | 1 + lake-manifest.json | 86 +++-------- lakefile.lean | 6 +- lean-toolchain | 2 +- 10 files changed, 191 insertions(+), 104 deletions(-) delete mode 100644 LeanCamCombi/Mathlib/Algebra/Polynomial/Degree/Lemmas.lean create mode 100644 docbuild/lake-manifest.json create mode 100644 docbuild/lakefile.toml create mode 100644 docbuild/lean-toolchain diff --git a/.github/workflows/push_master.yml b/.github/workflows/push_master.yml index 4fe7553e46..ec48e31075 100644 --- a/.github/workflows/push_master.yml +++ b/.github/workflows/push_master.yml @@ -45,37 +45,24 @@ jobs: run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0 - name: Get cache - run: ~/.elan/bin/lake -Kenv=dev exe cache get || true + run: ~/.elan/bin/lake exe cache get || true - name: Build project - run: ~/.elan/bin/lake -Kenv=dev build LeanCamCombi + run: ~/.elan/bin/lake build LeanCamCombi - name: Cache dependencies docs uses: actions/cache@v3 with: - path: | - .lake/build/doc/Aesop - .lake/build/doc/Batteries - .lake/build/doc/Cli - .lake/build/doc/DocGen4 - .lake/build/doc/ImportGraph - .lake/build/doc/Init - .lake/build/doc/Lake - .lake/build/doc/Lean - .lake/build/doc/LeanSearchClient - .lake/build/doc/Mathlib - .lake/build/doc/Plausible - .lake/build/doc/ProofWidgets - .lake/build/doc/Qq - .lake/build/doc/Std - .lake/build/doc/UnicodeBasic - .lake/build/doc/declarations + path: docbuild/.lake/build/doc key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} restore-keys: | MathlibDoc- - name: Build documentation - run: ~/.elan/bin/lake -Kenv=dev build LeanCamCombi:docs + working-directory: docbuild + run: | + ~/.elan/bin/lake exe cache get || true + ~/.elan/bin/lake build LeanCamCombi:docs # - name: Build blueprint and copy to `website/blueprint` # uses: xu-cheng/texlive-action@v2 @@ -95,7 +82,7 @@ jobs: - name: Copy documentation to `website/docs` run: | - mv .lake/build/doc website/docs + mv docbuild/.lake/build/doc website/docs - name: Bundle dependencies uses: ruby/setup-ruby@v1 @@ -119,4 +106,4 @@ jobs: - name: Make sure the cache works run: | - mv website/docs .lake/build/doc + mv website/docs docbuild/.lake/build/doc diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean index 2561919de8..5d7c136d1f 100644 --- a/LeanCamCombi.lean +++ b/LeanCamCombi.lean @@ -36,7 +36,6 @@ import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Basic import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Degrees import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Equiv import LeanCamCombi.Mathlib.Algebra.Order.Monoid.Unbundled.Pow -import LeanCamCombi.Mathlib.Algebra.Polynomial.Degree.Lemmas import LeanCamCombi.Mathlib.Algebra.Polynomial.Degree.Operations import LeanCamCombi.Mathlib.Algebra.Ring.Hom.Defs import LeanCamCombi.Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic diff --git a/LeanCamCombi/GrowthInGroups/Chevalley.lean b/LeanCamCombi/GrowthInGroups/Chevalley.lean index 9e5e5e2656..f3f9dec118 100644 --- a/LeanCamCombi/GrowthInGroups/Chevalley.lean +++ b/LeanCamCombi/GrowthInGroups/Chevalley.lean @@ -1,11 +1,10 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Polynomial import Mathlib.Data.DFinsupp.WellFounded -import LeanCamCombi.GrowthInGroups.ConstructiblePrimeSpectrum -import LeanCamCombi.Mathlib.Algebra.Polynomial.Degree.Lemmas import LeanCamCombi.Mathlib.Algebra.Polynomial.Degree.Operations import LeanCamCombi.Mathlib.Data.Prod.Lex import LeanCamCombi.Mathlib.RingTheory.FinitePresentation import LeanCamCombi.Mathlib.RingTheory.Localization.Integral +import LeanCamCombi.GrowthInGroups.ConstructiblePrimeSpectrum open Polynomial PrimeSpectrum TensorProduct Topology diff --git a/LeanCamCombi/Mathlib/Algebra/Polynomial/Degree/Lemmas.lean b/LeanCamCombi/Mathlib/Algebra/Polynomial/Degree/Lemmas.lean deleted file mode 100644 index 8d7eb6a4b5..0000000000 --- a/LeanCamCombi/Mathlib/Algebra/Polynomial/Degree/Lemmas.lean +++ /dev/null @@ -1,10 +0,0 @@ -import Mathlib.Algebra.Polynomial.Degree.Lemmas - -namespace Polynomial -variable {R : Type*} [CommRing R] - -lemma degree_C_mul_of_mul_ne_zero {r : R} {p : R[X]} (h : r * p.leadingCoeff ≠ 0) : - (C r * p).degree = p.degree := by - rw [degree_mul' (by simpa)]; simp [left_ne_zero_of_mul h] - -end Polynomial diff --git a/docbuild/lake-manifest.json b/docbuild/lake-manifest.json new file mode 100644 index 0000000000..2831f46bf6 --- /dev/null +++ b/docbuild/lake-manifest.json @@ -0,0 +1,142 @@ +{"version": "1.1.0", + "packagesDir": "../.lake/packages", + "packages": + [{"url": "https://github.com/leanprover/doc-gen4", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "0291556f04e89d46cd2999f0f4c1164c81778207", + "name": "«doc-gen4»", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.15.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"type": "path", + "scope": "", + "name": "LeanCamCombi", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "./../", + "configFile": "lakefile.lean"}, + {"url": "https://github.com/mhuisi/lean4-cli", + "type": "git", + "subDir": null, + "scope": "", + "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "scope": "", + "rev": "470c41643209208d325a5a7315116f293c7443fb", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "46376bc3c8f46ac1a1fd7712856b0f7bd6166098", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "f8ed91f3a9d806648ae6a03ab98c8b87e8bedc7e", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.15.0", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.15.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "9a0b533c2fbd6195df067630be18e11e4349051c", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.15.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "2b000e02d50394af68cfb4770a291113d94801b5", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.48", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "2689851f387bb2cef351e6825fe94a56a304ca13", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.15.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.15.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.15.0", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "docbuild", + "lakeDir": ".lake"} diff --git a/docbuild/lakefile.toml b/docbuild/lakefile.toml new file mode 100644 index 0000000000..e7b7ea260d --- /dev/null +++ b/docbuild/lakefile.toml @@ -0,0 +1,13 @@ +name = "docbuild" +reservoir = false +version = "0.1.0" +packagesDir = "../.lake/packages" + +[[require]] +name = "LeanCamCombi" +path = "../" + +[[require]] +scope = "leanprover" +name = "doc-gen4" +rev = "v4.15.0" diff --git a/docbuild/lean-toolchain b/docbuild/lean-toolchain new file mode 100644 index 0000000000..d0eb99ff68 --- /dev/null +++ b/docbuild/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.15.0 diff --git a/lake-manifest.json b/lake-manifest.json index ba085c6de8..c03bcbc0fb 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,74 +1,24 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/doc-gen4", + [{"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "e498801db5f148f633237b7cf9f4284f0fd197f8", - "name": "«doc-gen4»", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/mathlib4.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "0571c82877b7c2b508cbc9a39e041eb117d050b7", + "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": null, + "inputRev": "v4.15.0", "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/mhuisi/lean4-cli", - "type": "git", - "subDir": null, - "scope": "", - "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "type": "git", - "subDir": null, - "scope": "", - "rev": "d55279d2ff01759fa75752fcf1a93d1db8db18ff", - "name": "UnicodeBasic", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", - "type": "git", - "subDir": null, - "scope": "", - "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b", - "name": "BibtexQuery", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/acmepjz/md4lean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "fe8e6e649ac8251f43c6f6f934f095ebebce7e7c", - "name": "MD4Lean", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35", + "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0-rc1", + "inputRev": "v4.15.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", @@ -85,10 +35,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377", + "rev": "9a0b533c2fbd6195df067630be18e11e4349051c", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0-rc1", + "inputRev": "v4.15.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", @@ -105,29 +55,39 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a4a08d92be3de00def5298059bf707c72dfd3c66", + "rev": "2689851f387bb2cef351e6825fe94a56a304ca13", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.15.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac", + "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", + "inputRev": "v4.15.0", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f007bfe46ea8fb801ec907df9ab540054abcc5fd", + "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b", "name": "batteries", "manifestFile": "lake-manifest.json", + "inputRev": "v4.15.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", + "name": "Cli", + "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}], diff --git a/lakefile.lean b/lakefile.lean index a75267030c..7f99cf7e2e 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -9,11 +9,7 @@ package LeanCamCombi where ⟨`pp.proofs.withType, false⟩] require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" - -meta if get_config? env = some "dev" then -- dev is so not everyone has to build it -require «doc-gen4» from git - "https://github.com/leanprover/doc-gen4" @ "main" + "https://github.com/leanprover-community/mathlib4.git" @ "v4.15.0" @[default_target] lean_lib LeanCamCombi diff --git a/lean-toolchain b/lean-toolchain index cf25a9816f..d0eb99ff68 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.15.0-rc1 +leanprover/lean4:v4.15.0