summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--lakefile.lean9
-rw-r--r--lean-toolchain2
2 files changed, 2 insertions, 9 deletions
diff --git a/lakefile.lean b/lakefile.lean
index f92b653..ccc0a55 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -7,13 +7,6 @@ require base from git
package «AvlVerification» where
-- add package configuration options here
+@[default_target]
lean_lib «AvlVerification» where
-- add library configuration options here
-
-@[default_target]
-lean_exe «avlverification» where
- root := `Main
- -- Enables the use of the Lean interpreter by the executable (e.g.,
- -- `runFrontend`) at the expense of increased binary size on Linux.
- -- Remove this line if you do not need such functionality.
- supportInterpreter := true
diff --git a/lean-toolchain b/lean-toolchain
index cfcdd32..9ad3040 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.6.0-rc1
+leanprover/lean4:v4.7.0