Merge pull request #26 from leanprover/project

feat: only run on current project

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,73 @@ 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.
+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".
 -/
 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 verbose := "-v" ∈ flags || "--verbose" ∈ flags
+  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 := #[]
+  let sp ← searchPathRef.get
+  for target in targets do
+    let mut found := false
+    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 verbose 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 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
   return 0

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."