From cee149cc1f37a221121efe5a8043a21b1c80f7b1 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Fri, 19 Dec 2025 15:09:33 +1100 Subject: [PATCH] feat: add `#import_path`, `assert_not_exists`, `assert_not_imported` commands (#11726) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR upstreams dependency-management commands from Mathlib: - `#import_path Foo` prints the transitive import chain that brings `Foo` into scope - `assert_not_exists Foo` errors if declaration `Foo` exists (for dependency management) - `assert_not_imported Module` warns if `Module` is transitively imported - `#check_assertions` verifies all pending assertions are eventually satisfied These commands help maintain the independence of different parts of a library by catching unintended transitive dependencies early. ### Example usage ```lean -- Find out how Nat got into scope #import_path Nat -- Declaration Nat is imported via -- Init.Prelude, -- which is imported by Init.Coe, -- which is imported by Init.Notation, -- ... -- which is imported by this file. -- Assert that a declaration should not be in scope yet assert_not_exists SomeAdvancedType -- Assert that a module should not be imported assert_not_imported Some.Heavy.Module -- Verify all assertions are eventually satisfied #check_assertions ``` Addresses https://lean-fro.zulipchat.com/#narrow/channel/398861-general/topic/path.20of.20an.20import ๐Ÿค– Prepared with Claude Code --------- Co-authored-by: Claude --- src/Lean/Elab.lean | 1 + src/Lean/Elab/AssertExists.lean | 210 +++++++++++++++++++++++++++++++ src/Lean/Parser/Command.lean | 25 ++++ tests/lean/run/assertExists.lean | 98 +++++++++++++++ 4 files changed, 334 insertions(+) create mode 100644 src/Lean/Elab/AssertExists.lean create mode 100644 tests/lean/run/assertExists.lean diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean index ebef0e041c..1ea475d05e 100644 --- a/src/Lean/Elab.lean +++ b/src/Lean/Elab.lean @@ -46,6 +46,7 @@ public import Lean.Elab.Notation public import Lean.Elab.Mixfix public import Lean.Elab.MacroRules public import Lean.Elab.BuiltinCommand +public import Lean.Elab.AssertExists public import Lean.Elab.Command.WithWeakNamespace public import Lean.Elab.BuiltinEvalCommand public import Lean.Elab.RecAppSyntax diff --git a/src/Lean/Elab/AssertExists.lean b/src/Lean/Elab/AssertExists.lean new file mode 100644 index 0000000000..12564b0e55 --- /dev/null +++ b/src/Lean/Elab/AssertExists.lean @@ -0,0 +1,210 @@ +/- +Copyright (c) 2022 Kim Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Patrick Massot, Kim Morrison, Damiano Testa +-/ +module + +prelude +public import Lean.Elab.Command + +/-! +# Commands to assert and check the (non-)existence of declarations or imports + +These commands can be used to enforce the independence of different parts of a library. + +* `#import_path Foo` prints the transitive import chain that brings `Foo` into scope. +* `assert_not_exists Foo` fails if `Foo` is in scope (used for dependency management). +* `assert_not_imported Module` fails if `Module` is transitively imported. +* `#check_assertions` verifies that all asserted declarations/modules eventually exist. +-/ + +public section + +namespace Lean + +/-- Find the dependency chain, starting at a module that imports `imported`, and ends with the +current module. + +The path only contains the intermediate steps: it excludes `imported` and the current module. -/ +def Environment.importPath (env : Environment) (imported : Name) : Array Name := Id.run do + let mut result := #[] + let modData := env.header.moduleData + let modNames := env.header.moduleNames + if let some idx := env.getModuleIdx? imported then + let mut target := imported + for i in [idx.toNat + 1 : modData.size] do + if modData[i]!.imports.any (ยท.module == target) then + target := modNames[i]! + result := result.push modNames[i]! + return result + +namespace Elab.Command + +/-- `AssertExists` is the structure that carries the data to check whether a declaration or an +import is meant to exist somewhere in a library. -/ +structure AssertExists where + /-- The type of the assertion: `true` means declaration, `false` means import. -/ + isDecl : Bool + /-- The fully qualified name of a declaration that is expected to exist. -/ + givenName : Name + /-- The name of the module where the assertion was made. -/ + modName : Name + deriving BEq, Hashable + +/-- Defines the `assertExistsExt` extension for adding a `HashSet` of `AssertExists` entries +to the environment. -/ +builtin_initialize assertExistsExt : SimplePersistentEnvExtension AssertExists (Std.HashSet AssertExists) โ† + registerSimplePersistentEnvExtension { + addImportedFn := fun as => as.foldl Std.HashSet.insertMany {} + addEntryFn := .insert + } + +/-- +`addAssertExistsEntry isDecl declName mod` extends the `AssertExists` environment extension +with the data `isDecl, declName, mod`. +This information is used to capture declarations and modules that are forbidden from +existing/being imported at some point, but should eventually exist/be imported. +-/ +def addAssertExistsEntry (isDecl : Bool) (declName mod : Name) : CommandElabM Unit := + modifyEnv (assertExistsExt.addEntry ยท { isDecl := isDecl, givenName := declName, modName := mod }) + +/-- `getSortedAssertExists env` returns the array of `AssertExists`, placing first all declarations, +in alphabetical order, and then all modules, also in alphabetical order. -/ +def getSortedAssertExists (env : Environment) : Array AssertExists := + assertExistsExt.getState env |>.toArray.qsort fun d e => (e.isDecl < d.isDecl) || + (e.isDecl == d.isDecl && (d.givenName.toString < e.givenName.toString)) + +/-- `importPathMessage env idx` produces a message laying out an import chain from `idx` to the +current module. The output is of the form +``` +Lean.Init, + which is imported by Lean.Elab.Command, + which is imported by Lean.Elab.AssertExists, + which is imported by this file. +``` +if `env` is an `Environment` and `idx` is the module index of `Lean.Init`. -/ +def importPathMessage (env : Environment) (idx : ModuleIdx) : MessageData := + let modNames := env.header.moduleNames + let msg := (env.importPath modNames[idx]!).foldl (init := m!"{modNames[idx]!},") + (ยท ++ m!"\n which is imported by {ยท},") + msg ++ m!"\n which is imported by this file." + +/-- +`#import_path Foo` prints the transitive import chain that brings the declaration `Foo` +into the current file's scope. + +This is useful for understanding why a particular declaration is available, +especially when debugging unexpected dependencies. +-/ +@[builtin_command_elab Lean.Parser.Command.importPath] +def elabImportPath : CommandElab := fun stx => do + let n := stx[1] + let env โ† getEnv + let decl โ† + try liftCoreM <| realizeGlobalConstNoOverloadWithInfo n + catch _ => + logInfoAt n m!"Declaration '{n.getId}' is not in scope." + return + let c โ† mkConstWithLevelParams decl + let msg โ† (do + let mut some idx := env.getModuleIdxFor? decl + | pure m!"Declaration {c} is defined in this file." + pure m!"Declaration {c} is imported via\n{importPathMessage env idx}") + logInfoAt n msg + +/-- +`assert_not_exists dโ‚ dโ‚‚ ... dโ‚™` is a command that asserts that the declarations named +`dโ‚ dโ‚‚ ... dโ‚™` *do not exist* in the current import scope. + +Be careful to use names (e.g. `Rat`) rather than notations (e.g. `โ„š`). + +It may be used (sparingly!) to enforce plans that certain files are independent of each other. + +If you encounter an error on an `assert_not_exists` command while developing a library, +it is probably because you have introduced new import dependencies to a file. +In this case, you should refactor your work +(for example by creating new files rather than adding imports to existing files). +You should *not* delete the `assert_not_exists` statement without careful discussion ahead of time. + +`assert_not_exists` statements should generally live at the top of the file, after the module doc. +-/ +@[builtin_command_elab Lean.Parser.Command.assertNotExists] +def elabAssertNotExists : CommandElab := fun stx => do + let env โ† getEnv + for n in stx[1].getArgs do + let decl โ† + try liftCoreM <| realizeGlobalConstNoOverloadWithInfo n + catch _ => + addAssertExistsEntry true n.getId (โ† getMainModule) + continue + let c โ† mkConstWithLevelParams decl + let msg โ† (do + let mut some idx := env.getModuleIdxFor? decl + | pure m!"Declaration {c} is defined in this file." + pure m!"Declaration {c} is not allowed to be imported by this file.\n\ + It is defined in {importPathMessage env idx}") + logErrorAt n m!"{msg}\n\n\ + These invariants are maintained by `assert_not_exists` statements, \ + and exist in order to ensure that \"complicated\" parts of the library \ + are not accidentally introduced as dependencies of \"simple\" parts of the library." + +/-- `assert_not_imported mโ‚ mโ‚‚ ... mโ‚™` checks that each one of the modules `mโ‚ mโ‚‚ ... mโ‚™` is not +among the transitive imports of the current file. + +The command does not currently check whether the modules `mโ‚ mโ‚‚ ... mโ‚™` actually exist. +-/ +@[builtin_command_elab Lean.Parser.Command.assertNotImported] +def elabAssertNotImported : CommandElab := fun stx => do + let env โ† getEnv + for id in stx[1].getArgs do + if let some idx := env.getModuleIdx? id.getId then + logWarningAt id + m!"the module '{id}' is (transitively) imported via\n{importPathMessage env idx}" + else + addAssertExistsEntry false id.getId (โ† getMainModule) + +/-- `#check_assertions` retrieves all declarations and all imports that were declared +not to exist so far (including in transitively imported files) and reports their current +status: +* โœ“ means the declaration or import exists, +* ร— means the declaration or import does not exist. + +This means that the expectation is that all checks *succeed* by the time `#check_assertions` +is used, typically once all of the library has been built. + +If all declarations and imports are available when `#check_assertions` is used, +then the command logs an info message. Otherwise, it emits a warning. + +The variant `#check_assertions!` only prints declarations/imports that are not present in the +environment. In particular, it is silent if everything is imported, making it useful for testing. +-/ +@[builtin_command_elab Lean.Parser.Command.checkAssertions] +def elabCheckAssertions : CommandElab := fun stx => do + let tk := stx[1] + let env โ† getEnv + let entries := getSortedAssertExists env + if entries.isEmpty && tk.isNone then logInfo "No assertions made." else + let allMods := env.allImportedModuleNames + let mut msgs : Array MessageData := #[m!""] + let mut outcome := m!"" + let mut allExist? := true + for d in entries do + let type := if d.isDecl then "declaration" else "module" + let cond := if d.isDecl then env.contains d.givenName else allMods.contains d.givenName + outcome := if cond then m!"{checkEmoji}" else m!"{crossEmoji}" + allExist? := allExist? && cond + if tk.isNone || !cond then + msgs := msgs.push m!"{outcome} '{d.givenName}' ({type}) asserted in '{d.modName}'." + msgs := msgs.push m!"---" + |>.push m!"{checkEmoji} means the declaration or import exists." + |>.push m!"{crossEmoji} means the declaration or import does not exist." + let msg := MessageData.joinSep msgs.toList "\n" + if allExist? && tk.isNone then + logInfo msg + if !allExist? then + logWarning msg + +end Lean.Elab.Command + +end diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 35f5c2057a..7b6a657120 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -531,6 +531,31 @@ structure Pair (ฮฑ : Type u) (ฮฒ : Type v) : Type (max u v) where @[builtin_command_parser] def check_failure := leading_parser "#check_failure " >> termParser -- Like `#check`, but succeeds only if term does not type check /-- +`#import_path Foo` prints the transitive import chain that brings the declaration `Foo` +into the current file's scope. +-/ +@[builtin_command_parser] def importPath := leading_parser + "#import_path " >> ident +/-- +`assert_not_exists Foo Bar` asserts that the declarations `Foo` and `Bar` do not exist +in the current import scope. Used for dependency management. +-/ +@[builtin_command_parser] def assertNotExists := leading_parser + "assert_not_exists " >> many1 ident +/-- +`assert_not_imported Mod1 Mod2` asserts that the modules `Mod1` and `Mod2` are not +transitively imported by the current file. Used for dependency management. +-/ +@[builtin_command_parser] def assertNotImported := leading_parser + "assert_not_imported " >> many1 ident +/-- +`#check_assertions` reports whether all `assert_not_exists` and `assert_not_imported` +assertions in the current file and its imports have been satisfied. +Use `#check_assertions!` to only show unsatisfied assertions. +-/ +@[builtin_command_parser] def checkAssertions := leading_parser + "#check_assertions" >> optional "!" +/-- `#eval e` evaluates the expression `e` by compiling and evaluating it. * The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result. diff --git a/tests/lean/run/assertExists.lean b/tests/lean/run/assertExists.lean new file mode 100644 index 0000000000..244cfa3e58 --- /dev/null +++ b/tests/lean/run/assertExists.lean @@ -0,0 +1,98 @@ +/-! +# Tests for `#import_path`, `assert_not_exists`, `assert_not_imported`, and `#check_assertions` +-/ + +-- Test #import_path with an existing declaration +/-- +info: Declaration LawfulMonadLift is imported via +Init.Control.Lawful.MonadLift.Basic, + which is imported by Init.Control.Lawful.MonadLift.Lemmas, + which is imported by Init.Control.Lawful.MonadLift.Instances, + which is imported by Init.Control.Lawful.MonadLift, + which is imported by Init.Control.Lawful, + which is imported by Init.Control, + which is imported by Init, + which is imported by this file. +-/ +#guard_msgs in +#import_path LawfulMonadLift + +-- Test #import_path with a non-existent declaration +/-- +info: Declaration 'NonExistentDecl' is not in scope. +-/ +#guard_msgs in +#import_path NonExistentDecl + +-- Test assert_not_exists with declarations that don't exist (should pass silently) +#guard_msgs in +assert_not_exists FooBarBaz + +#guard_msgs in +assert_not_exists NonExistent1 NonExistent2 + +-- Test assert_not_imported with modules that don't exist (should pass silently) +#guard_msgs in +assert_not_imported Fake.Module + +-- Test assert_not_exists with an existing declaration (should error) +/-- +error: Declaration LawfulMonadLift is not allowed to be imported by this file. +It is defined in Init.Control.Lawful.MonadLift.Basic, + which is imported by Init.Control.Lawful.MonadLift.Lemmas, + which is imported by Init.Control.Lawful.MonadLift.Instances, + which is imported by Init.Control.Lawful.MonadLift, + which is imported by Init.Control.Lawful, + which is imported by Init.Control, + which is imported by Init, + which is imported by this file. + +These invariants are maintained by `assert_not_exists` statements, and exist in order to ensure that "complicated" parts of the library are not accidentally introduced as dependencies of "simple" parts of the library. +-/ +#guard_msgs in +assert_not_exists LawfulMonadLift + +-- Test assert_not_imported with an imported module (should warn) +/-- +warning: the module 'Init.Control.Lawful.MonadLift.Basic' is (transitively) imported via +Init.Control.Lawful.MonadLift.Basic, + which is imported by Init.Control.Lawful.MonadLift.Lemmas, + which is imported by Init.Control.Lawful.MonadLift.Instances, + which is imported by Init.Control.Lawful.MonadLift, + which is imported by Init.Control.Lawful, + which is imported by Init.Control, + which is imported by Init, + which is imported by this file. +-/ +#guard_msgs in +assert_not_imported Init.Control.Lawful.MonadLift.Basic + +-- Test #check_assertions - should show the pending assertions +-- Note: The module name below is `lean.run.assertExists` (from the file path). +-- In VSCode or when run interactively, it would show `_stdin` instead. +/-- +warning: +โŒ๏ธ 'FooBarBaz' (declaration) asserted in 'lean.run.assertExists'. +โŒ๏ธ 'NonExistent1' (declaration) asserted in 'lean.run.assertExists'. +โŒ๏ธ 'NonExistent2' (declaration) asserted in 'lean.run.assertExists'. +โŒ๏ธ 'Fake.Module' (module) asserted in 'lean.run.assertExists'. +--- +โœ…๏ธ means the declaration or import exists. +โŒ๏ธ means the declaration or import does not exist. +-/ +#guard_msgs in +#check_assertions + +-- Test #check_assertions! - should only show unmet assertions +/-- +warning: +โŒ๏ธ 'FooBarBaz' (declaration) asserted in 'lean.run.assertExists'. +โŒ๏ธ 'NonExistent1' (declaration) asserted in 'lean.run.assertExists'. +โŒ๏ธ 'NonExistent2' (declaration) asserted in 'lean.run.assertExists'. +โŒ๏ธ 'Fake.Module' (module) asserted in 'lean.run.assertExists'. +--- +โœ…๏ธ means the declaration or import exists. +โŒ๏ธ means the declaration or import does not exist. +-/ +#guard_msgs in +#check_assertions!