Zulip Chat Archive

Stream: lean4

Topic: doc-gen4


Henrik Böving (Sep 21 2021 at 23:43):

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 (Sep 21 2021 at 23:45):

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

Mac (Sep 21 2021 at 23:45):

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 (Sep 21 2021 at 23:46):

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

Henrik Böving (Sep 21 2021 at 23:54):

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

Mac (Sep 22 2021 at 00:10):

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 (Sep 22 2021 at 00:19):

@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 (Sep 22 2021 at 00:30):

@Mac I just pushed the change.

Mac (Sep 22 2021 at 01:09):

@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 (Sep 22 2021 at 01:26):

@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 (Sep 22 2021 at 04:22):

@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 (Sep 22 2021 at 10:21):

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 (Sep 24 2021 at 10:10):

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 (Sep 24 2021 at 10:30):

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 (Sep 24 2021 at 10:46):

@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 (Sep 24 2021 at 10:48):

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 (Sep 24 2021 at 11:45):

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 (Sep 24 2021 at 11:46):

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 (Sep 24 2021 at 11:48):

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 (Sep 24 2021 at 11:50):

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

Patrick Massot (Sep 24 2021 at 12:10):

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 (Sep 24 2021 at 13:36):

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 (Sep 24 2021 at 13:38):

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

Chris Lovett (Nov 02 2021 at 23:11):

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

image.png

Mac (Nov 02 2021 at 23:16):

@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 (Nov 03 2021 at 00:17):

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 (Nov 03 2021 at 00:57):

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 (Nov 03 2021 at 01:03):

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

Mac (Nov 03 2021 at 01:16):

@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 (Nov 03 2021 at 01:24):

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 (Nov 03 2021 at 19:31):

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 (Nov 03 2021 at 19:32):

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

Henrik Böving (Nov 03 2021 at 19:33):

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

Patrick Massot (Nov 03 2021 at 20:11):

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

Sebastian Ullrich (Nov 03 2021 at 20:58):

It wasn't there before :)

Patrick Massot (Nov 03 2021 at 21:10):

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

Leonardo de Moura (Nov 03 2021 at 21:11):

I loved the alias "insightmind" :)

Niklas Bülow (Nov 03 2021 at 22:41):

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 (Dec 10 2021 at 15:17):

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 (Dec 10 2021 at 15:41):

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 (Dec 10 2021 at 15:47):

I wrote a POC of using sphinx for Lean.

Julian Berman (Dec 10 2021 at 15:47):

But I haven't touched it in months.

Julian Berman (Dec 10 2021 at 15:47):

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

Julian Berman (Dec 10 2021 at 15:48):

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

Arthur Paulino (Dec 10 2021 at 15:50):

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 (Dec 10 2021 at 15:54):

Julian, that was pretty rad :+1:

Scott Morrison (Dec 03 2022 at 13:06):

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

Scott Morrison (Dec 03 2022 at 13:07):

@Henrik Böving

Henrik Böving (Dec 03 2022 at 13:07):

I fixed it just yesterday /o\

Scott Morrison (Dec 03 2022 at 13:15):

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

Henrik Böving (Dec 03 2022 at 13:16):

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 (Dec 03 2022 at 13:23):

@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 (Dec 03 2022 at 16:35):

@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 (Dec 03 2022 at 16:35):

We shall see that right away!

Henrik Böving (Dec 03 2022 at 16:54):

@Scott Morrison builds now

Matthew Ballard (Sep 04 2023 at 19:55):

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

Henrik Böving (Sep 04 2023 at 20:11):

That's a known issue in Lean core

Henrik Böving (Sep 04 2023 at 20:11):

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

Henrik Böving (Sep 04 2023 at 20:12):

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

Yury G. Kudryashov (Nov 03 2023 at 02:14):

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


Last updated: Dec 20 2023 at 11:08 UTC