The Syntax of the Import Section

Stream: lean4

[Simon Hudon]

I'm trying to do some search and replace on the import section of some Lean 4 source files and I'm wondering if there's a simple way that a low-tech parser / regex can determine where the import section ends in a file.

With Lean 3, after the last import, custom commands cannot be used right away so you only need to parse until you encounter one keyword among a fixed list. Is it still the case with Lean 4?

[Henrik Böving]

Lean 4 will not allow you to use imports again after you have started declaring stuff yes, I'd say as soon as you encounter a line that is:

• not a comment
• not an import
  the import section is done. At least the compiler has complained to me whenever I've violated this in the past.

[Sebastian Ullrich]

Simon Hudon said:

With Lean 3, after the last import, custom commands cannot be used right away so you only need to parse until you encounter one keyword among a fixed list. Is it still the case with Lean 4?

No, because every import statement expects exactly one module name.

[Simon Hudon]

Henrik Böving said:

Lean 4 will not allow you to use imports again after you have started declaring stuff yes, I'd say as soon as you encounter a line that is:

• not a comment
• not an import
  the import section is done. At least the compiler has complained to me whenever I've violated this in the past.

That was also the case with Lean 3. But Lean 3 and Lean 4 both allow you to define syntax for commands. That can be troublesome for parsing the import section because without context, when you scan a token, you can't know if it's a keyword or a module name. Lean 3 solves the problem by not letting you use a user-defined command as the first thing after the import section. @Sebastian Ullrich Now tells us that Lean 4 avoids the issue by allowing only one module name per import.

@Sebastian Ullrich , does it mean that the first thing after an import can now be a user-defined command?

[Sebastian Ullrich]

Yes.

[Alex J. Best]

I think community lean 3 changed at some point to be whitespace sensitive instead. Certainly you can now open_locale immediately after imports. https://github.com/leanprover-community/lean/pull/188

[Arthur Paulino]

(deleted)

[Anders Christiansen Sørby]

Is there any way to fix name collisions from imports? For example when you have a diamon dependecy tree

  A
/   \
B   C
\   /
  D

If you import B and C in D you run into trouble. In my case there C is depending on a copy of A, but it is still a problem.

[Arthur Paulino]

Are you using namespaces? It's a nice way to enclosure content

[Anders Christiansen Sørby]

Yes, but A uses the same namespace and definitions.

[Arthur Paulino]

Is the project on Github? (can we take a look at it?)

[Anders Christiansen Sørby]

https://github.com/yatima-inc/lean-ipld

[Arthur Paulino]

Which are the problematic files?

[Anders Christiansen Sørby]

Blake3 and Neptune both uses a module BinaryTools which produces name collisions

[Anders Christiansen Sørby]

I could ofc just wrap those files in namespaces, but ideally I want to extract this as a separate dependency

[Arthur Paulino]

Hm, so those are external dependencies? I don't have experience with such, sorry :(

[Anders Christiansen Sørby]

It uses the normal lean compiler and includes the lean source files as separate builds using the buildLeanPackage nix function.

[Sebastian Ullrich]

Anders Christiansen Sørby said:

In my case there C is depending on a copy of A

Without looking further into the actual code, it sounds like this is the problem right there. You cannot (transitively) import two different versions (i.e. derivations) of the same module. It's the same restriction as in Haskell.

[Anders Christiansen Sørby]

But in Haskell you can do import qualified to avoid name collisions. But I guess I just have to wrap with namespaces or make sure they use the same olean file?

[Locria Cyber]

Name collision from different packages/files is still possible. There's no way for the importer to choose what to import.