From c1da28af468d07e256147c7fbdc47b798c154458 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 7 Jun 2024 10:38:39 +1000 Subject: [PATCH 1/2] chore: switch to lakefile.toml --- lakefile.lean | 17 ----------------- 1 file changed, 17 deletions(-) delete mode 100644 lakefile.lean diff --git a/lakefile.lean b/lakefile.lean deleted file mode 100644 index ac5a06f..0000000 --- a/lakefile.lean +++ /dev/null @@ -1,17 +0,0 @@ -import Lake -open Lake DSL - -package «lean4checker» where - - @[default_target] -lean_lib «Lean4Checker» where - globs := #[.andSubmodules `Lean4Checker] - -@[default_target] -lean_exe «lean4checker» where - root := `Main - supportInterpreter := true - -@[default_target] -lean_lib «Lean4CheckerTests» where - globs := #[.andSubmodules `Lean4CheckerTests] From 5fa7a50e0f939c01bbd9c9cdc0647cc11b112650 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 7 Jun 2024 10:38:44 +1000 Subject: [PATCH 2/2] chore: switch to lakefile.toml --- lakefile.toml | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 lakefile.toml diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..91ecb6b --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,15 @@ +name = "lean4checker" +defaultTargets = ["Lean4Checker", "lean4checker", "Lean4CheckerTests"] + +[[lean_lib]] +name = "Lean4Checker" +globs = ["Lean4Checker.*"] + +[[lean_lib]] +name = "Lean4CheckerTests" +globs = ["Lean4CheckerTests.*"] + +[[lean_exe]] +name = "lean4checker" +root = "Main" +supportInterpreter = true