fix: lake: test script bugs w/ Mathlib & non-Linux (#9397)

This PR fixes some issues with the Lake tests on Windows and macOS. It
also avoids downloading Mathlib in the `init` test, which was currently
doing this after changes to the `math-lax` template in #8866.

To skip the Mathlib download in `init`, an undocumented `--offline`
option was added`. This option is currently meant for internal use only.

src/lake/Lake/CLI/Init.lean

@@ -409,7 +409,10 @@ def createLeanActionWorkflow (dir : FilePath) (tmp : InitTemplate) : LogIO PUnit
     logVerbose s!"created create-release CI workflow at '{workflowFile}'"
 
 /-- Initialize a new Lake package in the given directory with the given name. -/
-def initPkg (dir : FilePath) (name : Name) (tmp : InitTemplate) (lang : ConfigLang) (env : Lake.Env) : LoggerIO PUnit := do
+def initPkg
+  (dir : FilePath) (name : Name) (tmp : InitTemplate) (lang : ConfigLang)
+  (env : Lake.Env) (offline := false)
+: LoggerIO PUnit := do
   let configFile :=  dir / defaultConfigFile.addExtension lang.fileExtension
   if (← configFile.pathExists) then
     error "package already initialized"
@@ -483,7 +486,7 @@ def initPkg (dir : FilePath) (name : Name) (tmp : InitTemplate) (lang : ConfigLa
   [1]: https://github.com/leanprover/lean4/issues/2518
   -/
   let toolchainFile := dir / toolchainFileName
-  if tmp = .mathLax || tmp = .math then
+  if !offline && (tmp matches .mathLax | .math) then
     logInfo "downloading mathlib `lean-toolchain` file"
     try
       download mathToolchainBlobUrl toolchainFile
@@ -491,6 +494,8 @@ def initPkg (dir : FilePath) (name : Name) (tmp : InitTemplate) (lang : ConfigLa
       logError "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
       -- Empty githash implies dev build
@@ -502,17 +507,16 @@ def initPkg (dir : FilePath) (name : Name) (tmp : InitTemplate) (lang : ConfigLa
     else
       IO.FS.writeFile toolchainFile <| env.toolchain ++ "\n"
 
-  -- Create a manifest file based on the dependencies.
-  if tmp = .mathLax || tmp = .math then
-    updateManifest { lakeEnv := env, wsDir := dir }
-
 def validatePkgName (pkgName : String) : LogIO PUnit := do
   if pkgName.isEmpty || pkgName.all (· == '.') || pkgName.any (· ∈ ['/', '\\']) then
     error s!"illegal package name '{pkgName}'"
   if pkgName.toLower ∈ ["init", "lean", "lake", "main"] then
     error "reserved package name"
 
-def init (name : String) (tmp : InitTemplate) (lang : ConfigLang) (env : Lake.Env) (cwd : FilePath := ".") : LoggerIO PUnit := do
+def init
+  (name : String) (tmp : InitTemplate) (lang : ConfigLang)
+  (env : Lake.Env) (cwd : FilePath := ".") (offline := false)
+: LoggerIO PUnit := do
   let name ← id do
     if name == "." then
       let path ← IO.FS.realPath cwd
@@ -524,13 +528,16 @@ def init (name : String) (tmp : InitTemplate) (lang : ConfigLang) (env : Lake.En
   let name := name.trim
   validatePkgName name
   IO.FS.createDirAll cwd
-  initPkg cwd (stringToLegalOrSimpleName name) tmp lang env
+  initPkg cwd (stringToLegalOrSimpleName name) tmp lang env offline
 
-def new (name : String) (tmp : InitTemplate) (lang : ConfigLang)  (env : Lake.Env) (cwd : FilePath := ".") : LoggerIO PUnit := do
+def new
+  (name : String) (tmp : InitTemplate) (lang : ConfigLang)
+  (env : Lake.Env) (cwd : FilePath := ".") (offline := false)
+: LoggerIO PUnit := do
   let name := name.trim
   validatePkgName name
   let name := stringToLegalOrSimpleName name
   let dirName := dotlessName name
   let dir := cwd / dirName
   IO.FS.createDirAll dir
-  initPkg dir name tmp lang env
+  initPkg dir name tmp lang env offline

src/lake/Lake/CLI/Main.lean

@@ -48,6 +48,7 @@ structure LakeOptions where
   outLv? : Option LogLevel := .none
   ansiMode : AnsiMode := .auto
   outFormat : OutFormat := .text
+  offline : Bool := false
 
 def LakeOptions.outLv (opts : LakeOptions) : LogLevel :=
   opts.outLv?.getD opts.verbosity.minLogLv
@@ -195,6 +196,7 @@ def lakeLongOption : (opt : String) → CliM PUnit
 | "--no-cache"    => modifyThe LakeOptions ({· with noCache := true})
 | "--try-cache"   => modifyThe LakeOptions ({· with noCache := false})
 | "--rehash"      => modifyThe LakeOptions ({· with trustHash := false})
+| "--offline"     => modifyThe LakeOptions ({· with offline := true})
 | "--wfail"       => modifyThe LakeOptions ({· with failLv := .warning})
 | "--iofail"      => modifyThe LakeOptions ({· with failLv := .info})
 | "--log-level"   => do
@@ -340,14 +342,14 @@ protected def new : CliM PUnit := do
   let opts ← getThe LakeOptions
   let name ← takeArg "package name"
   let (tmp, lang) ← parseTemplateLangSpec <| ← takeArgD ""
-  noArgsRem do new name tmp lang (← opts.computeEnv) opts.rootDir
+  noArgsRem do new name tmp lang (← opts.computeEnv) opts.rootDir opts.offline
 
 protected def init : CliM PUnit := do
   processOptions lakeOption
   let opts ← getThe LakeOptions
   let name := ← takeArgD "."
   let (tmp, lang) ← parseTemplateLangSpec <| ← takeArgD ""
-  noArgsRem do init name tmp lang (← opts.computeEnv) opts.rootDir
+  noArgsRem do init name tmp lang (← opts.computeEnv) opts.rootDir opts.offline
 
 protected def build : CliM PUnit := do
   processOptions lakeOption

src/lake/tests/cache/test.sh

@@ -52,7 +52,7 @@ cp "$CACHE_DIR/inputs/test.jsonl" .lake/backup-inputs.json
 # and equivalent to the standard artifact
 local_art="$(LAKE_CACHE_DIR= $LAKE query +Test:o)"
 cache_art="$(LAKE_CACHE_DIR="$CACHE_DIR" $LAKE query +Test:o)"
-test_exp "$(dirname -- "$cache_art")" = "$CACHE_DIR/artifacts"
+test_exp "$(norm_dirname "$cache_art")" = "$CACHE_DIR/artifacts"
 test_exp "$cache_art" != "$local_art"
 test_cmd cmp -s "$cache_art" "$local_art"
 
@@ -62,7 +62,7 @@ test_cached() {
   target="$1"; shift
   art="$(LAKE_CACHE_DIR="$CACHE_DIR" $LAKE query $target)"
   echo "${1:-?} artifact cached: $target -> $art"
-  test ${1:-} "$(dirname -- "$art")" = "$CACHE_DIR/artifacts"
+  test ${1:-} "$(norm_dirname "$art")" = "$CACHE_DIR/artifacts"
 }
 test_cached test:exe
 test_cached Test:static

src/lake/tests/common.sh

@@ -13,7 +13,7 @@ echo "OS=$OS"
 UNAME="`uname`"
 echo "UNAME=$UNAME"
 
-if [ "${OS:-}" = Windows_NT ]; then
+if [ "$OS" = Windows_NT ]; then
 LIB_PREFIX=
 SHARED_LIB_EXT=dll
 elif [ "$UNAME" = Darwin ]; then
@@ -32,6 +32,12 @@ else
   TAIL=tail
 fi
 
+if [ "$OS" = Windows_NT ]; then
+  norm_dirname() { cygpath -u "$(dirname -- "$1")";  }
+else
+  norm_dirname() { dirname -- "$1"; }
+fi
+
 # Test functions
 
 test_cmd() {
@@ -209,7 +215,7 @@ test_maybe_err() {
   match_text "$expected" produced.out
 }
 
-check_diff() {
+check_diff_core() {
   expected=$1; actual=$2
   if diff -u --strip-trailing-cr "$expected" "$actual"; then
     cat "$actual"
@@ -220,11 +226,18 @@ check_diff() {
   fi
 }
 
+check_diff() {
+  expected=$1; actual=$2
+  cat "$actual" > produced.out
+  check_diff_core "$expected" produced.out
+}
+
 test_out_diff() {
   expected=$1; shift
+  cat "$expected" > produced.expected.out
   echo '$' lake "$@"
   if "$LAKE" "$@" >produced.out 2>&1; then rc=$?; else rc=$?; fi
-  if check_diff "$expected" produced.out; then
+  if check_diff_core produced.expected.out produced.out; then
     if [ $rc != 0 ]; then
       echo "FAILURE: Program exited with code $rc"
       return 1
@@ -239,9 +252,10 @@ test_out_diff() {
 
 test_err_diff() {
   expected=$1; shift
+  cat "$expected" > produced.expected.out
   echo '$' lake "$@"
   if "$LAKE" "$@" >produced.out 2>&1; then rc=$?; else rc=$?; fi
-  if check_diff "$expected" produced.out; then
+  if check_diff_core produced.expected.out produced.out; then
     if [ $rc != 1 ]; then
       echo "FAILURE: Lake unexpectedly succeeded"
       return 1

src/lake/tests/env/test.sh

@@ -28,7 +28,8 @@ test_out "hello" -d ../../examples/hello env printenv PATH
 # Test other variables are set
 test_eq "false" env printenv LAKE_NO_CACHE
 test_eq "false" env printenv LAKE_ARTIFACT_CACHE
-test_run env printenv LAKE_CACHE_DIR
+# No cache directory is available in Windows CI (i.e., Windows Server)
+# test_run env printenv LAKE_CACHE_DIR
 
 # Test that `env` preserves the input environment for certain variables
 echo "# TEST: Setting variables for lake env"

src/lake/tests/init/test.sh

@@ -67,14 +67,16 @@ rm -rf hello
 # Test math-lax template
 
 echo "# TEST: math-lax template"
-test_run new qed math-lax.lean || true # ignore toolchain download errors
-# Remove the require, since we do not wish to download mathlib during tests
+# 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
-test_run new qed math-lax.toml || true # ignore toolchain download errors
-# Remove the require, since we do not wish to download mathlib during tests
+# 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

src/lake/tests/inputFile/clean.sh

@@ -1,2 +1,2 @@
-rm -rf .lake lake-manifest.json produced.out
-rm -rf inputs lakefile.produced.lean lakefileAlt.produced.toml
+rm -rf .lake lake-manifest.json inputs
+rm -f *produced*

src/lake/tests/inputFile/test.sh

@@ -66,4 +66,4 @@ EOF
 ) -q exe test
 
 # Cleanup
-rm -f produced.out
+rm -f produced*

src/lake/tests/noRelease/clean.sh

@@ -1 +1,2 @@
-rm -rf produced.out .lake lake-manifest.json dep/.lake dep/.git
+rm -f produced*
+rm -rf .lake lake-manifest.json dep/.lake dep/.git

src/lake/tests/noRelease/test.sh

@@ -94,4 +94,4 @@ test_run build dep:release
 
 # Cleanup
 rm -rf dep/.git
-rm -f prdouced.out
+rm -f produced*

src/lake/tests/reservoirConfig/clean.sh

@@ -1 +1,2 @@
-rm -rf .lake lake-manifest.json .git produced.out
+rm -f produced*
+rm -rf .lake lake-manifest.json .git

src/lake/tests/reservoirConfig/test.sh

@@ -26,4 +26,4 @@ test_out_diff expected.json reservoir-config
 
 # Cleanup
 rm -rf .git
-rm -f produced.out
+rm -f produced*

src/lake/tests/versionTags/clean.sh

@@ -1 +1,2 @@
-rm -rf .lake lake-manifest.json .git produced.out
+rm -rf .lake lake-manifest.json .git
+rm -f produced*

src/lake/tests/versionTags/test.sh

@@ -31,5 +31,5 @@ EOF
 ) version-tags
 
 # Cleanup
-rm -f produced.out
+rm -f produced*
 rm -rf .git