feat: re-integrate lean4checker as leanchecker

src/CMakeLists.txt

@@ -695,7 +695,7 @@ endif()
 
 set(STDLIBS Init Std Lean Leanc)
 if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  list(APPEND STDLIBS Lake)
+  list(APPEND STDLIBS Lake LeanChecker)
 endif()
 
 add_custom_target(make_stdlib ALL
@@ -758,6 +758,12 @@ if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
     DEPENDS lake_shared
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make lake
     VERBATIM)
+
+  add_custom_target(leanchecker ALL
+    WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
+    DEPENDS lake_shared
+    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanchecker
+    VERBATIM)
 endif()
 
 if(PREV_STAGE)

src/Lean/Environment.lean

@@ -1502,7 +1502,8 @@ def mkEmptyEnvironment (trustLevel : UInt32 := 0) : IO Environment := do
   return {
     base := .const {
       const2ModIdx    := {}
-      constants       := {}
+      -- Make sure we return a sharing-friendly map set to stage 2, like in `finalizeImport`.
+      constants       := SMap.empty.switch
       header          := { trustLevel }
       extensions      := exts
       irBaseExts      := exts

src/LeanChecker.lean

@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2023 Kim Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Sebastian Ullrich
+-/
+import Lean.CoreM
+import Lean.Replay
+import LeanChecker.Replay
+import Lake.Load.Manifest
+
+open Lean
+
+unsafe def replayFromImports (module : Name) : IO Unit := do
+  let mFile ← findOLean module
+  unless (← mFile.pathExists) do
+    throw <| IO.userError s!"object file '{mFile}' of module {module} does not exist"
+  -- Load all module data parts (exported, server, private)
+  let mut fnames := #[mFile]
+  let sFile := OLeanLevel.server.adjustFileName mFile
+  if (← sFile.pathExists) then
+    fnames := fnames.push sFile
+    let pFile := OLeanLevel.private.adjustFileName mFile
+    if (← pFile.pathExists) then
+      fnames := fnames.push pFile
+  let parts ← readModuleDataParts fnames
+  if h : parts.size = 0 then throw <| IO.userError "failed to read module data" else
+  let (mod, _) := parts[0]
+  let (_, s) ← importModulesCore mod.imports |>.run
+  let env ← finalizeImport s mod.imports {} 0 false false (isModule := true)
+  let mut newConstants := {}
+  -- Collect constants from last ("most private") part, which subsumes all prior ones
+  for name in parts[parts.size-1].1.constNames, ci in parts[parts.size-1].1.constants do
+    newConstants := newConstants.insert name ci
+  let env' ← env.replay' newConstants
+  env'.freeRegions
+
+unsafe def replayFromFresh (module : Name) : IO Unit := do
+  Lean.withImportModules #[{module}] {} 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. `leanchecker` to check everything in the current project.
+or e.g. `leanchecker 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 `leanchecker --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
+  -- Contributor's note: lean4lean is intended to have a CLI interface matching leanchecker,
+  -- so if you want to make a change here please either make a sibling PR to
+  -- https://github.com/digama0/lean4lean or ping @digama0 (Mario Carneiro) to go fix it.
+  initSearchPath (← findSysroot)
+  let (flags, args) := args.partition fun s => s.startsWith "-"
+  let verbose := "-v" ∈ flags || "--verbose" ∈ flags
+  let fresh := "--fresh" ∈ 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 !fresh && target.isPrefixOf m || target == m then
+          targetModules := targetModules.insert m
+          found := true
+    if not found then
+      throw <| IO.userError s!"Could not find any oleans for: {target}"
+  if fresh then
+    if targetModules.length != 1 then
+      throw <| IO.userError s!"--fresh flag is only valid when specifying a single module:\n\
+        {targetModules}"
+    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!"leanchecker found a problem in {m}"
+        throw e
+  return 0

src/LeanChecker/Replay.lean

@@ -0,0 +1,191 @@
+/-
+Copyright (c) 2023 Kim Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Lean.CoreM
+import Lean.AddDecl
+import Lean.Util.FoldConsts
+
+/-!
+# `Lean.Environment.replay`
+
+`replay env constantMap` will "replay" all the constants in `constantMap : HashMap Name ConstantInfo` into `env`,
+sending each declaration to the kernel for checking.
+
+`replay` does not send constructors or recursors in `constantMap` to the kernel,
+but rather checks that they are identical to constructors or recursors generated in the environment
+after replaying any inductive definitions occurring in `constantMap`.
+
+`replay` can be used either as:
+* a verifier for an `Environment`, by sending everything to the kernel, or
+* a mechanism to safely transfer constants from one `Environment` to another.
+
+## Implementation notes
+
+This is a patched version of `Lean.Environment.Replay`, which is in the `lean4` repository
+up to `v4.18.0`, but will be deprecated in `v4.19.0` and then removed. Once it it removed,
+the prime on the `Replay'` namespace, the prime on `Lean.Environment.replay'`
+should be removed here.
+
+-/
+
+namespace Lean.Environment
+
+namespace Replay'
+
+structure Context where
+  newConstants : Std.HashMap Name ConstantInfo
+
+structure State where
+  env : Kernel.Environment
+  remaining : NameSet := {}
+  pending : NameSet := {}
+  postponedConstructors : NameSet := {}
+  postponedRecursors : NameSet := {}
+
+abbrev M := ReaderT Context <| StateRefT State IO
+
+/-- Check if a `Name` still needs processing. If so, move it from `remaining` to `pending`. -/
+def isTodo (name : Name) : M Bool := do
+  let r := (← get).remaining
+  if r.contains name then
+    modify fun s => { s with remaining := s.remaining.erase name, pending := s.pending.insert name }
+    return true
+  else
+    return false
+
+/-- Use the current `Environment` to throw a `Kernel.Exception`. -/
+def throwKernelException (ex : Kernel.Exception) : M Unit := do
+  throw <| .userError <| (← ex.toMessageData {} |>.toString)
+
+/-- Add a declaration, possibly throwing a `Kernel.Exception`. -/
+def addDecl (d : Declaration) : M Unit := do
+  match (← get).env.addDeclCore 0 d (cancelTk? := none) with
+  | .ok env => modify fun s => { s with env := env }
+  | .error ex => throwKernelException ex
+
+mutual
+/--
+Check if a `Name` still needs to be processed (i.e. is in `remaining`).
+
+If so, recursively replay any constants it refers to,
+to ensure we add declarations in the right order.
+
+The construct the `Declaration` from its stored `ConstantInfo`,
+and add it to the environment.
+-/
+partial def replayConstant (name : Name) : M Unit := do
+  if ← isTodo name then
+    let some ci := (← read).newConstants[name]? | unreachable!
+    replayConstants ci.getUsedConstantsAsSet
+    -- Check that this name is still pending: a mutual block may have taken care of it.
+    if (← get).pending.contains name then
+      match ci with
+      | .defnInfo   info =>
+        addDecl (Declaration.defnDecl   info)
+      | .thmInfo    info =>
+        -- Ignore duplicate theorems. This code is identical to that in `finalizeImport` before it
+        -- added extended duplicates support for the module system, which is not relevant for us
+        -- here as we always load all .olean information. We need this case *because* of the module
+        -- system -- as we have more data loaded than it, we might encounter duplicate private
+        -- theorems where elaboration under the module system would have only one of them in scope.
+        if let some (.thmInfo info') := (← get).env.find? ci.name then
+          if info.name == info'.name &&
+            info.type == info'.type &&
+            info.levelParams == info'.levelParams &&
+            info.all == info'.all
+          then
+            return
+        addDecl (Declaration.thmDecl    info)
+      | .axiomInfo  info =>
+        addDecl (Declaration.axiomDecl  info)
+      | .opaqueInfo info =>
+        addDecl (Declaration.opaqueDecl info)
+      | .inductInfo info =>
+        let lparams := info.levelParams
+        let nparams := info.numParams
+        let all ← info.all.mapM fun n => do pure <| ((← read).newConstants[n]!)
+        for o in all do
+          modify fun s =>
+            { s with remaining := s.remaining.erase o.name, pending := s.pending.erase o.name }
+        let ctorInfo ← all.mapM fun ci => do
+          pure (ci, ← ci.inductiveVal!.ctors.mapM fun n => do
+            pure ((← read).newConstants[n]!))
+        -- Make sure we are really finished with the constructors.
+        for (_, ctors) in ctorInfo do
+          for ctor in ctors do
+            replayConstants ctor.getUsedConstantsAsSet
+        let types : List InductiveType := ctorInfo.map fun ⟨ci, ctors⟩ =>
+          { name := ci.name
+            type := ci.type
+            ctors := ctors.map fun ci => { name := ci.name, type := ci.type } }
+        addDecl (Declaration.inductDecl lparams nparams types false)
+      -- We postpone checking constructors,
+      -- and at the end make sure they are identical
+      -- to the constructors generated when we replay the inductives.
+      | .ctorInfo info =>
+        modify fun s => { s with postponedConstructors := s.postponedConstructors.insert info.name }
+      -- Similarly we postpone checking recursors.
+      | .recInfo info =>
+        modify fun s => { s with postponedRecursors := s.postponedRecursors.insert info.name }
+      | .quotInfo _ =>
+        -- `Quot.lift` and `Quot.ind` have types that reference `Eq`,
+        -- so we need to ensure `Eq` is replayed before adding the quotient declaration.
+        replayConstant `Eq
+        addDecl (Declaration.quotDecl)
+      modify fun s => { s with pending := s.pending.erase name }
+
+/-- Replay a set of constants one at a time. -/
+partial def replayConstants (names : NameSet) : M Unit := do
+  for n in names do replayConstant n
+
+end
+
+/--
+Check that all postponed constructors are identical to those generated
+when we replayed the inductives.
+-/
+def checkPostponedConstructors : M Unit := do
+  for ctor in (← get).postponedConstructors do
+    match (← get).env.find? ctor, (← read).newConstants[ctor]? with
+    | some (.ctorInfo info), some (.ctorInfo info') =>
+      if ! (info == info') then throw <| IO.userError s!"Invalid constructor {ctor}"
+    | _, _ => throw <| IO.userError s!"No such constructor {ctor}"
+
+/--
+Check that all postponed recursors are identical to those generated
+when we replayed the inductives.
+-/
+def checkPostponedRecursors : M Unit := do
+  for ctor in (← get).postponedRecursors do
+    match (← get).env.find? ctor, (← read).newConstants[ctor]? with
+    | some (.recInfo info), some (.recInfo info') =>
+      if ! (info == info') then throw <| IO.userError s!"Invalid recursor {ctor}"
+    | _, _ => throw <| IO.userError s!"No such recursor {ctor}"
+
+end Replay'
+
+open Replay'
+
+/--
+"Replay" some constants into an `Environment`, sending them to the kernel for checking.
+
+Throws a `IO.userError` if the kernel rejects a constant,
+or if there are malformed recursors or constructors for inductive types.
+-/
+def replay' (newConstants : Std.HashMap Name ConstantInfo) (env : Environment) : IO Environment := do
+  let mut remaining : NameSet := ∅
+  for (n, ci) in newConstants.toList do
+    -- We skip unsafe constants, and also partial constants.
+    -- Later we may want to handle partial constants.
+    if !ci.isUnsafe && !ci.isPartial then
+      remaining := remaining.insert n
+  let (_, s) ← StateRefT'.run (s := { env := env.toKernelEnv, remaining }) do
+    ReaderT.run (r := { newConstants }) do
+      for n in remaining do
+        replayConstant n
+      checkPostponedConstructors
+      checkPostponedRecursors
+  return .ofKernelEnv s.env

src/lakefile.toml.in

@@ -8,7 +8,7 @@
 name = "lean4"
 bootstrap = true
 
-defaultTargets = ["Init", "Std", "Lean", "Lake", "LakeMain", "Leanc"]
+defaultTargets = ["Init", "Std", "Lean", "Lake", "LakeMain", "Leanc", "LeanChecker"]
 
 # Have Lake use CMake's build type (e.g., `Release`, `Debug`) where possible
 buildType = "${CMAKE_BUILD_TYPE_TOML}"
@@ -85,3 +85,7 @@ defaultFacets = ["static.export"]
 name = "Leanc"
 srcDir = "${CMAKE_BINARY_DIR}/leanc"
 defaultFacets = ["static"]
+
+[[lean_lib]]
+name = "LeanChecker"
+defaultFacets = ["static"]

src/stdlib.make.in

@@ -34,15 +34,15 @@ ifeq "${STAGE}" "0"
 endif
 
 # These can be phony since the inner Makefile/Lake will have the correct dependencies and avoid rebuilds
-.PHONY: Init Std Lean leanshared Lake libLake_shared lake lean
+.PHONY: Init Std Lean leanshared Lake libLake_shared lake lean LeanChecker leanchecker
 
 ifeq "${USE_LAKE}" "ON"
 
 # build in parallel
 Init:
 	${PREV_STAGE}/bin/lake build -f ${CMAKE_BINARY_DIR}/lakefile.toml $(LAKE_EXTRA_ARGS)
 
-Std Lean Lake Leanc: Init
+Std Lean Lake Leanc LeanChecker: Init
 
 else
 
@@ -68,6 +68,9 @@ Lake: Lean
 # lake is in its own subdirectory, so must adjust relative paths...
 	+"${LEAN_BIN}/leanmake" -C lake lib lib.export ../${LIB}/temp/LakeMain.o.export  PKG=Lake $(LEANMAKE_OPTS) OUT="../${LIB}" LIB_OUT="../${LIB}/lean" TEMP_OUT="../${LIB}/temp" OLEAN_OUT="../${LIB}/lean" EXTRA_SRC_ROOTS=LakeMain.lean
 
+LeanChecker: Lake
+	+"${LEAN_BIN}/leanmake" lib PKG=LeanChecker $(LEANMAKE_OPTS) OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}" LIB_OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}" OLEAN_OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}"
+
 endif
 
 ${LIB}/temp/empty.c:
@@ -170,3 +173,11 @@ ${CMAKE_BINARY_DIR}/bin/leanc${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_ARCHIVE_OUTPUT_
 	"${CMAKE_BINARY_DIR}/leanc.sh" $< ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@
 
 leanc: ${CMAKE_BINARY_DIR}/bin/leanc${CMAKE_EXECUTABLE_SUFFIX}
+
+${CMAKE_BINARY_DIR}/bin/leanchecker${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/libLeanChecker.a ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
+	@echo "[    ] Building $@"
+# on Windows, must remove file before writing a new one (since the old one may be in use)
+	@rm -f $@
+	"${CMAKE_BINARY_DIR}/leanc.sh" $< -lLake_shared ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@
+
+leanchecker: ${CMAKE_BINARY_DIR}/bin/leanchecker${CMAKE_EXECUTABLE_SUFFIX}