doc-gen4

Stream: lean4

[Henrik Böving]

I'd be interested in writing a tool like doc-gen for Lean 4 since this seems rather important to me, especially considering Lean 4 wants to be more of a general purpose language as well where you'd definitely want to have a nice way to explore documentation.

Now I've never messed with the lean compiler itself before and the original doc-gen mentions some PR that added additional APIs so they could actually access the docstrings so I'm wondering whether APIs like this already exist/whether there is a plan for them to exist.

[Mac]

In Lean 4, doc comments are a first class part of the syntax, so you can directly extract it from a declaration source.

[Mac]

In fact, a documentation generator for Lean 4 would likely only need to analyze the Syntax of a Lean file and not even worry about the elaborator or the compiler.

[Mac]

With the one caveat of likely needed to extract said syntax first from the elaboration Environment.

[Henrik Böving]

I'll try to do some digging regarding both of those types tomorrow then, thanks for the pointers!

[Mac]

I quickly whipped up this example which reads a file, elaborates it, and prints the doc string of a declaration:

Foo.lean

/-- Some comment -/
def foo := 0

Main.lean

import Lean
open Lean System

abbrev EnvM := StateM Environment

def EnvM.run' (env : Environment) (self : EnvM α) := StateT.run' self env |>.run

instance : MonadEnv EnvM where
  getEnv := get
  modifyEnv := modify

def printDocString (declName : Name) (path : FilePath) : IO PUnit := do
  let opts := Options.empty
  let mainModuleName := `main
  let input ← IO.FS.readFile path
  let (env, ok) ← Elab.runFrontend input opts path.toString mainModuleName
  unless ok do throw <| IO.userError "could not elaborate file"
  match EnvM.run' env <| findDocString? declName with
  | some docStr => IO.println docStr
  | none => throw <| IO.userError s!"no doc string found for '{declName}'"

#eval printDocString `foo "Foo.lean" -- prints "Some comment"

[Mac]

@Leonardo de Moura / @Sebastian Ullrich, could docStringExt be made public or, alternatively, could we get a findDocString? variant that operates on a explicitly specified Environment?

[Leonardo de Moura]

@Mac I just pushed the change.

[Mac]

@Leonardo de Moura Thanks! This also reminded me of a code style question I had been meaning to ask for a while: why are functions like findDocString?/getMainModuleDoc (and other env getters) not added to the Environment namespace so they can be used with dot notation?

[Leonardo de Moura]

@Mac It is what it is. We are focusing now on missing features, bugs, and porting Mathlib.
After we finish the porting, we can discuss these issues and try to make the API more consistent.

[Johan Commelin]

@Henrik Böving Note that @Eric Rodriguez has been working on a Lean 3 port of Alectryon: https://www.ma.imperial.ac.uk/~buzzard/xena/alectryon/ and https://www.ma.imperial.ac.uk/~buzzard/xena/alectryon/plain.lean.html
I think Eric can provide a lot more details than I can.

It would be great if a doc-gen tool for Lean 4 could have dedicated support for goal states and the "interactive" nature of Lean.

[Henrik Böving]

Oh that looks really cool as well! I'll keep it in the back of my head for sure for when the regular doc-gen stuff is working.

[Eric Rodriguez]

Sorry, just say this! I'm hoping that Alectryon for lean4 can become a defacto alternative for doc-gen, as it should be able to do everything we want, and some more nice stuff (say, custom rendererers for things like commutative diagrams in docstrings or even in the code, and as Johan mentioned interactive features). I haven't started looking at lean4 too deeply yet, but it seems a lot easier to work with than Lean3 in this regard so I have high hopes

[Henrik Böving]

I'll definitely try to have a look at it (however I'm rather a beginner with regular programming in Lean so that might take some time). And while the thing about the defacto alternative might surely be right for mathematical purposes Lean 4 is also supposed to be used by regular programmers and those want explorable documentation as is provided by doc-gen so I think a fusion of both is the correct way to go here.

[Scott Morrison]

@Eric Rodriguez, I'm actually a bit surprised that you're trying to produce documentation that captures the intermediate goal states of proofs. At least for Lean3 where we have lean-in-a-browser, isn't just linking to a live lean session in every way superior?

[Eric Rodriguez]

I mean, that's just how Alectryon is set up. I think it's got its advantages and disadvantages; for beginners, it makes it clearer where the bigger changes are; also, it will load far faster than the browser Lean/gitpod, and there's cool things that you can do that you couldn't do with the live setup (e.g. replace some Props in the tactic state with MathJax'd versions). However, there are many times I wish I had the flexibility of the server, too.

[Eric Wieser]

My understanding of Alectryon was that its primary goal was for exploring proofs, whereas doc-gen's primary goal is for exploring lemma statements. Am I underestimating the scope of Alectryon?

[Eric Rodriguez]

It's not too tough to extend it; put the proof in a spoiler bracket to indeed allow that, and format the docs with the other nice formatting tools that we have available to act as docs

[Eric Rodriguez]

I'm not too sure what's up with the full demo, but this is an example that hasn't been too far processed (in Coq, mind): https://alectryon-paper.github.io/bench/stdlib/theories/Lists/List.html

[Eric Rodriguez]

Extending that to better docstrings and generating a doc-gen-like-stub doesn't seem too far out of reach

[Patrick Massot]

I think it would be really nice to have something like Alectryon reading on Lean file and produce both doc-gen like documentation and fully interactive online file (including widgets) with a seamless transition.

[Kevin Buzzard]

Eric I think your summer project funding runs out at the end of Sept so looks like you have a lot to do ;-)

[Eric Rodriguez]

I do have a lot to do:) Exciting times!

[Chris Lovett]

Hey @Mac, I tried your code on the latest master bits, but it is not compiling, can you help me out?

image.png

[Mac]

@Chris Lovett Leo kindly improved the API so the following simpler example now works:

import Lean
open Lean System

def printDocString (declName : Name) (path : FilePath) : IO PUnit := do
  let opts := Options.empty
  let mainModuleName := `main
  let input ← IO.FS.readFile path
  let (env, ok) ← Elab.runFrontend input opts path.toString mainModuleName
  unless ok do throw <| IO.userError "could not elaborate file"
  match findDocString? env declName with
  | some docStr => IO.println docStr
  | none => throw <| IO.userError s!"no doc string found for '{declName}'"

#eval printDocString `foo "Foo.lean" -- prints "Some comment"

[Chris Lovett]

Thanks that works, and I figured out a slight variation that checks the name is actually defined:

def printDocString (declName : Name) (path : FilePath) : IO PUnit := do
    let opts := Options.empty
    let mainModuleName := `main
    let input ← IO.FS.readFile path
    let (env, ok) ← Elab.runFrontend input opts path.toString mainModuleName
    unless ok do throw <| IO.userError "could not elaborate file"
    if env.contains declName then
      let comment := (findDocString? env declName)
      IO.println comment
    else throw <| IO.userError s!"symbol '{declName}' not found"

I don't really care if the comment is 'none' - I care more than the symbol is not defined...

[Chris Lovett]

hey @Mac one more newby question, how do I get this getEnv to work for a version that looks up Lean defined doc comments?

def findLeanDocString (declName : Name) : IO String := do
    let env ← getEnv
    if env.contains declName then
      let comment := (findDocString? env declName)
      return comment.get!
    else
      return ""

Not sure what to do about the error failed to synthesize instance MonadEnv IO I see similar code containing let e ← getEnv all over the place in Lean sources so I'm not sure why it isn't working here...

[Chris Lovett]

Never mind, found the missing magic, I needed to add MetaM to the return types...

[Mac]

@Chris Lovett while that does work, that is doing something very different -- that is checking the environment of the running Lean interpreter instead, of as the example is doing, checking the environment of a newly elaborated file.

[Chris Lovett]

Right, that's what I want in this case, build lean.exe, then run this program using that new build and dump all the docs for that version of lean, that way I don't have to go searching for .lean source files.

[Henrik Böving]

Also since some people voiced interest in alectryon like visualization for lean4 proofs, I found this on Github today: https://github.com/insightmind/LeanInk

CC @Patrick Massot @Eric Rodriguez @Johan Commelin

[Johan Commelin]

Cool! @Niklas Bülow are you working with Sebastian?

[Henrik Böving]

Yeah sebastian is commenting in the issues, they definitely know of each other.

[Patrick Massot]

Yes, this work was mentioned before but the repo wasn't mentioned I think

[Sebastian Ullrich]

It wasn't there before :)

[Patrick Massot]

And how long did you believe you could hide it? :smiling_devil:

[Leonardo de Moura]

I loved the alias "insightmind" :)

[Niklas Bülow]

Thx, yeah LeanInk is basically a Lean 4 driver (written in Lean 4) for Alectryon. You'll still be using Alectryon directly to generate the webpages, etc. but Alectryon will use the driver to get some information about the Lean code. I'll be doing the project as my bachelor thesis, so Sebastian will support me on my way there. Our first goal is to get Lean 4 near feature-parity compared to Alectryon's Coq support. Afterward, we'll try to hopefully take advantage of some Lean 4 features to make it even more capable. So if you have some suggestions for features you'd like to see, feel free to share them with us. PS.: About hiding xD, Github Actions is just a lot more affordable when we're not trying to hide it :wink:

[Arthur Paulino]

Does anyone know if it is possible to make Read the Docs compatible with generic documentation generators (like doc-gen4) or is it committed to Python?

Edit: it's compatible with MkDocs but then I don't know if it's possible to write plugins that would allow MkDocs to process other languages :thinking:

[Henrik Böving]

Read the Docs is meant as a website to show documentation generated by Sphinx or just plain restructured text (for example the Linux kernel docs are hosted this way). You would probably have to hack Lean support into Sphinx in order to make this work, I don't really know how painful this would be.

Besides since Lean 4 is a fully fledged programming language on its own I don't think we have to rely on something like Read the Docs etc. I'm currently porting over the jinja2 templates from the original doc-gen to this JSX like syntax proposed over here https://github.com/leanprover/lean4/pull/723/files (fetching information from the compiler is already sort of working in the fork over here https://github.com/hargoniX/doc-gen4).

[Julian Berman]

I wrote a POC of using sphinx for Lean.

[Julian Berman]

But I haven't touched it in months.

[Julian Berman]

It's here https://github.com/Julian/sphinxcontrib-lean/ and Lean3 obviously

[Julian Berman]

You can see a result of it here: https://lean-across-the-board.readthedocs.io/en/latest/

[Arthur Paulino]

I was thinking more about the easiness of hosting and synchronization that Read the Docs allows. I mean, it is a business with adds and stuff, which allows them to keep the repo hooks online

[Arthur Paulino]

Julian, that was pretty rad :+1:

[Scott Morrison]

doc-gen4 won't build with nightly-2022-12-03 (due to changes in Lake; recBuildLocalModules has been removed)

[Scott Morrison]

@Henrik Böving

[Henrik Böving]

I fixed it just yesterday /o\

[Scott Morrison]

Sorry, just checking --- you mean you fixed something else, right? It's not compiling for me.

[Henrik Böving]

Yeah yeah I made it compatible with 11-30 yesterday. There was a relatively calm phase now because Mac didn't work much on Lake but when he does you can usually expect stuff to break on a daily or weekly basis until it eventually stabilizes

[Henrik Böving]

@Mac I'm not quite sure how to fix this here?

  let moduleJobs ← BuildJob.mixArray <| ← lib.recBuildLocalModules #[`docs]

I'm guessing i want something along the lines of what you are doing in LeanLib.recBuildStatic but specifically tailored to the docs module facet?

[Mac]

@Henrik Böving Oo! I forgot doc-gen4 was using recBuildLocalModules. Yeah, you got the idea right. With the new API the code would be:

let mods ← lib.modules.fetch
let moduleJobs ← BuildJob.mixArray <| ← mods.mapM (fetch <| ·.facet `docs)

The change was made to increase performance, so hopefully you might see a bit of a gain in doc-gen4 as well!

[Henrik Böving]

We shall see that right away!

[Henrik Böving]

@Scott Morrison builds now

[Matthew Ballard]

docs#Lean.findModuleOf? is giving me (declName : Lake.Name) as an argument but linking to Lean.Name

[Henrik Böving]

That's a known issue in Lean core

[Henrik Böving]

Mario noted down why it happens in a few days back in some topic here...

[Henrik Böving]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Confusing.20delaboration.20in.20.20doc-gen/near/388165262

[Yury G. Kudryashov]

Docs for docs#ContinuousSup don't show the instance for docs#TopologicalLattice extending this class.