From e71a489011b91acd47f2d7865a55c21a0018ab4f Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 14 Oct 2024 11:17:42 +1100 Subject: [PATCH 1/6] feat: allow checking just the current project --- Main.lean | 83 ++++++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 60 insertions(+), 23 deletions(-) diff --git a/Main.lean b/Main.lean index d44ad9f..c30d998 100644 --- a/Main.lean +++ b/Main.lean @@ -6,6 +6,7 @@ Authors: Scott Morrison import Lean.CoreM import Lean.Replay import Lean4Checker.Lean +import Lake.Load.Manifest open Lean @@ -28,38 +29,74 @@ unsafe def replayFromFresh (module : Name) : IO Unit := do Lean.withImportModules #[{module}] {} 0 fun env => do discard <| (← mkEmptyEnvironment).replay env.constants.map₁ +/-- Read the name of the main module from the `lake-manifest`. -/ +-- This has been copied from `ImportGraph.getCurrentModule` in the +-- https://github.com/leanprover-community/import-graph repository. +def getCurrentModule : IO Name := do + match (← Lake.Manifest.load? ⟨"lake-manifest.json"⟩) with + | none => + -- TODO: should this be caught? + pure .anonymous + | some manifest => + -- TODO: This assumes that the `package` and the default `lean_lib` + -- have the same name up to capitalisation. + -- Would be better to read the `.defaultTargets` from the + -- `← getRootPackage` from `Lake`, but I can't make that work with the monads involved. + return manifest.name.capitalize + + /-- -Run as e.g. `lake exe lean4checker` to check everything on the Lean search path, -or `lake exe lean4checker Mathlib.Data.Nat.Basic` to check a single file. +Run as e.g. `lake exe lean4checker` to check everything in the current project. +or e.g. `lake exe lean4checker Mathlib.Data.Nat` to check everything with module name +starting with `Mathlib.Data.Nat`. This will replay all the new declarations from the target file into the `Environment` as it was at the beginning of the file, using the kernel to check them. You can also use `lake exe lean4checker --fresh Mathlib.Data.Nat.Basic` to replay all the constants -(both imported and defined in that file) into a fresh environment. +(both imported and defined in that file) into a fresh environment, +but this can only be used on a single file. This is not an external verifier, simply a tool to detect "environment hacking". -/ unsafe def main (args : List String) : IO UInt32 := do initSearchPath (← findSysroot) - let (flags, args) := args.partition fun s => s.startsWith "--" - match flags, args with - | flags, [mod] => match mod.toName with - | .anonymous => throw <| IO.userError s!"Could not resolve module: {mod}" - | m => - if "--fresh" ∈ flags then - replayFromFresh m - else - replayFromImports m - | [], _ => do - let sp ← searchPathRef.get - let mut tasks := #[] - for path in (← SearchPath.findAllWithExt sp "olean") do - if let some m := (← searchModuleNameOfFileName path sp) then - tasks := tasks.push (m, ← IO.asTask (replayFromImports m)) - for (m, t) in tasks do - if let .error e := t.get then - IO.eprintln s!"lean4checker found a problem in {m}" - throw e - | _, _ => throw <| IO.userError "--fresh flag is only valid when specifying a single module" + let (flags, args) := args.partition fun s => s.startsWith "-" + let targets ← do + match args with + | [] => pure [← getCurrentModule] + | args => args.mapM fun arg => do + let mod := arg.toName + if mod.isAnonymous then + throw <| IO.userError s!"Could not resolve module: {arg}" + else + pure mod + let mut targetModules := #[] + for target in targets do + let mut found := false + let sp ← searchPathRef.get + for path in (← SearchPath.findAllWithExt sp "olean") do + if let some m := (← searchModuleNameOfFileName path sp) then + if target.isPrefixOf m then + targetModules := targetModules.push m + found := true + if not found then + throw <| IO.userError s!"Could not find any oleans for: {target}" + if "--fresh" ∈ flags then + if targetModules.size != 1 then + throw <| IO.userError "--fresh flag is only valid when specifying a single module" + for m in targetModules do + if "-v" ∈ flags || "--verbose" ∈ flags then + IO.println s!"replaying {m} with --fresh" + replayFromFresh m + else + let mut tasks := #[] + for m in targetModules do + tasks := tasks.push (m, ← IO.asTask (replayFromImports m)) + for (m, t) in tasks do + if "-v" ∈ flags || "--verbose" ∈ flags then + IO.println s!"replaying {m}" + if let .error e := t.get then + IO.eprintln s!"lean4checker found a problem in {m}" + throw e return 0 From bf227216b86d6213c7332cbd16c08f4f2eb19c55 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 14 Oct 2024 11:21:32 +1100 Subject: [PATCH 2/6] fix tests --- test.sh | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/test.sh b/test.sh index 0629d35..46a2d95 100755 --- a/test.sh +++ b/test.sh @@ -23,19 +23,22 @@ check_command() { fi } -check_command "lake -q exe lean4checker Lean4CheckerTests.AddFalse" "uncaught exception: (kernel) declaration type mismatch, 'false' has type +check_command "lake -q exe lean4checker Lean4CheckerTests.AddFalse" "lean4checker found a problem in Lean4CheckerTests.AddFalse +uncaught exception: (kernel) declaration type mismatch, 'false' has type Prop but it is expected to have type False" -check_command "lake -q exe lean4checker Lean4CheckerTests.AddFalseConstructor" "uncaught exception: No such constructor False.intro" +check_command "lake -q exe lean4checker Lean4CheckerTests.AddFalseConstructor" "lean4checker found a problem in Lean4CheckerTests.AddFalseConstructor +uncaught exception: No such constructor False.intro" check_command "lake -q exe lean4checker --fresh Lean4CheckerTests.UseFalseConstructor" "uncaught exception: (kernel) unknown constant 'False.intro'" # The 'ReduceBool' test writes to a temporary file. # We clean up before and afterwards for consistency, although neither should be required. rm -f .lean4checker.tmp -check_command "lake -q exe lean4checker Lean4CheckerTests.ReduceBool" "uncaught exception: (kernel) unknown declaration 'foo'" +check_command "lake -q exe lean4checker Lean4CheckerTests.ReduceBool" "lean4checker found a problem in Lean4CheckerTests.ReduceBool +uncaught exception: (kernel) unknown declaration 'foo'" rm -f .lean4checker.tmp echo "All commands produced the expected errors." From 74a282a4a4ecbadb438ab6c4311bc237225537a2 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 14 Oct 2024 11:26:01 +1100 Subject: [PATCH 3/6] sigh --- Main.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Main.lean b/Main.lean index c30d998..f6a5524 100644 --- a/Main.lean +++ b/Main.lean @@ -77,7 +77,9 @@ unsafe def main (args : List String) : IO UInt32 := do let sp ← searchPathRef.get for path in (← SearchPath.findAllWithExt sp "olean") do if let some m := (← searchModuleNameOfFileName path sp) then + IO.println s!"considering {m}" if target.isPrefixOf m then + IO.println s!"adding {m}" targetModules := targetModules.push m found := true if not found then From e65f526aead625d4b65f40693816ad1779dd2e71 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 14 Oct 2024 11:31:49 +1100 Subject: [PATCH 4/6] sigh --- Main.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Main.lean b/Main.lean index f6a5524..90767c9 100644 --- a/Main.lean +++ b/Main.lean @@ -62,6 +62,7 @@ This is not an external verifier, simply a tool to detect "environment hacking". unsafe def main (args : List String) : IO UInt32 := do initSearchPath (← findSysroot) let (flags, args) := args.partition fun s => s.startsWith "-" + let verbose := "-v" ∈ flags || "--verbose" ∈ flags let targets ← do match args with | [] => pure [← getCurrentModule] @@ -88,16 +89,15 @@ unsafe def main (args : List String) : IO UInt32 := do if targetModules.size != 1 then throw <| IO.userError "--fresh flag is only valid when specifying a single module" for m in targetModules do - if "-v" ∈ flags || "--verbose" ∈ flags then - IO.println s!"replaying {m} with --fresh" + if verbose then IO.println s!"replaying {m} with --fresh" replayFromFresh m else let mut tasks := #[] for m in targetModules do + if verbose then IO.println s!"starting {m}" tasks := tasks.push (m, ← IO.asTask (replayFromImports m)) for (m, t) in tasks do - if "-v" ∈ flags || "--verbose" ∈ flags then - IO.println s!"replaying {m}" + if verbose then IO.println s!"replaying {m}" if let .error e := t.get then IO.eprintln s!"lean4checker found a problem in {m}" throw e From 835bde01bd81b82bd734bdc67e52b04f61fd01ae Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 14 Oct 2024 11:33:01 +1100 Subject: [PATCH 5/6] sigh --- Main.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Main.lean b/Main.lean index 90767c9..b39c90e 100644 --- a/Main.lean +++ b/Main.lean @@ -96,6 +96,7 @@ unsafe def main (args : List String) : IO UInt32 := do for m in targetModules do if verbose then IO.println s!"starting {m}" tasks := tasks.push (m, ← IO.asTask (replayFromImports m)) + IO.println s!"waiting for {tasks.size} tasks" for (m, t) in tasks do if verbose then IO.println s!"replaying {m}" if let .error e := t.get then From 7bef601f53806942c70bec98bd9199d6cc9762d8 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 14 Oct 2024 11:56:21 +1100 Subject: [PATCH 6/6] cleanup --- Main.lean | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/Main.lean b/Main.lean index b39c90e..d210502 100644 --- a/Main.lean +++ b/Main.lean @@ -53,9 +53,9 @@ starting with `Mathlib.Data.Nat`. This will replay all the new declarations from the target file into the `Environment` as it was at the beginning of the file, using the kernel to check them. -You can also use `lake exe lean4checker --fresh Mathlib.Data.Nat.Basic` to replay all the constants -(both imported and defined in that file) into a fresh environment, -but this can only be used on a single file. +You can also use `lake exe lean4checker --fresh Mathlib.Data.Nat.Prime.Basic` +to replay all the constants (both imported and defined in that file) into a fresh environment. +This can only be used on a single file. This is not an external verifier, simply a tool to detect "environment hacking". -/ @@ -73,14 +73,12 @@ unsafe def main (args : List String) : IO UInt32 := do else pure mod let mut targetModules := #[] + let sp ← searchPathRef.get for target in targets do let mut found := false - let sp ← searchPathRef.get for path in (← SearchPath.findAllWithExt sp "olean") do if let some m := (← searchModuleNameOfFileName path sp) then - IO.println s!"considering {m}" if target.isPrefixOf m then - IO.println s!"adding {m}" targetModules := targetModules.push m found := true if not found then @@ -94,9 +92,7 @@ unsafe def main (args : List String) : IO UInt32 := do else let mut tasks := #[] for m in targetModules do - if verbose then IO.println s!"starting {m}" tasks := tasks.push (m, ← IO.asTask (replayFromImports m)) - IO.println s!"waiting for {tasks.size} tasks" for (m, t) in tasks do if verbose then IO.println s!"replaying {m}" if let .error e := t.get then