Generate documentation

Stream: general

[Björn Fischer]

I see there is a --doc command line argument in Lean. But when I try it the resulting file is entirely empty. Is there a trick to it? Or other options to generate docs?

[Reid Barton]

I think it's just broken

[Simon Hudon]

@Björn Fischer Can you file an issue on leanprover-community/lean?

[Björn Fischer]

@Reid Barton Thanks!

[Björn Fischer]

@Simon Hudon Sure! In the meantime, is there any working library to generate docs out there?

[Simon Hudon]

I know @matt rice is working on something but I don't know what the status is

[Simon Hudon]

What happens if you use

/-- docs for the win! -/
lemma abc : true := true.intro

instead of

/- docs for the win! -/
lemma abc : true := true.intro

[Björn Fischer]

same behavior

[matt rice]

@Björn Fischer The documentation generator i've been working on is here it currently works on linux, and can generate the mathlib documentation, the output could use some work (i.e. it doesn't yet output type information, and is sometimes not pretty). Haven't managed to test it on windows yet, the file path handling is subtle in a way that may lead to empty output.

[Björn Fischer]

@matt rice Awesome! Just tested it successfully on Linux.

[Patrick Massot]

@matt rice I tried to install lumpy-leandoc but the cargo command fails with message

error: failed to run custom build command for `tectonic v0.1.11`
process didn't exit successfully: `/tmp/cargo-installbDfJsx/release/build/tectonic-f11d59dd300c8949/build-script-build` (exit code: 101)
--- stderr
thread 'main' panicked at 'called `Result::unwrap()` on an `Err` value: Failure { command: "\"pkg-config\" \"--libs\" \"--cflags\" \"fontconfig harfbuzz >= 1.4 harfbuzz-icu icu-uc freetype2 graphite2 libpng zlib\"", output: Output { status: ExitStatus(ExitStatus(256)), stdout: "", stderr: "Package harfbuzz was not found in the pkg-config search path.\nPerhaps you should add the directory containing `harfbuzz.pc\'\nto the PKG_CONFIG_PATH environment variable\nNo package \'harfbuzz\' found\nPackage harfbuzz-icu was not found in the pkg-config search path.\nPerhaps you should add the directory containing `harfbuzz-icu.pc\'\nto the PKG_CONFIG_PATH environment variable\nNo package \'harfbuzz-icu\' found\nPackage graphite2 was not found in the pkg-config search path.\nPerhaps you should add the directory containing `graphite2.pc\'\nto the PKG_CONFIG_PATH environment variable\nNo package \'graphite2\' found\n" } }', src/libcore/result.rs:997:5
note: Run with `RUST_BACKTRACE=1` environment variable to display a backtrace.

warning: build failed, waiting for other jobs to finish...

This is using a freshly installed rust. I'm trying to flush my pile of cool things to look at (that's why I'm also pestering Bryan). Also is there any news regarding a more structure output than LaTeX? What about HTML output?

[matt rice]

@Patrick Massot It depends, which linux & what version, but with a new enough debian/ubuntu, apt-get install libharfbuzz-dev should bring in all the needed dependencies, there is work in a branch to build that at compile time if not available, but it's not ready yet

[matt rice]

As far as HTML output, it shouldn't be hard (in theory easier than latex), both the dependencies syntect and pulldown_cmark have functions to output HTML, the main issue is IIUC they want to output an entire html file per markdown which means a file per def which is an annoying number of files

[Mario Carneiro]

One file per def is not unreasonable if you are displaying proofs

[matt rice]

Well, if that is wanted it should be a fairly small patch...

Edit: I should clarify that this wouldn't give any of the inline TeX via KaTeX/MathJax, there is a plan for how to do it, but is a lot of work involved.

[Patrick Massot]

Thanks @matt rice installing libharfbuzz-dev was enough to compile lumpy-leandoc. I think it would help to add this to the README. Then I tried to run this on the perfectoid project using this Lumpy.toml:

[[documents]]
title = "Example"
file_name = "examples"
authors = ["Kevin Buzzard", "Johan Commelin", "Patrick Massot"]
src_dirs = ["src/."]
output_dir = "docs_out/"
output_formats = ["tex", "pdf"]
comment_format = "cmark"

The result was that lumpy-leandoc displayed

[2019-07-04T12:52:34Z INFO  lumpy_leandoc] Elapsed=921.888182ms, process lean
[2019-07-04T12:52:34Z INFO  lumpy_leandoc] Elapsed=647.134µs, sorting, sections examples.tex
[2019-07-04T12:52:34Z INFO  lumpy_leandoc] Elapsed=117.504µs, collating, sections examples.tex
[2019-07-04T12:52:34Z INFO  lumpy_leandoc] Elapsed=120.497µs, writing, examples.tex

then hanged for a very long time, but created some examples.tex. And after a long time:

[2019-07-04T13:00:37Z INFO  lumpy_leandoc] Elapsed=482.614324169s, generate, examples.pdf
Error: Error(Msg("the LaTeX engine failed"), State { next_error: Some(Error(EngineError("TeX"), State { next_error: Some(Error(Msg("halted on potentially-recoverable error as specified"), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })), backtrace: InternalBacktrace { backtrace: None } })), backtrace: InternalBacktrace { backtrace: None } })

Note that examples.tex is not correct because the author field was missing spaces after \and. After fixing this by hand, one can compile the tex file but it's almost empty: examples.pdf

[Patrick Massot]

Looking back at the example file in lumpy-leandoc, maybe the fact the output is almost empty is normal. I saw Lean code in the example, but that is actually also from the docstring. So we get only docstring in the output, right?

[Patrick Massot]

Is there any option to render also Lean code, at least definitions and statements?

[Patrick Massot]

Or maybe I completely misunderstood the project. I thought the idea was to get the analogue of math-comp.github.io/math-comp/htmldoc/mathcomp.field.galois.html

[matt rice]

Thanks, I will have a look at the error (and see if perhaps there isn't a timeout I can lessen), Currently it only output's docstrings and function names. I was going to include definitions by default (just haven't gotten to it yet), statements may not be possible as lean only allows docstrings on definitions as far as I can tell. I was planning on adding an "annotate = true" setting to the Lumpy.toml which would generate annotated sources such as you linked.

[Patrick Massot]

Ok, I'll be happy to test any new version, and I hope you'll get extra motivation from this

[Patrick Massot]

I also ordered a book about Rust, as it seems knowing Rust is more and more a prerequisite for using Lean

[matt rice]

Appreciate the feedback! Looking at the output it seemed like the index was filled with a lot of empty files with no docstrings, I should probably squelch those I imagine?

[Patrick Massot]

Indeed there are not very useful, except they remind us that we should write more docstrings!

[matt rice]

yeah, that's why i had left them in.

[Patrick Massot]

Maybe you could output a warning when running lumpy-leandoc, saying we should write docstrings, but remove them from the output document

[matt rice]

Thanks, good idea.

[matt rice]

@Patrick Massot I haven't been able to reproduce the long wait for that error message, It takes only a few seconds here, I'm wondering after fixing that do you still see the long runtime?

Edit: This appears to be an issue with the downloading of latex packages (perhaps a hosting issue), I reproduced it by removing ~/.cache/Tectonic.

[Wojciech Nawrocki]

I looked at this today and it turned out that almost all doc-generation infrastructure for --doc= is already there in Lean. It was only missing a few parts, so I added them in a PR. At the same time, I have no idea what I'm doing so this might well halt and catch fire (although it seems to work in my tests).

[matt rice]

@Wojciech Nawrocki Sorry for delay in responding to this, i have been attempting to compile mathlib w/ your patches but haven't had much luck. leanpkg build -- --doc=doc.json eventually uses up all my memory/swap and stops making any timely forward progress (completes without the --doc setting). Currently trying something like for file in $(find src -name "*.lean"); do lean --make $file --doc="$(basename $file .lean).leandoc_json"; done which if i got that right might finish.

[Wojciech Nawrocki]

Thanks! I'll look into the memory consumption issue. For now I'd advise against spending a lot of time testing these patches, since I simply coded the first thing that worked for simple test cases. Instead, I will now try to better understand how documentation_ext/module_ext are supposed to work and write something to match that.

[Wojciech Nawrocki]

Oh and yeah, currently lean --make --doc=doc.json will put O(n_docstrings_in_mathlib*n_modules_in_mathlib) fields in one file, which is completely unnecessary - it should only output docs for each module once. This is what I am looking into now.

[matt rice]

Ahh, I am mainly trying with mathlib since it has the most real docstrings to parse. Anyhow once i get some output to work with i'll try working on parsing the json in lumpy-leandoc