Generate documentation for a specific version of mathlib

Stream: general

[Qzaac]

Hi everyone, I've been trying to generate the mathlib doc for the version I'm using (9a8dcb9be408e7ae8af9f6832c08c021007f40ec) with doc-gen however I'm still struggling.
I've clonned the repo and modified leanpkg.toml to replace it with the versions of Lean and mathlib I'm using. After that, I ran leanproject build (to download the right version of mathlib and create the olean files) but ./gen_docs just ran for 35 minutes and ended with an obscure error (see the full traceback below)...
Does anybody know how to solve this or how to get the mathlib doc for this specific version any other way ?

Traceback:
./gen_docs: line 36: 5873 Killed lean src/entrypoint.lean > export.json
Traceback (most recent call last):
File "print_docs.py", line 762, in <module>
main()
File "print_docs.py", line 749, in main
file_map, loc_map, notes, mod_docs, instances, tactic_docs = load_json()
File "print_docs.py", line 328, in load_json
decls = json.load(f, strict=False)
File "/usr/lib/python3.8/json/__init__.py", line 293, in load
return loads(fp.read(),
File "/usr/lib/python3.8/json/__init__.py", line 370, in loads
return cls(**kw).decode(s)
File "/usr/lib/python3.8/json/decoder.py", line 337, in decode
obj, end = self.raw_decode(s, idx=_w(s, 0).end())
File "/usr/lib/python3.8/json/decoder.py", line 355, in raw_decode
raise JSONDecodeError("Expecting value", s, err.value) from None
json.decoder.JSONDecodeError: Expecting value: line 1 column 1 (char 0)

[Rob Lewis]

Modern doc-gen might depend on features of mathlib/lean that were added since then. Try checking out an older version of doc-gen from around the same time as that commit?

[Rob Lewis]

You can also look in export.json and see if you can spot anything suspicious

[Qzaac]

Thank you for your answer. I tried the same process with an older version of doc gen (6252aff80b6a62e87c351123d90785a4d04f897f) which has been released a week after my version of mathlib but I got more or less the same error :

./gen_docs: line 36: 837 Killed lean src/entrypoint.lean > export.json
Traceback (most recent call last):
File "print_docs.py", line 747, in <module>
main()
File "print_docs.py", line 735, in main
file_map, loc_map, notes, mod_docs, instances, tactic_docs = load_json()
File "print_docs.py", line 322, in load_json
decls = json.load(f, strict=False)
File "/usr/lib/python3.8/json/__init__.py", line 293, in load
return loads(fp.read(),
File "/usr/lib/python3.8/json/__init__.py", line 370, in loads
return cls(**kw).decode(s)
File "/usr/lib/python3.8/json/decoder.py", line 337, in decode
obj, end = self.raw_decode(s, idx=_w(s, 0).end())
File "/usr/lib/python3.8/json/decoder.py", line 355, in raw_decode
raise JSONDecodeError("Expecting value", s, err.value) from None
json.decoder.JSONDecodeError: Expecting value: line 1 column 1 (char 0)

[Qzaac]

I also tried looking in export.json but the file is completely empty. However I realized there were issues during my leanproject build to, it seems like Lean doesn't know where to search a file called "all" (/home/qzaac/LEAN/doc-gen/src/entrypoint.lean:1:0: error: file 'all' not found in the search path). I tried changing the path but I don't know where this file might be...

Other errors follow, such as :
/home/qzaac/LEAN/doc-gen/src/export_json.lean:242:31: error: invalid field notation, 'instantiate_pis' is not a valid "field" because environment does not contain 'expr.instantiate_pis'
proj_tp
which has type
expr

I think they are a consequence of the broken import but I'm not sure.

[Rob Lewis]

Yes, to run doc-gen you need to generate all.lean in the mathlib dependency (https://github.com/leanprover-community/doc-gen/blob/master/gen_docs#L35). Run _target/deps/mathlib/scripts/mk_all.sh

[Rob Lewis]

You should do that and then call whatever Lean command the doc_gen executable calls. (It changed at some point -- might be lean --run src/export_json.lean, or lean src/entrypoint.lean, or something similar.)

[Eric Wieser]

What's your motivation for wanting to generate the docs at that specific version? Is it because you have a project of your own pinned to an old version? If so, I have a script on GitHub I can point you to that not only generates and uploads docs for a specific mathlib version, but does it for your own project code too.

[Jireh Loreaux]

@Eric Wieser I'd like to see that. Could be handy for pedagogy (i.e., if I design my own small library for students to use for a class).

[Eric Wieser]

It's at https://github.com/pygae/lean-ga/blob/master/.github/workflows/lean_doc.yml