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 <pkg> 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

@@ -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

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}

tests/lake/tests/init/.gitignore

@@ -7,4 +7,5 @@
 /123-hello
 /A-B-C-D
 /meta
+/qed-lax
 /qed

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

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

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

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