Zulip Chat Archive

Stream: lean4 dev

Topic: nix help building docs


Chris Lovett (Sep 06 2022 at 18:10):

I need some Nix help to figure out why the new monad documentation is not building properly. I'm looking at doc/flake.nix, seems "examples" folder is handled specially, so perhaps I need to add monads = renderDir "monads" ./monads;, but I don't understand why renderLean is making an examples folder, perhaps that needs to be a variable name? Another special think seems to be on line 43 with cp -r ${examples}/* examples/ which I don't understand, and I don't understand why boiler plate *.lean.md files have to be checked in, is this also a Nix thing? Anyway, I would love to have this cleaned up and generalized by a Nix expert so that there is no special-casing and we can leaninkify any new folder in the future without having to touch this file.

Sebastian Ullrich (Sep 06 2022 at 19:15):

Okay, I've generalized it to build all .lean files in doc/. Which is way more than are actually reachable from the manual (see NFM2022/), but it's a matter of a few seconds of overhead.

Sebastian Ullrich (Sep 06 2022 at 19:15):

I don't understand why boiler plate *.lean.md files have to be checked in

As I said before, it is purely for the benefit of building the docs without LeanInk

Sebastian Ullrich (Sep 06 2022 at 19:17):

It also solves https://github.com/leanprover/LeanInk/issues/24 in a roundabout way now that I remember

Chris Lovett (Sep 06 2022 at 21:43):

Thanks for fixing it. https://leanprover.github.io/lean4/doc/monads/functors.lean.html looks good now.

Note that mdbook build works fine without the *.lean.md stub files, you just get blank pages there instead which is fine for those who don't want to use leanink.


Last updated: Dec 20 2023 at 11:08 UTC