nix help building docs

Stream: lean4 dev

[Chris Lovett]

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]

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]

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]

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

[Chris Lovett]

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.