Zulip Chat Archive

Stream: std4

Topic: documentation efforts


Adrien Champion (Oct 18 2022 at 08:44):

I would be interested in contributing to std4 and I think (re-)writing documentation is a good place to start. We can discuss this during the mentoring sessions, but maybe mentors could point to places where better/additional doc would be useful

Adrien Champion (Oct 18 2022 at 08:45):

And/or have github issues with a doc tag so that we can close them when they're done

Adrien Champion (Oct 18 2022 at 17:29):

  • [ ] add top-level module doc, including main definitions, possibly implementation details, and search-engine-related tags

Adrien Champion (Oct 25 2022 at 14:16):

Regarding documentation efforts, maybe it would be a good idea to add doc-gen4 to the lakefile.lean, so that we can build and inspect the doc as we improve it.

Should I open an issue and PR this?

Adrien Champion (Oct 25 2022 at 14:19):

Actually, doc-gen4 (and std4 it seems) do not compile on macos M1, so maybe not

Henrik Böving (Oct 25 2022 at 15:41):

What's the errors?

Adrien Champion (Oct 25 2022 at 16:02):

Here are the std4 errors, with [...] to remove similar errors so that it abides by Zulip's character constraints

output

Adrien Champion (Oct 25 2022 at 17:48):

So this comes from running on macos M1, where Lean's linking fails. This causes failures on FFI, which Std4 does not have, but the linter is a default target and does trigger this problem

Adrien Champion (Oct 25 2022 at 18:35):

lake build Std works fine, as pointed out by Mac

Adrien Champion (Oct 26 2022 at 07:22):

See also https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/elan.20toolchains.20broken.20on.20macos.20M1/near/306122168


Last updated: Dec 20 2023 at 11:08 UTC