chore: bump Lean to v4.8.0

tydeu · Jun 19, 2024 · d93e059 · d93e059
1 parent 8da8169
commit d93e059
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 3 deletions.
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.8.0-rc1
+leanprover/lean4:v4.8.0
diff --git a/tests/envIncludePath.lean b/tests/envIncludePath.lean
@@ -1,7 +1,8 @@
 import Alloy.C
 open scoped Alloy.C
 
-#eval Alloy.C.modifyLocalServerConfig (·.addFlag "--language=c")
+run_cmd Lean.Elab.Command.liftCoreM <|
+  Alloy.C.modifyLocalServerConfig (·.addFlag "--language=c")
 
 set_option Alloy.shimDiagnostics.serverOnly false in
 alloy c include "includePath.h"
diff --git a/tests/run/includePath.lean b/tests/run/includePath.lean
@@ -2,7 +2,7 @@ import Alloy.C
 open Alloy.C
 
 open Lean Elab Command in
-#eval show CommandElabM _ from do
+run_cmd
   let leanFile ← IO.FS.realPath <| System.FilePath.mk (← getFileName)
   let includeDir := leanFile.parent.bind (·.parent) |>.get!
   logInfo includeDir.toString
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:4.8.0-rc1
		leanprover/lean4:v4.8.0