From 87e68396e965f3d99e9c88374576093bb5b90d67 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Mon, 20 Nov 2023 15:43:35 -0500
Subject: [PATCH 1/2] test: lake: verify math template

---
 src/lake/tests/init/.gitignore |  1 +
 src/lake/tests/init/clean.sh   |  1 +
 src/lake/tests/init/test.sh    | 14 ++++++++++++++
 3 files changed, 16 insertions(+)

diff --git a/src/lake/tests/init/.gitignore b/src/lake/tests/init/.gitignore
index d42950317c13..5ca6f1be54ce 100644
--- a/src/lake/tests/init/.gitignore
+++ b/src/lake/tests/init/.gitignore
@@ -5,3 +5,4 @@
 /lean-data
 /123-hello
 /meta
+/qed
diff --git a/src/lake/tests/init/clean.sh b/src/lake/tests/init/clean.sh
index 914fe91cfd56..81c26bac0ce6 100755
--- a/src/lake/tests/init/clean.sh
+++ b/src/lake/tests/init/clean.sh
@@ -5,3 +5,4 @@ rm -rf hello_world
 rm -rf lean-data
 rm -rf 123-hello
 rm -rf meta
+rm -rf qed
diff --git a/src/lake/tests/init/test.sh b/src/lake/tests/init/test.sh
index 9980137c5a03..cf382a1f738d 100755
--- a/src/lake/tests/init/test.sh
+++ b/src/lake/tests/init/test.sh
@@ -3,6 +3,12 @@ set -euxo pipefail
 
 ./clean.sh
 
+if [ "`uname`" = Darwin ]; then
+  sed_i() { sed -i '' "$@"; }
+else
+  sed_i() { sed -i "$@"; }
+fi
+
 LAKE1=${LAKE:-../../../.lake/build/bin/lake}
 LAKE=${LAKE:-../../.lake/build/bin/lake}
 
@@ -34,6 +40,14 @@ $LAKE1 build
 .lake/build/bin/hello
 popd
 
+# Test math template
+
+$LAKE new qed math
+# Remove the require, since we do not wish to download mathlib during tests
+sed_i '/^require.*/{N;d;}' qed/lakefile.lean
+$LAKE -d qed build Qed
+test -f qed/.lake/build/lib/Qed.olean
+
 # Test creating packages with uppercase names
 # https://github.com/leanprover/lean4/issues/2540
 

From cafd0a4ec1c17329705aa9b2925388579102e56f Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Mon, 20 Nov 2023 15:52:51 -0500
Subject: [PATCH 2/2] refactor: lake: simplify math template

---
 src/lake/Lake/CLI/Init.lean | 24 ++++++------------------
 1 file changed, 6 insertions(+), 18 deletions(-)

diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean
index 057638f3ec6b..c4c00a55d7db 100644
--- a/src/lake/Lake/CLI/Init.lean
+++ b/src/lake/Lake/CLI/Init.lean
@@ -93,31 +93,19 @@ def mathConfigFileContents (pkgName libRoot : String) :=
 s!"import Lake
 open Lake DSL
 
-def leanOptions : Array LeanOption := #[
-  ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
-  ⟨`pp.proofs.withType, false⟩
-]
-
--- These are additional settings which do not affect the lake hash,
--- so they can be enabled in CI and disabled locally or vice versa.
--- Warning: Do not put any options here that actually change the olean files,
--- or inconsistent behavior may result
-def weakLeanArgs : Array String :=
-  if get_config? CI |>.isSome then
-    #[\"-DwarningAsError=true\"]
-  else
-    #[]
-
 package {pkgName} where
-  leanOptions := leanOptions
-  -- add any package configuration options here
+  -- Settings applied to both builds and interactive editing
+  leanOptions := #[
+    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
+    ⟨`pp.proofs.withType, false⟩
+  ]
+  -- add any additional package configuration options here
 
 require mathlib from git
   \"https://github.com/leanprover-community/mathlib4.git\"
 
 @[default_target]
 lean_lib {libRoot} where
-  weakLeanArgs := weakLeanArgs
   -- add any library configuration options here
 "