Inter-project name collision

Stream: lean4

[Jun Yoshida]

I ran into a problem about collision of theorem names in different projects.
I have two personal projects, say A and B, using Lean4; A doesn't depend on Mathlib while B does.
The problem is that I cannot use codes from the project A in B because some auxiliary lemmas in A have the same names as ones in Mathlib.
My questions are:

• is there any "standard" solution in such a situation?
• lake build stops at each collision pair with the error message like

B.lean:1:0: error: import A.Data.List.Basic failed, environment already contains 'List.dropLast_eq_take' from Mathlib.Data.List.Basic

It is good if I can detect all collision pair at onece. Any idea?

[Jun Yoshida]

Another concern is that, as Mathlib is growing, I am not sure my auxiliary theorems in the project A have "safe" names even in near future.

[Mac Malone]

@Jun Yoshida The usual way to solve this is for packages to not define all their definitions within a namespace that matches the package / root module name (i.e., A and B and your example). Only very standard libraries like Mathlib and Std should stick stuff in the root namespace or augment existing namespaces like List.

[Jun Yoshida]

If List.dropLast_eq_take, for example, is defined inbetween namespace A-end A, then I cannot write l.dropLast_eq_take for l : List Nat.
This seems a drawback.

[Alex J. Best]

(deleted)

[Kyle Miller]

The "standard" solution for having names in library namespaces might be to try to contribute such lemmas to mathlib or std.

Another solution would be to add a prefix to names you insert into library namespaces, like List.my_dropLast_eq_take or List.jun_dropLast_eq_take.

[Kyle Miller]

The safest solution is to do what Mac suggested, put your own things into your own namespace. It's true that it's unfortunate that you can't use l.dropLast_eq_take notation, but that's the tradeoff you have to take if you want to be safe against name collisions.

[Eric Wieser]

The "standard" solution for having names in library namespaces might be to try to contribute such lemmas to mathlib or std.

In this particular case it sounds like the lemma is already in mathlib; the problem is that project A decided to reimplement this lemma rather than depending on mathlib

[Jun Yoshida]

Thank you for a lot of advice. I do not use mathlib in the project A because it is a library for data structures/algorithms to be used in constructive context. Some name collision are actually due to Classical-free re-proof of theorems in std for which I just stupidly add primes in the last of the original name. I understand that the library name space is the safest solution, but it requires a huge refactor in the project A, which I want to avoid as much as possible.

I also consider the use of private declarations. If I keep track with such declarations in the project, I can export them locally in the same way as export private does.
Here is my attempt to this approach:

Definition of pkg_local attribute and pkg_include command

import Lean

/-
I define
* `pkg_local (pkg := PackageName)?` attribute, which register a private declaration in a declaration list associated to `PackageName`, and
* `pkg_include (pkg := PackageName)? ident*` command, which imports declarations specified by `decl`s from the declaration list associated to `PackageName` into the current file.
In both cases, the part `(pkg := PackageName)` is optional; if it is not served, `PackageName` is the head of the current module name (i.e. in the module `A.B.C`, ``PackageName = `A``).
-/

open Lean Elab Term Command Meta

/-!
### `PkgLocalDecl`
-/

/-- The data structure that carries major data of package local declarations -/
structure PkgLocalDecl where
  pkgName : Name
  declName : Name
  deriving Inhabited, Repr, BEq, Hashable


/-!
### `pkg_local` attribute
-/

syntax (name := pkg_local) "pkg_local " ("(" &"pkg" " := " ident ")")? : attr

initialize registerTraceClass `pkg_local

/-- The environment extension to track declarations with @[pkg_local] attribute. -/
initialize pkglocalExtension :
    SimpleScopedEnvExtension PkgLocalDecl (HashSet PkgLocalDecl) ←
  registerSimpleScopedEnvExtension {
    addEntry := fun dt => dt.insert
    initial := {}
  }

private def Lean.Name.head : Name → Name
| .anonymous => .anonymous
| .str .anonymous x => x
| .str child _ => child.head
| .num child _ => child.head

initialize registerBuiltinAttribute {
  name := `pkg_local
  descr := "Attribute for package-local definitions/theorems."
  applicationTime := .afterTypeChecking
  add := fun declName stx kind => do
    let `(attr| pkg_local $[(pkg := $pkgid)]?) := stx
      | throwError "unexted `@[pkg_local]` attribute {stx}"
    let .global := kind | throwError "`@[pkg_local]` can only be used as a global attribute."
    if !(isPrivateName declName) then
      logWarning "`[@pkg_local]` is used on a non-private declaration."
    MetaM.run' do
      dbg_trace "declName : {declName}"
      let moduleName ← getMainModule
      let pkgName := (pkgid.map fun id => (id.getId)).getD moduleName.head
      dbg_trace "pkgName : {pkgName}"
      pkglocalExtension.add {pkgName, declName}
}


/-!
### `pkg_include` command
-/

syntax (name := pkg_include) "pkg_include " ("(" &"pkg" " := " ident ")")? ident,* : command
syntax (name := pkg_include_all) "pkg_include " ("(" &"pkg" " := " ident ")")? " * " : command

@[inline] def getPkgLocalDecls {m : Type → Type} [Monad m] [MonadEnv m] (pkgName : Name) : m (Array PkgLocalDecl) := do
  let declsAll := pkglocalExtension.getState (← getEnv)
  bif pkgName == .anonymous then
    return declsAll.toArray
  else do
    let mut decls : Array PkgLocalDecl := {}
    for d in declsAll do
      if d.pkgName = pkgName then decls := decls.push d
    return decls

/-- Construct `Lean.Declaration` from `PkgLocalDecl` -/
@[inline] def makeDecl {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (pkgdecl : PkgLocalDecl) : m Declaration := do
  let cinfo ← getConstInfo pkgdecl.declName
  let name : Name :=
    mkPrivateName (← getEnv) ((privateToUserName? pkgdecl.declName).getD pkgdecl.declName)
  if (← getEnv).contains name then
    throwError s!"'{name}' has already been declared"
  let constval : ConstantVal := {
    name := name,
    levelParams := cinfo.levelParams,
    type := cinfo.type
  }
  match cinfo with
  | .thmInfo tinfo =>
    return Declaration.thmDecl {
      constval with
      value := mkConst pkgdecl.declName (tinfo.levelParams.map mkLevelParam),
    }
  | _ =>
    return Declaration.defnDecl {
      constval with
      value := mkConst pkgdecl.declName (cinfo.levelParams.map mkLevelParam),
      hints := ReducibilityHints.abbrev,
      safety := if cinfo.isUnsafe then .unsafe else .safe
    }

@[command_elab «pkg_include»]
def elabPkgInclude : CommandElab := fun stx => do
  let `(command| pkg_include $[(pkg := $pkgid)]? $ids,*) := stx
    | throwError "invalid use of 'pkg_include' command: {stx}"
  let pkgName : Name := (pkgid.map fun id => id.getId).getD (← getMainModule).head
  let pkgdecls ← getPkgLocalDecls pkgName
  let mut decls : Array PkgLocalDecl := {}
  for id in ids.getElems do
    dbg_trace "finding {id.getId} from {repr pkgdecls}"
    let some pkgdecl := pkgdecls.find? fun d => id.getId.isSuffixOf d.declName
      | throwError "local declaration not found: {id}"
    dbg_trace "{id} → {repr pkgdecl} found"
    decls := decls.push pkgdecl
  liftCoreM do
    for decl in decls do
      let decl ← makeDecl decl
      addDecl decl
      compileDecl decl

@[command_elab «pkg_include_all»]
def elabPkgIncludeAll : CommandElab := fun stx => do
  let `(command| pkg_include $[(pkg := $pkgid)]? *) := stx
    | throwError "invalid use of 'pkg_include' command: {stx}"
  let pkgdecls := pkglocalExtension.getState (← getEnv)
  liftCoreM do
    for pkgdecl in pkgdecls do
      let decl ← makeDecl pkgdecl
      addDecl decl
      compileDecl decl

Expected workflow is

1. Define a private def/theorem with pkg_local attribute:

-- A.Data.List.Basic

@[pkg_local]
private theorem List.foo {α : Type u} (x : List α) : x.length = x.length := sorry

2. In other modules in the same project, import the declaration using pkg_include command:

-- A.Data.MyData.Lemma

-- #print List.foo -- error before `pkg_include`

pkg_include List.foo

#print List.foo
/-
private theorem List.foo.{u} : {α : Type u} → (x : List α) → x.length = x.length := List.foo
-/