Zulip Chat Archive

Stream: general

Topic: Generate documentation


view this post on Zulip Björn Fischer (Jun 20 2019 at 12:40):

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?

view this post on Zulip Reid Barton (Jun 20 2019 at 12:41):

I think it's just broken

view this post on Zulip Simon Hudon (Jun 20 2019 at 15:26):

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

view this post on Zulip Björn Fischer (Jun 20 2019 at 15:27):

@Reid Barton Thanks!

view this post on Zulip Björn Fischer (Jun 20 2019 at 15:28):

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

view this post on Zulip Simon Hudon (Jun 20 2019 at 15:32):

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

view this post on Zulip Simon Hudon (Jun 20 2019 at 15:52):

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

view this post on Zulip Björn Fischer (Jun 20 2019 at 15:55):

same behavior

view this post on Zulip matt rice (Jun 20 2019 at 18:54):

@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.

view this post on Zulip Björn Fischer (Jun 21 2019 at 09:05):

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

view this post on Zulip Patrick Massot (Jul 02 2019 at 14:01):

@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?

view this post on Zulip matt rice (Jul 02 2019 at 16:26):

@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

view this post on Zulip matt rice (Jul 02 2019 at 16:29):

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

view this post on Zulip Mario Carneiro (Jul 02 2019 at 16:32):

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

view this post on Zulip matt rice (Jul 02 2019 at 16:40):

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.

view this post on Zulip Patrick Massot (Jul 04 2019 at 13:04):

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

view this post on Zulip Patrick Massot (Jul 04 2019 at 13:09):

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?

view this post on Zulip Patrick Massot (Jul 04 2019 at 13:11):

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

view this post on Zulip Patrick Massot (Jul 04 2019 at 13:14):

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

view this post on Zulip matt rice (Jul 04 2019 at 15:23):

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.

view this post on Zulip Patrick Massot (Jul 04 2019 at 15:24):

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

view this post on Zulip Patrick Massot (Jul 04 2019 at 15:25):

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

view this post on Zulip matt rice (Jul 04 2019 at 15:26):

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?

view this post on Zulip Patrick Massot (Jul 04 2019 at 15:27):

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

view this post on Zulip matt rice (Jul 04 2019 at 15:27):

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

view this post on Zulip Patrick Massot (Jul 04 2019 at 15:28):

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

view this post on Zulip matt rice (Jul 04 2019 at 15:29):

Thanks, good idea.

view this post on Zulip matt rice (Jul 04 2019 at 18:09):

@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.

view this post on Zulip Wojciech Nawrocki (Jul 05 2019 at 20:53):

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).

view this post on Zulip matt rice (Jul 07 2019 at 21:12):

@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.

view this post on Zulip Wojciech Nawrocki (Jul 07 2019 at 21:19):

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.

view this post on Zulip Wojciech Nawrocki (Jul 07 2019 at 21:22):

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.

view this post on Zulip matt rice (Jul 07 2019 at 21:24):

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


Last updated: May 08 2021 at 10:12 UTC