Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

refactor: lake: simplify math template & test it #2930

Merged
merged 2 commits into from
Nov 27, 2023
Merged

refactor: lake: simplify math template & test it #2930

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
87e6839
test: lake: verify math template
tydeu Nov 20, 2023
cafd0a4
refactor: lake: simplify math template
tydeu Nov 20, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 6 additions & 18 deletions src/lake/Lake/CLI/Init.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
"

Expand Down
1 change: 1 addition & 0 deletions src/lake/tests/init/.gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,3 +5,4 @@
/lean-data
/123-hello
/meta
/qed
1 change: 1 addition & 0 deletions src/lake/tests/init/clean.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,3 +5,4 @@ rm -rf hello_world
rm -rf lean-data
rm -rf 123-hello
rm -rf meta
rm -rf qed
14 changes: 14 additions & 0 deletions src/lake/tests/init/test.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}

Expand Down Expand Up @@ -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

Expand Down
Loading