Syntax for imports

Stream: lean4

[Damiano Testa]

Is it possible to get some form of Syntax for the imports of a file?

What I would like is to extract from the current file something like an Array Syntax, where each entry represents a import X, for each module imported by the current file. Even just the Syntax terms for the names of the files would be good enough!

[Damiano Testa]

Here is an example of what I would like (not working code):

import A
import B

open Lean Elab Command
def getImportSyntax : CommandElabM (Array Syntax) := <insert magic code here>

run_cmd
  dbg_trace (← getImportSyntax)
/-
#[
  (Command.import "import", ("A")),
  (Command.import "import", ("B"))
]
-/

[Michael Rothgang]

Let me second this request: currently, the broadImports style linter in mathlib does some ad-hoc parsing of the file to determine all imports. I wouldn't mind replacing that by something more principled.

[Adam Topaz]

docs#Lean.Environment

[Damiano Testa]

I am specifically interested in getting the ranges of the individual imports: does the environment hold that?

[Adam Topaz]

The information is contained (in one way or another) in the header as part of the environment

[Adam Topaz]

(Sorry, the I added the link above for my own convenience since I’m on mobile)

[Damiano Testa]

I should have been more specific: I know how to access the "processed" imports, direct and transitive from the environment. I do not know how to get ranges, so that I can, for instance, log a warning on a targeted import.

[Adam Topaz]

Yeah I understand. For some reason I thought the syntax for the imports was saved, but I guess not

[Adam Topaz]

I guess you could get the source of the current file and use something like https://leanprover-community.github.io/mathlib4_docs/Lean/Parser/Module.html#Lean.Parser.parseHeader

[Adam Topaz]

I don’t know if that’s the best way :-/

[Thomas Murrills]

I’ll third the request, and specifically propose that Import should have an optional ref? field.

[Thomas Murrills]

I’m not 100% positive this is the best option, but hopefully proposing something specific will invite criticism (or agreement!), and we can figure out what would be! :)

[Damiano Testa]

I personally like the Import.ref? proposal very much! I'm guessing you were thinking of Option Syntax (or maybe Option (TSyntax `something) as its type?

Why Option, though? Could it not be just Import.ref? (Note the question mark outside the code!)

[Eric Wieser]

How would withImportModules work in that case?

[Kyle Miller]

Adam Topaz said:

I don’t know if that’s the best way :-/

I think that might be the only reliable way to do this at the moment, though it looks like this is packaged up by docs#Lean.Elab.parseImports, which is used for getting the lean executable to print imports with the -d flag.

[Kyle Miller]

Eric Wieser said:

How would withImportModules work in that case?

What's the objection? Synthetic Imports? Option Syntax can be collapsed to Syntax using Syntax.missing at least.

[Eric Wieser]

Ah, Syntax.missing indeed resolves my concern

[Damiano Testa]

Kyle showed me how to actually use this:

import /- -/Lean
-- then a random comment
/-
trying to confuse
import Command
-/
import Batteries /- an actual import -/ import Lean
import

Batteries

open Lean Parser in
run_cmd
  let fm ← getFileMap
  let fil ← getFileName
  let (stx, _) ← parseHeader { input := fm.source, fileName := fil, fileMap := fm }
  dbg_trace "'{stx}'"
/-
'(Module.header
 []
 [(Module.import "import" [] `Lean [])
  (Module.import "import" [] `Batteries [])
  (Module.import "import" [] `Lean [])
  (Module.import "import" [] `Batteries [])])'
-/