efmt in doc-gen4

Stream: lean4

[Henrik Böving]

Hi! I've written a little doc-gen4 PoC over here https://github.com/hargoniX/doc-gen4/ (if you want to try it yourself you'll have to change the hardcoded locations for olean files that will hopefully at some day :tm: be auto provided by lake). At the moment it basically prints information about all the declarations it can gobble up from the olean files into the command line. Now the next interesting step would of course be to generate some HTML from this (I have barely any clue about webdev so that'll be fun) and the first thing that jumped to my mind was how exactly shall I link from custom syntax to what it actually points to? Right now I'm just extracting Syntax objects from the type Exprs and pretty print them to the CLI but that is of course not enough for HTML. However as far as I understood the Syntax type it destroys this information about what is the actual functionality behind custom syntax? So I don't really know how to approach that at all.

Also this is basically my first Lean 4 meta program so I probably committed lots and lots of (style) mistakes here, please do point them out to me if you happen to check out the code^^

[Mac]

@Henrik Böving is there no main method / executable for thee doc-gen?

[Mac]

scratch that, I'm blind.

[Mac]

@Henrik Böving instead, better question, why are you hard coding the library into the executable? Also, you probably should be invoking the elaborator via runFrontend on some .lean and operating on the resulting environment, not calling importModules directly

[Wojciech Nawrocki]

I'd say if the tool is only meant to process .oleans and not run the elaborator, importModules sounds okay.

[Wojciech Nawrocki]

What do you mean by "link from custom syntax to what it actually points to"? If you are trying to find the source location of a declaration, DeclarationRange should help.

[Henrik Böving]

Mac said:

Henrik Böving instead, better question, why are you hard coding the library into the executable? Also, you probably should be invoking the elaborator via runFrontend on some .lean and operating on the resulting environment, not calling importModules directly

Right now I'm just hardcoding it because you told me the other day that lake doesnt yet allow me to fetch these parts as a script, ideally at some point it would be possible to have lake give me the paths + Name of the top level module to import and everything just work dynamically.

[Henrik Böving]

Wojciech Nawrocki said:

What do you mean by "link from custom syntax to what it actually points to"? If you are trying to find the source location of a declaration, DeclarationRange should help.

For example when something like ℕ pops up in a function declaration the current doc-gen links that to the natural numbers, e.g. here: https://leanprover-community.github.io/mathlib_docs/init/data/fin/basic.html#fin However as far as I could see from the Syntax datatype it doesnt provide information on what the ℕ notation actually stands for (?). So now I'm wondering how I would be able to achieve that.

[Sebastian Ullrich]

Henrik Böving said:

Mac said:

Henrik Böving instead, better question, why are you hard coding the library into the executable? Also, you probably should be invoking the elaborator via runFrontend on some .lean and operating on the resulting environment, not calling importModules directly

Right now I'm just hardcoding it because you told me the other day that lake doesnt yet allow me to fetch these parts as a script, ideally at some point it would be possible to have lake give me the paths + Name of the top level module to import and everything just work dynamically.

You can use lake print-paths for this. It will build the requested modules and give you back the LEAN_PATH for importing them. See https://github.com/leanprover/lean4/blob/45917f2f900f177259eebc7a6740193f86292927/src/Lean/Server/FileWorker.lean#L123 for how the server uses it.

[Henrik Böving]

Sebastian Ullrich said:

Henrik Böving said:

Mac said:

Henrik Böving instead, better question, why are you hard coding the library into the executable? Also, you probably should be invoking the elaborator via runFrontend on some .lean and operating on the resulting environment, not calling importModules directly

Right now I'm just hardcoding it because you told me the other day that lake doesnt yet allow me to fetch these parts as a script, ideally at some point it would be possible to have lake give me the paths + Name of the top level module to import and everything just work dynamically.

You can use lake print-paths for this. It will build the requested modules and give you back the LEAN_PATH for importing them. See https://github.com/leanprover/lean4/blob/45917f2f900f177259eebc7a6740193f86292927/src/Lean/Server/FileWorker.lean#L123 for how the server uses it.

Added this! Thank you.

[Mac]

Henrik Böving said:

Right now I'm just hardcoding it because you told me the other day that lake doesnt yet allow me to fetch these parts as a script, ideally at some point it would be possible to have lake give me the paths + Name of the top level module to import and everything just work dynamically.

Clearly, I am bad at communicating. :laughter_tears: Maybe an example would help. I personally would expect the use of doc-gen4 to work something like the following:

$ doc-gen4 Mathlib
... generate doc for the Mathlib module ..

where doc-gen4 is the built executable. If I need to augment LEAN_PATH so doc-gen4 can find Mathlib, I could do the following:

$ lake env doc-gen4 Mathlib

lake env runs the following command with the environment set up appropriately for the workspace.

[Henrik Böving]

@Mac The first example works now^^

[Sebastian Ullrich]

Henrik Böving said:

Wojciech Nawrocki said:

What do you mean by "link from custom syntax to what it actually points to"? If you are trying to find the source location of a declaration, DeclarationRange should help.

For example when something like ℕ pops up in a function declaration the current doc-gen links that to the natural numbers, e.g. here: https://leanprover-community.github.io/mathlib_docs/init/data/fin/basic.html#fin However as far as I could see from the Syntax datatype it doesnt provide information on what the ℕ notation actually stands for (?). So now I'm wondering how I would be able to achieve that.

The delaborator attaches synthetic positions to the generated Syntax objects that can be used to retrieve the original Expr, which you could e.g. check for being an Expr.const, or an application thereof (Expr.getAppFn) if you also want to e.g. link + to Add.add. The function for looking up the subterm given the position should be https://github.com/leanprover/lean4/blob/45917f2f900f177259eebc7a6740193f86292927/src/Lean/Widget/InteractiveCode.lean#L39, though apparently it is currently unused (because a TypeScript version is used instead in the client?). @Wojciech Nawrocki should be able to tell you more here.