Multiple-import syntax

Stream: lean4

[James Gallicchio]

Thoughts on adding built-in syntax for multiple import? something like

import MyPackage.Namespace.{Basic,NotSoBasic,Lemmas}

since we're trying to move away from the default files it seems like a good idea. (has this been discussed before? I feel like it has been, but I couldn't find any relevant threads)

[James Gallicchio]

can this be done with macros? Like if you first import Std.MultiImport or something and then get multi-import syntax? or is import a special syntax that can't be macro-ified?

[Kyle Miller]

I don't know the answer, but I do know that this function is responsible for parsing the header, to get the list of modules to import.

[Kyle Miller]

The header parser is at the top of the file, and it looks like it's not something you can override as a user:

def «prelude»  := leading_parser "prelude"
def «import»   := leading_parser "import " >> optional "runtime" >> ident
def header     := leading_parser optional («prelude» >> ppLine) >> many («import» >> ppLine) >> ppLine

[François G. Dorais]

What does import runtime do? I see it sets the module flag runtimeOnly but, after a quick search, I couldn't find where it is actually used.

[François G. Dorais]

I found the flag used in Lean.importModules where the flag causes it to ignore the import. That's probably the only effect?

[Mario Carneiro]

it's deprecated