From 162428159e934cb497b1573d9486a362e222736a Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sat, 21 Dec 2024 02:06:48 -0600 Subject: [PATCH] fix: parser 'subscript' not found Use `enableInitializersExecution` so that `checkdecls` doesn't fail on any project that imports a file with subscript/superscript notation. --- Main.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Main.lean b/Main.lean index ab943ec..ceab749 100644 --- a/Main.lean +++ b/Main.lean @@ -1,7 +1,7 @@ import Lake.CLI.Main open Lake Lean -def main (args : List String) : IO UInt32 := do +unsafe def main (args : List String) : IO UInt32 := do unless args.length == 1 do println! "This command takes exactly one argument: the path to a file containing a list of declarations to check." return 1 @@ -15,6 +15,8 @@ def main (args : List String) : IO UInt32 := do log.replay (logger := .stderr) let some ws := ws? | return 1 let imports := ws.root.leanLibs.flatMap (·.config.roots.map fun module => { module }) + -- see comments in https://github.com/leanprover/lean4/pull/6325 + enableInitializersExecution let env ← Lean.importModules imports {} let mut ok := true for line in ← IO.FS.lines filename do