doc-gen4 feature request

Stream: lean4

[Mac]

In order to test a new feature I am adding to Lake, I ended up playing around with doc-gen4 and I had some feedback to share. I noticed that doc-gen4 builds the entire dependency graph worth of modules every time it is run and also re-outputs the doc directory each time. @Henrik Böving, would it be feasible to split these tasks up? That is, have something like doc-gen4 --setup generate the directory first, and have a doc-gen4 Module --single output the documentation of single module?

Now, I should explain why this would be useful. The feature I am adding to Lake is called "module facets". A package can define a facet like so:

require «doc-gen4» from git "https://github.com/leanprover/doc-gen4"

module_facet docs : PUnit := fun mod => do
  let some docGen4 ← findLeanExe? &`«doc-gen4»
    | error "no doc-gen4 executable configuration found in workspace"
  let exeTarget ← docGen4.info.recBuild
  let task ← exeTarget.bindSync fun exeFile depTrace => do
    proc {
      cmd := exeFile.toString
      args := #[mod.name.toString]
      env := ← getLeanEnv
    }
    return depTrace
  return ActiveTarget.opaque task

And then users can build the facet on any module by using lake build +Module:docs. For example, doc-gen4 could define such a facet and then any package importing it can build documentation for a module using such am invocation.

P.S. I wasn't sure where was best to put this (e.g., here, on the doc-gen4 repository's issues, etc.). If there is a place you would prefer @Henrik Böving feel free to say and I will do that next time. :laughing:

[Wojciech Nawrocki]

This looks very cool. If you are up for a bit of bikeshedding, I'll note that I always found Lake's "facet" terminology a bit mysterious. As a non-native speaker, I could probably count on one hand the number of times I'd heard it used before Lake. This may well be an advantage - while there is a dictionary definition (which I just looked up), I can basically conceptualize "facet of X" as a new idea meaning "a thing that Lake produces from X" independently of non-programming uses. The first alternative that came to mind was module_functor but that's mysteriously mathematical and probably not better. module_view uses a more common noun. But again, maybe the more obscure word is a good idea.

[Mac]

@Wojciech Nawrocki I appreciate the feedback! :smile: I do note, though, that there was not actually much bikeshedding there as, by the end of the comment, you appear to have come around to the terminology. At least I think that is a fair reading?

[Wojciech Nawrocki]

That's right. I am raising the point in case others have thoughts on this.

[Henrik Böving]

What exactly would you expect --setup to do? Just generate build/doc? Or the entire directory layout because creating that without analysis of the modules seems kinda hard?

Regarding the --single output, that is possible but the page will likely end up with a million broken links (or a lot of links less) like that, do we really want that?

[Henrik Böving]

Ideally we could just build a caching mechanism into doc-gen that checks whether a doc file is older/newer than the .olean file and doesn't regen it right?

[Mac]

Henrik Böving said:

What exactly would you expect --setup to do? Just generate build/doc? Or the entire directory layout because creating that without analysis of the modules seems kinda hard?

Regarding the --single output, that is possible but the page will likely end up with a million broken links (or a lot of links less) like that, do we really want that?

From my quick examination of the directory it seems like only the Module html files (e.g., Test.html) and the declaration data are dependent on the analysis. Everything else (e.g., CSS, JS, etc.) are just static resources copied into the directory. Thus, I was thinking doc-gen4 --setup would do just that later step (setting up the directory and copying the static resources).

For --single, doc-gen generating links that are broken until the documentation for the linked module is generated is exactly what I would want. It would also maybe be nice to be able to specify an different base URLs for modules of different packages (this way doc-gen4 wouldn't need to generate the entire tree, but just link to already generated documentation for remote packages).

Henrik Böving said:

Ideally we could just build a caching mechanism into doc-gen that checks whether a doc file is older/newer than the .olean file and doesn't regen it right?

My plan was essentially to do the reverse. Have the doc-gen4 executable operate as a light-weight utility hat produces documentation that Lake can smartly call out to (if a rebuild is needed) when the user request new documentation. In such a situation, doc-gen could leave all the dependency analysis, module building, and trace checking to Lake. This allows each tool to focus on what it is good at and prevent code duplication across the core tools. What do you think, though?

[Sebastian Ullrich]

Assuming we want to automatically run doc-gen4 in the lean4 CI as well at some point and assuming we still use Nix for building the docs at that point, this setup sounds good to me as well. It should be relatively easy to integrate into an incremental Nix build, similar to how we're e.g. already doing that for doc/examples/ (which should also be ported to doc-gen4): https://github.com/leanprover/lean4/blob/c7c6fc8bc903392c0e4832a4c2804809bee1bd6f/doc/flake.nix#L82-L88

[Henrik Böving]

Mac said:

For --single, doc-gen generating links that are broken until the documentation for the linked module is generated is exactly what I would want. It would also maybe be nice to be able to specify an different base URLs for modules of different packages (this way doc-gen4 wouldn't need to generate the entire tree, but just link to already generated documentation for remote packages).

doc-gen4 still needs to take a look at the entire dependency tree to generate the tree view but that should be fine I guess, it doesn't need to run the expensive analysis part on them.

Either way what you are asking for definitely makes sense to me if we want a tighter integration of doc-gen and lake in the future, people will stop using it as a standalone tool at that point anyways so its w/e.

That being said I'll probably not get around to implementing it soon, I've my exams for this semester in 2 weeks (spread over 2 weeks) so my anxious mind won't allow me to write much Lean without feeling guilty and wanting to learn even though I know I'll easily pass :D So I'll get back to it in either 4 weeks or in the next week if I end up overcoming my guilt^^ Hence it would probably make sense to open an issue for it so I don't end up forgetting about it

[Henrik Böving]

I spent a while implementing this now, there is a second issue. doc-gen generates a file declaration-data.bmp (its bmp instead of JSON for Github pages hack reason...they cache .bmp, dont ask) which contains the declaration data the JS can use for the client side search of stuff. I had the idea of splitting this up into multipl declaration-data-topLevelModule.bmp but of course the JS needs to know which files to fetch, which I wanted to circumvent by using a central declaration-data.bmp that tells it where to fetch data from. However in order for this to work out the step that generates declaration-data.bmp would have to already know all the modules that are involved and not just a single one (in the case of --single) or none at all in the case of --setup. In theory I guess I could append to the file over time but that seems very hacky and wouldn't harmony nicely with the Nix idea of Sebastian :( so I'm out of ideas right now how to separate the steps for the modules properly and keep the search working. Would someone else happen to have one?

[Mac]

Henrik Böving

How about generating it at the end (after documentation for some modules has been generated). For example:

doc-gen4 --setup # setup doc directory
doc-gen4 A --single # output module A docs
doc-gen4 B C --single # output module B/C docs
doc-gen4 --index # output `declaration-data.tmp` with index for search of A B C
doc-gen4 D # output module D docs
doc-gen4 --index # regenerate `declaration-data.tmp` with index for search of A B C D

It also might be worthwhile to make the options subcommands instead (e.g., setup, index, tree, single, etc.)

[Henrik Böving]

Oh that would be fine for Nix as well? I was under the assumption that it wouldn't like if i mutate the file afterwards but if that works I'll do it like that.

[Sebastian Ullrich]

We can always mutate a copy of the original file... :)

[Henrik Böving]

@Mac got it: https://github.com/leanprover/doc-gen4#multi-stage

[Mac]

@Henrik Böving Cool! Some comments:

• I was envisioning single to build literally a single module. It seems to only built root modules of a packages. I would also like to do e.g., doc-gen4 single Lean.Data.Json
• The init/setup command seems to be missing? I see it in the code but there appears to be no CLI to use it.

[Henrik Böving]

Oh i forgot to delete that, it is not necessary finalize does both the init and the finalize part as suggested by @Sebastian Ullrich in the PR, there is no need to separate them.

[Henrik Böving]

The single non root module part requires a little more work but should be doable as well I believe.

[Mac]

Henrik Böving said:

Oh i forgot to delete that, it is not necessary finalize does both the init and the finalize part as suggested by Sebastian Ullrich in the PR, there is no need to separate them.

Ah, maybe rename the command to index or something else that suggests it need not be used only at the end?

[Henrik Böving]

"finalize" sounds pretty eh final to me?

[Mac]

That's my point, it makes it sound like it can only be used at the end when, as you stated, it can also be used at the start.

[Mac]

Also, could you elaborate on why the top level module argument is needed for single?

[Henrik Böving]

Because in order for the navbar on the left hand side to show the entire module tree we need to know the module tree, I did also not like this as well but unless we get rid off the navbar as it is right now it is required.

[Mac]

Henrik Böving said:

Because in order for the navbar on the left hand side to show the entire module tree we need to know the module tree,

Ah, so this is something that could be solve by lake graph?

[Henrik Böving]

Hmmmm, thinking further it is also required for the links between modules to work out because I need to know where Nat is in order to link to it from say Mathlib.

[Mac]

Or, wait, could the navbar on the left hand side use an iframe to point to a HTML file e.g., navbar.html that is generated during doc-gen4 finalize.

[Henrik Böving]

That might work out yeah but then the link issue is still blocking sadly :/

[Mac]

Could you elaborate on the link issues? I am not entirely sure what you mean.

[Henrik Böving]

Oh it actually doesn't happen because of transitive imports I guess mhm

Buuuut I have a third thing ;p and this is actually a bug I noticed before introducing this. The imported-by part on the top right hand side needs to know all modules to know where it was imported from.

[Henrik Böving]

So for example if we only import Std it wont show that Std.Data.HashMap is imported from Lean and Mathilb.

[Mac]

Henrik Böving said:

Oh it actually doesn't happen because of transitive imports I guess mhm

doc-gen4 single should not be building imports, correct?

[Henrik Böving]

Yes it has to because of this link issue. If I have a setup like this:

• Lib1 top level modules
• Lib2 top level module
• TopLevelLib which imports Lib1 and Lib2

and we have a declaration in Lib1 that uses a type from Lib2 I need to know the location (that is, the file) inside of Lib2 to link that type from Lib1.

So for example in Mathlib if I have a reference to Nat I need to have imported Init to know that it is in Init.Prelude and then link there from Mathlib.

[Mac]

Henrik Böving said:

So for example if we only import Std it wont show that Std.Data.HashMap is imported from Lean and Mathilb.

I think that is fine. If no top-level module(s) are provided, just don't generate the "Imported by" section. This makes sense for API documentation that is uploaded to the web, were the library creator will have no knowledge of what downstream modules import it.

[Mac]

testing: docs4#Nat

[Mac]

Henrik Böving said:

I need to know the location (that is, the file) inside of Lib2 to link that type from Lib1.

Could it not just link them using the same way Zulip command does e.g., <docs>/find/?pattern=<type>#doc?

[Henrik Böving]

docs4#Nat uses find.js to figure out where Nat is. That is a possiblity to fix this (so just link to the right find.js call instead of linking directly) but a rather ugly one IMO.

[Henrik Böving]

Yeah

[Mac]

I would quite like it. The whole point, for me, of doc-gen4 single Foo.Bar is to generate the docs for exactly the module Foo.Bar and nothing else.

[Mac]

More broadly, my hope is remove Lake as a dependency for doc-gen4.

[Henrik Böving]

Okay so we have:

• iframe for navbar to avoid the top level module
• building single modules instead of just top level ones
• always using find.js instead of direct links
• rename finalize to index
• dropping Imported By
  right?

[Henrik Böving]

Mac said:

More broadly, my hope is remove Lake as a dependency for doc-gen4.

But I need lake graph for my search path and stuff :p though I guess you mean as a direct dependency?

[Mac]

Henrik Böving said:

But I need lake graph for my search path and stuff :p though I guess you mean as a direct dependency?

No you don't. You can just use lake exe doc-gen4 <args> and lake will set the environment's search path appropriately. :)

[Mac]

Henrik Böving said:

Okay so we have:

• iframe for navbar to avoid the top level module
• building single modules instead of just top level ones
• always using find.js instead of direct links
• rename finalize to index
• dropping Imported By

Sounds great to me!

...

Wait a second, is the find.js trick even needed? Isn't the information as to where a type comes from already available in the environment of the module to analyze? Since the import of e.g., Foo.Bar also includes its transitive dependencies?

[Henrik Böving]

Yeah that's what I said above as well but you seemed to disagree?

[Mac]

Sorry, I think there was a miscommunication. I meant that doc-gen4 should not need to generate documentation of transitive dependences (they still need to be built by Lean/Lake for the module to be built and imported, though) and I interpreted your response to mean that links require documentation to be generated for the transitive imports, but I think I musunderstood?

[Henrik Böving]

Yeah I just meant the same thing as you said just now, it already does not generate documentation for transitives right now^^

[Henrik Böving]

@Mac like this? https://github.com/leanprover/doc-gen4/tree/improve-single#multi-stage

[Mac]

@Henrik Böving Great!

To verify, the following:

doc-gen4 single Mathlib
doc-gen4 index Mathlib

Would just produce the documentation for the single top-level Mathlib module and not any of its submodules (e.g., Mathlib.Algebra), correct? Similarly replacing Mathlib with Mathlib.Algebra would generate documentation just for the single Mathlib.Algebra module and not any of its submodules as well.

Also, why does doc-gen4 index need a module as an argument?

[Henrik Böving]

Right now its transitive but that should be a one line diff :tm:

The module is for the navbar as explained above we need a module tree to build it, however it is now only built once and included as an iframe as you suggested.

[Mac]

Henrik Böving said:

The module is for the navbar as explained above we need a module tree to build it, however it is now only built once and included as an iframe as you suggested.

Can you not just use the file tree in the build/doc folder to generate it?

[Mac]

A tree walk of the folder should work. However, you either need to special case away index.html or move the module documentation into a dedicated api folder so the other files (like index.html) don't get caught in the walk.

[Mac]

If you need an example of how to do such a walk see forEachModuleIn in Lake, which performs this walk for each .lean file in the directory tree.

[Henrik Böving]

True that would work, I'll get to that as well...I won't move it into an api folder for now since that would require some more refactoring basically everywhere for the linking stuff but I'll put that onto the list.

The non transitive stuff now works as well, however not on Mathlib.Algebra since that is not a Lean file but it can now be used for single Lean files only.

[Mac]

Great! (Though it appears my lack of mathlib knowledge is showing.)

[Henrik Böving]

Also is there a specific reason you are not using docs4#System.FilePath.walkDir for that forEachModuleIn?

[Mac]

For one, I am not sure that even existed at the time Glob was initially created. :laughter_tears: Secondly, that returns the full real path of the file and it is non-trivial (and likely impossible in the presence of symlinks) to reverse engineer the module path from that.

[Wojciech Nawrocki]

Henrik Böving said:

Also is there a specific reason you are not using docs4#System.FilePath.walkDir for that forEachModuleIn?

Btw, that link sends me to an empty page on Safari 15.5. The HTML seems itself seems empty:

<html lang="en">
<head>
    <link rel="preload" href=".././declaration-data.bmp">
    </link>
    <script>
    const SITE_ROOT = ".././";
    </script>
    <script type="module" async="true" src="./find.js"></script>
</head>
<body></body>
</html>

[Mac]

@Wojciech Nawrocki Link works for me on Chromium 99.0.4844.65

[Henrik Böving]

Works on Firefox as well....mysterious.

I want to add that my frontend knowledge is almost 0 and if something like this happens I have absolutely no clue how to help you /o\

[Wojciech Nawrocki]

If I am reading the HTTP response correctly, the body is also empty there so this seems like a backend issue (the server is not sending anything).

[Henrik Böving]

The backend is just a static file host by github pages, I don't think it should be acting up.

[Wojciech Nawrocki]

You are right, it looks like the preload should be <link rel="preload" href=".././declaration-data.bmp" as="image"> (or whatever type you need for the as), otherwise Safari rejects it.

[Henrik Böving]

I'll push a fix for that soon then^^

[Henrik Böving]

@Mac next thing I noticed which will of course break like this. Foreign instances of typeclasses will no longer be visible at the instances list...I'm not quite sure whether that is reasonable? That seems to invalidate this feature as well kinda.

Foreign in this context meaning: Not declared in this exact file.

[Henrik Böving]

But I got the index without import feature implemented as well now regardless, i'm just observing that it keeps cutting down on the information it can be provide which is obvious given the fact it doesn't use global analysis in this mode I guess.

[Mac]

Henrik Böving said:

i'm just observing that it keeps cutting down on the information it can be provide which is obvious given the fact it doesn't use global analysis in this mode I guess.

While this is unfortunate, I also think it is reasonable. If a library author serves API documentation on the web it makes sense that it would not be able to tell you were you used / augmented the library in your own code. And it would also make sense for the API documentation not to include the documentation of all its dependencies. Especially since, at some point, a library should hopefully be compatible with multiple different versions of its dependencies rather than the specific one it was built with.

However, for local documentation were we do have a global persepective, it is worthwhile to have the option to provide some root to give this information to doc-gen4 (or alternatively, it could invoke lake graph to get hat information once that command exists).

[Henrik Böving]

But the issue here is that not even all of the library author's instances will show up. Right now as we elaborated above single Module.Foo.Bar will only import that file and all of its dependencies. If this module declares a typeclass it will be the first module that can also declare instances on them so the renderer for the type class declaration will only see the instances in this exact same file and not say in Module.Foo.Nat.Basic which imports Module.Foo.Bar itself and declares an instance for Nat.

[Mac]

Henrik Böving said:

Foreign instances of typeclasses will no longer be visible at the instances list...I'm not quite sure whether that is reasonable?

Could we have some equivalent to find.js that uses the data generated during index to dynamically populate this listing (and maybe the same could happen for "imported by")

[Henrik Böving]

So basically stuff even more information into the declaration-data files...I don't see why that shouldn't work at least. If i understood the JS stuff correctly it is also already organizing them in some sort of DB you can do queries on so I guess one could dynamically query for all instances of a certain class yeah.

[Mac]

This is kind of my general solution to these problems -- the information that can be generated from a single file should be generated immediately on single and information which needs larger scope should lazily acquire it from some resource generated by index.

[Henrik Böving]

Makes sense yeah. I'll see what I can do regarding that tomorrow then. I think focusing on specific files is a great idea for reducing complexity anyways so the refactors I'm doing right now are most likely beneficial in general.

[Mac]

Note that this incremental approach has a major advantage: It means you don't have to regenerate documentation for a module unless that module itself changes. Which, in turn, means that documentation for static dependencies never has to be regenerated.

[Sebastian Ullrich]

Out of curiosity, what order of compile times are we talking about here for pure doc-gen? I know of course that adding LeanInk generation necessarily is slow, but for that we have the plan of plugging it right into the initial package build in order to avoid double elaboration of the whole project.

[Henrik Böving]

WIthout LeanInk a full render of mathlib (this includes the parts it imports from Init Std and Lean of course) that only reads the olean files and doesn't compile them via lake we have 47 seconds of build time right now and the tool itself is still not parallelized so I'd imagine there is a bit of speedup left there.

The build time in general does also depend a little bit on how many equational lemmata it fails to generate, there are two reasons for failure right now:

1. proof failure, those used to be there but are actually fully gone by now, very cool
2. timeouts, the things that timeout while generating their proof say it was for 5k heartbeats and we have like a dozen timeouts right now. That used to be a lot more as well and I remember the build taking over a minute as well in past times. Now I guess we don't necessarily have to generate the proof for the equational lemma and can only steal the term from Lean? But I'd have to dig a little deeper in the API for that.

Anyway, long story short: ~50s right now standalone.

[Sebastian Ullrich]

Ah, generating equational lemmas is not cheap, yeah. Regarding parallelism, when invoked per module I guess this becomes the responsibility of whoever invokes doc-gen4.

[Gabriel Ebner]

It means you don't have to regenerate documentation for a module unless that module itself changes.

We have (or want, or at least have in Lean 3) lots of documentation content that is global. This is one of the big advantages over just browsing the source. For example, type classes have a list of instances, types have a list of type classes that they implement.

[Henrik Böving]

The thing you saw in the JSON thread is for getting just that to work^^ The idea is that each module generates a JSON file with its information and then there is a final doc-gen4 index call that combines all of the JSONs into a huge JSON file that the instance lists, the search etc. is built from

[Henrik Böving]

Alright @Wojciech Nawrocki i got your as image fix up now, does it work?

@Mac I moved the other stuff to JSON as well now and played around a little with the builds, everything seems to be working nicely and one module at a time, no transitive stuff etc. Classes and Imported by still work :thumbs_up:

[Mac]

@Henrik Böving does that mean you can remove Lake as a dependency now? If not, what else do you need Lake for?

[Henrik Böving]

Lake is right now used for the search path and for linking to git source URLs so both of that would be covered by the lake graph we discussed. (the search path stuff also by the exec one but not the git source URLs)

[Mac]

@Henrik Böving couldn't you git the git source URLS by walk the directories in lean_packages and running git remote get-url origin?

[Henrik Böving]

Yes but how would I know where each module is coming from?

[Mac]

To explain my rationale, not needing to call lake from doc-gen4 would be beneficial as it would not require restarting lake and thus not re-elaborating the configuration files and re-resolving dependencies

[Henrik Böving]

I get that yeah but assuming I know all of the git remote urls from the lean_packages directory I still need a map from Lean module -> directory its coming from right? Lean already has to figure this out when it loads the module I guess? But I dont know how to access this information.

[Mac]

Henrik Böving said:

Yes but how would I know where each module is coming from?

How are you doing this currently doing this? Are you using findModule?

[Henrik Böving]

https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Output/SourceLinker.lean#L80-L84

[Henrik Böving]

But yeah basically asking Lake for help

[Wojciech Nawrocki]

Henrik Böving said:

Alright Wojciech Nawrocki i got your as image fix up now, does it work?

Mac I moved the other stuff to JSON as well now and played around a little with the builds, everything seems to be working nicely and one module at a time, no transitive stuff etc. Classes and Imported by still work :thumbs_up:

Ahh it still doesn't, it looks like the actual error that was obscured by the preload one is that Safari doesn't support lookbehind. Honestly I wouldn't worry about it, I'll just use a more up-to-date browser :)

[Wojciech Nawrocki]

(Tbf though, you'll probably have people on Macs run into this again.)

[Henrik Böving]

I never signed up to do frontend work /o\ :D but I guess I'll look into that as well. Though I want to get the Lake feature and the LeanInk link back done by the end of next week since I'll be back to work after that and have less time to spend on it

[Mac]

Wojciech Nawrocki said:

Safari doesn't support lookbehind.

I looked at the SafariWebKit Bugzilla entry for it and its been sitting open for 5 years with virtually no feedback Safari is a major browser with regular updates, the fact it does not support a 5 year old standard feature is actually insane. Not only that, its not like this is some complex browser feature, this is just standard regex. If necessary, the could probably just directly copy existing an regex compiler implementation that supports the feature into the codebase. I am honestly flabbergasted to learn this.

[Mauricio Collares]

AFAIK there are only two regexp compilers used in browsers, JavaScriptCore's (YARR) and V8's (Irregexp). Firefox never had its own regexp compiler. It would be a shame to reduce that number in half.

[Henrik Böving]

Mac said:

Henrik Böving said:

Yes but how would I know where each module is coming from?

How are you doing this currently doing this? Are you using findModule?

Do you have an alternative idea?

[Mac]

@Henrik Böving not at the moment