Bump Lean version to 4.1.0 #17
|
@ -1,5 +1,6 @@
|
||||||
.*
|
.*
|
||||||
!.gitignore
|
!.gitignore
|
||||||
|
|
||||||
|
*.olean
|
||||||
/build
|
/build
|
||||||
/lake-packages
|
/lake-packages
|
||||||
|
|
|
@ -88,7 +88,7 @@ unsafe def main (args: List String): IO Unit := do
|
||||||
let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
|
let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
|
||||||
|
|
||||||
let env ← Lean.importModules
|
let env ← Lean.importModules
|
||||||
(imports := imports.map (λ str => { module := str_to_name str, runtimeOnly := false }))
|
(imports := imports.toArray.map (λ str => { module := str_to_name str, runtimeOnly := false }))
|
||||||
(opts := {})
|
(opts := {})
|
||||||
(trustLevel := 1)
|
(trustLevel := 1)
|
||||||
let context: Context := {
|
let context: Context := {
|
||||||
|
|
|
@ -1 +1 @@
|
||||||
leanprover/lean4:4.0.0
|
leanprover/lean4:4.1.0
|
||||||
|
|
Loading…
Reference in New Issue