From d23dcc88ea73817821afda91521eecc8ba7bb5b0 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Sun, 2 Nov 2025 21:16:29 -0500 Subject: [PATCH] fix: lake: pin mathlib in `new`/`init` to toolchain (#11063) This PR changes the `math` and `math-lax` templates for `lake new` and `lake init` to use the version of Mathlib corresponding to the current Lean toolchain. Thus, `lake +x.y.z new math` will use the Mathlib for Lean `x.y.z`. On the other hand, `lake update` on such packages will no longer update Mathlib automatically. Users will need to change the Mathlib revision in the configuration file before updating. This change was inspired by a [discussion](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Build.20error.20on.20.60lake.20.2Bleanprover.2Flean4.3Av4.2E22.2E0.20new.20foo.20math.60/near/546236449) on the community Zulip. --- src/lake/Lake/CLI/Init.lean | 66 +++++++++++++------------- tests/lake/tests/common.sh | 5 ++ tests/lake/tests/init/.gitignore | 1 + tests/lake/tests/init/clean.sh | 1 + tests/lake/tests/init/online-test.sh | 31 ++++++++++++ tests/lake/tests/init/test.sh | 70 +++++++++++----------------- tests/lake/tests/toolchain/test.sh | 2 - 7 files changed, 98 insertions(+), 78 deletions(-) create mode 100755 tests/lake/tests/init/online-test.sh diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index 912704d4a9..293f9d187f 100644 --- a/src/lake/Lake/CLI/Init.lean +++ b/src/lake/Lake/CLI/Init.lean @@ -127,7 +127,7 @@ defaultTargets = [{repr libRoot}] name = {repr libRoot} " -def mathLaxLeanConfigFileContents (pkgName libRoot : String) := +def mathLaxLeanConfigFileContents (pkgName libRoot rev : String) := s!"import Lake open Lake DSL @@ -138,14 +138,14 @@ package {repr pkgName} where ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b` ] -require \"leanprover-community\" / \"mathlib\" +require \"leanprover-community\" / \"mathlib\" @ git {repr rev} @[default_target] lean_lib {libRoot} where -- add any library configuration options here " -def mathLaxTomlConfigFileContents (pkgName libRoot : String) := +def mathLaxTomlConfigFileContents (pkgName libRoot rev : String) := s!"name = {repr pkgName} version = \"0.1.0\" keywords = [\"math\"] @@ -157,12 +157,13 @@ pp.unicode.fun = true # pretty-prints `fun a ↦ b` [[require]] name = \"mathlib\" scope = \"leanprover-community\" +rev = {repr rev} [[lean_lib]] name = {repr libRoot} " -def mathLeanConfigFileContents (pkgName libRoot : String) := +def mathLeanConfigFileContents (pkgName libRoot rev : String) := s!"import Lake open Lake DSL @@ -176,14 +177,14 @@ package {repr pkgName} where ⟨`weak.linter.mathlibStandardSet, true⟩, ] -require \"leanprover-community\" / \"mathlib\" +require \"leanprover-community\" / \"mathlib\" @ git {repr rev} @[default_target] lean_lib {libRoot} where -- add any library configuration options here " -def mathTomlConfigFileContents (pkgName libRoot : String) := +def mathTomlConfigFileContents (pkgName libRoot rev : String) := s!"name = {repr pkgName} version = \"0.1.0\" keywords = [\"math\"] @@ -198,6 +199,7 @@ maxSynthPendingDepth = 3 [[require]] name = \"mathlib\" scope = \"leanprover-community\" +rev = {repr rev} [[lean_lib]] name = {repr libRoot} @@ -220,12 +222,6 @@ To set up your new GitHub repository, follow these steps: After following the steps above, you can remove this section from the README file. " -def mathToolchainBlobUrl : String := - "https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain" - -def mathToolchainUrl : String := - "https://github.com/leanprover-community/mathlib4/blob/master/lean-toolchain" - def leanActionWorkflowContents := "name: Lean Action CI @@ -363,8 +359,12 @@ def escapeName! : Name → String def dotlessName (name : Name) := name.toString false |>.map fun chr => if chr == '.' then '-' else chr -def InitTemplate.configFileContents (tmp : InitTemplate) (lang : ConfigLang) (pkgName : Name) (root : Name) : String := +def InitTemplate.configFileContents + (tmp : InitTemplate) (lang : ConfigLang) (pkgName : Name) (root : Name) + (leanVer? : Option LeanVer) +: String := let pkgNameStr := dotlessName pkgName + let mathRev := leanVer?.elim "master" (s!"v{·.toString}") match tmp, lang with | .std, .lean => stdLeanConfigFileContents pkgNameStr (escapeName! root) pkgNameStr.toLower | .std, .toml => stdTomlConfigFileContents pkgNameStr root.toString pkgNameStr.toLower @@ -372,10 +372,10 @@ def InitTemplate.configFileContents (tmp : InitTemplate) (lang : ConfigLang) (p | .lib, .toml => libTomlConfigFileContents pkgNameStr root.toString | .exe, .lean => exeLeanConfigFileContents pkgNameStr pkgNameStr.toLower | .exe, .toml => exeTomlConfigFileContents pkgNameStr pkgNameStr.toLower - | .mathLax, .lean => mathLaxLeanConfigFileContents pkgNameStr (escapeName! root) - | .mathLax, .toml => mathLaxTomlConfigFileContents pkgNameStr root.toString - | .math, .lean => mathLeanConfigFileContents pkgNameStr (escapeName! root) - | .math, .toml => mathTomlConfigFileContents pkgNameStr root.toString + | .mathLax, .lean => mathLaxLeanConfigFileContents pkgNameStr (escapeName! root) mathRev + | .mathLax, .toml => mathLaxTomlConfigFileContents pkgNameStr root.toString mathRev + | .math, .lean => mathLeanConfigFileContents pkgNameStr (escapeName! root) mathRev + | .math, .toml => mathTomlConfigFileContents pkgNameStr root.toString mathRev def createLeanActionWorkflow (dir : FilePath) (tmp : InitTemplate) : LogIO PUnit := do logVerbose "creating lean-action CI workflow" @@ -433,8 +433,13 @@ def initPkg else return (root, rootFile) + -- Compute the Lean version from the environment toolchain + let leanVer? := match ToolchainVer.ofString env.toolchain with + | .release ver => some ver + | _ => none + -- write template configuration file - IO.FS.writeFile configFile <| tmp.configFileContents lang name root + IO.FS.writeFile configFile <| tmp.configFileContents lang name root leanVer? -- write example code if the files do not already exist if let some rootFile := rootFile? then @@ -486,26 +491,21 @@ def initPkg [1]: https://github.com/leanprover/lean4/issues/2518 -/ let toolchainFile := dir / toolchainFileName - if !offline && (tmp matches .mathLax | .math) then - logInfo "downloading mathlib `lean-toolchain` file" - try - download mathToolchainBlobUrl toolchainFile - catch errPos => - logError s!"failed to download mathlib 'lean-toolchain' file; \ - you can manually copy it from:\n {mathToolchainUrl}" - throw errPos - -- Create a manifest file based on the dependencies. - updateManifest { lakeEnv := env, wsDir := dir } - else - if env.toolchain.isEmpty then + if env.toolchain.isEmpty then -- Empty githash implies dev build unless env.lean.githash.isEmpty do unless (← toolchainFile.pathExists) do - logWarning <| - "could not create a `lean-toolchain` file for the new package; " ++ - "no known toolchain name for the current Elan/Lean/Lake" + logWarning "could not create a `lean-toolchain` file for the new package; \ + no known toolchain name for the current Elan/Lean/Lake" else IO.FS.writeFile toolchainFile <| env.toolchain ++ "\n" + if tmp matches .mathLax | .math then + if leanVer?.isNone then + logWarning "creating a new math package with a non-release Lean toolchain; \ + Mathlib may not work properly" + unless offline do + -- Checkout mathlib and pin the version in the manifest + updateManifest { lakeEnv := env, wsDir := dir, updateToolchain := false } def validatePkgName (pkgName : String) : LogIO PUnit := do if pkgName.isEmpty || pkgName.all (· == '.') || pkgName.any (· ∈ ['/', '\\']) then diff --git a/tests/lake/tests/common.sh b/tests/lake/tests/common.sh index cf0a1eb060..982562aac5 100644 --- a/tests/lake/tests/common.sh +++ b/tests/lake/tests/common.sh @@ -1,5 +1,10 @@ set -euo pipefail +# Elan configuration + +ELAN=${ELAN:-elan} +echo "ELAN=$ELAN" + # Lake configuration LAKE=${LAKE:-lake} diff --git a/tests/lake/tests/init/.gitignore b/tests/lake/tests/init/.gitignore index f990b1f12f..30f8a8f277 100644 --- a/tests/lake/tests/init/.gitignore +++ b/tests/lake/tests/init/.gitignore @@ -7,4 +7,5 @@ /123-hello /A-B-C-D /meta +/qed-lax /qed diff --git a/tests/lake/tests/init/clean.sh b/tests/lake/tests/init/clean.sh index ad3b8be466..600dc0a6fb 100755 --- a/tests/lake/tests/init/clean.sh +++ b/tests/lake/tests/init/clean.sh @@ -8,5 +8,6 @@ rm -rf lean-data rm -rf 123-hello rm -rf A-B-C-D rm -rf meta +rm -rf qed-lax rm -rf qed rm -rf mathlib_standards diff --git a/tests/lake/tests/init/online-test.sh b/tests/lake/tests/init/online-test.sh new file mode 100755 index 0000000000..bf7501f514 --- /dev/null +++ b/tests/lake/tests/init/online-test.sh @@ -0,0 +1,31 @@ +#!/usr/bin/env bash +source ../common.sh + +./clean.sh + +# Ensure that Lake is run without a toolchain name +# (for consistent default behavior in tests) +export ELAN_TOOLCHAIN= + +# WARNING: This test of the `math` template will fail unless Mathlib and Lean +# are synchronized. + +# Test that Mathlib-standard packages have the expected strict linter options. +mkdir mathlib_standards +pushd mathlib_standards +test_run init mathlib_standards math + +# Run via elan to make sure the version of Lean is compatible with the version of Mathlib. + +# skip if no elan found +echo "# Check if elan exists" +if ! command -v $ELAN > /dev/null; then + echo "elan not found; skipping test" + exit 0 +fi + +# '#'-commands are not allowed only when enabling the Mathlib standard linters. +echo >MathlibStandards.lean "import Mathlib.Init" +echo >>MathlibStandards.lean "#guard true" +test_cmd_out 'note: this linter can be disabled with `set_option linter.hashCommand false`' $ELAN run $(cat lean-toolchain) lake build mathlib_standards +popd diff --git a/tests/lake/tests/init/test.sh b/tests/lake/tests/init/test.sh index 82680918f5..9908abc0f3 100755 --- a/tests/lake/tests/init/test.sh +++ b/tests/lake/tests/init/test.sh @@ -3,6 +3,10 @@ source ../common.sh ./clean.sh +# Ensure that Lake is run without a toolchain name +# (for consistent default behavior in tests) +export ELAN_TOOLCHAIN= + # Test `new` and `init` with bad template/language (should error) echo "# TEST: Template validation" @@ -64,22 +68,30 @@ test_run -d hello build Hello test -f hello/.lake/build/lib/lean/Hello.olean rm -rf hello -# Test math-lax template +# Test math & math-lax template -echo "# TEST: math-lax template" -# Use `--offline` and remove the `require`, -# since we do not wish to download mathlib during tests -test_run new qed math-lax.lean --offline -sed_i '/^require.*/{N;d;}' qed/lakefile.lean -test_run -d qed build Qed -test -f qed/.lake/build/lib/lean/Qed.olean -rm -rf qed -# Use `--offline` and remove the `require`, -# since we do not wish to download mathlib during tests -test_run new qed math-lax.toml --offline -sed_i '/^\[\[require\]\]/{N;N;N;d;}' qed/lakefile.toml -test_run -d qed build Qed -test -f qed/.lake/build/lib/lean/Qed.olean +test_math_tmp () { + tmp=$1; pkg=$2; mod=$3 + echo "# TEST: $tmp template" + # Use `--offline` and remove the `require`, + # since we do not wish to download mathlib during tests + ELAN_TOOLCHAIN="v4.0.0-test" test_run new $pkg $tmp.lean --offline + sed_i '/^require.*/{N;d;}' $pkg/lakefile.lean + test_cmd_out "v4.0.0-test" cat $pkg/lean-toolchain + test_run -d $pkg build $mod + test -f $pkg/.lake/build/lib/lean/$mod.olean + rm -rf $pkg + # Use `--offline` and remove the `require`, + # since we do not wish to download mathlib during tests + test_out "creating a new math package with a non-release Lean toolchain" \ + new $pkg $tmp.toml --offline + sed_i '/^\[\[require\]\]/{N;N;N;d;}' $pkg/lakefile.toml + test_run -d $pkg build $mod + test -f $pkg/.lake/build/lib/lean/$mod.olean +} + +test_math_tmp math-lax qed-lax QedLax +test_math_tmp math qed Qed # Test `init .` @@ -152,33 +164,5 @@ popd echo "# TEST: init existing" test_err "package already initialized" -d hello_world init -# Tests of the `math` template are usually disabled as they fail unless Mathlib -# and Lean are synchronized. However, it remains here as it useful when testing -# changes to the template. -if false; then - -# Test that Mathlib-standard packages have the expected strict linter options. -mkdir mathlib_standards -pushd mathlib_standards -test_run init mathlib_standards math - -# Run via elan to make sure the version of Lean is compatible with the version of Mathlib. -ELAN=${ELAN:-elan} - -# skip if no elan found -echo "# Check if elan exists" -if ! command -v $ELAN > /dev/null; then - echo "elan not found; skipping test" - exit 0 -fi - -# '#'-commands are not allowed only when enabling the Mathlib standard linters. -echo >MathlibStandards.lean "import Mathlib.Init" -echo >>MathlibStandards.lean "#guard true" -test_cmd_out 'note: this linter can be disabled with `set_option linter.hashCommand false`' $ELAN run $(cat lean-toolchain) lake build mathlib_standards -popd - -fi - # Cleanup rm -f produced.out diff --git a/tests/lake/tests/toolchain/test.sh b/tests/lake/tests/toolchain/test.sh index 4225309355..c347d2011f 100755 --- a/tests/lake/tests/toolchain/test.sh +++ b/tests/lake/tests/toolchain/test.sh @@ -3,8 +3,6 @@ source ../common.sh # Tests which require Elan to download a toolchain -ELAN=${ELAN:-elan} - # skip if no elan found echo "# Check if elan exists" if ! command -v $ELAN > /dev/null; then