FAQ

Stream: general

[Eric Rodriguez]

On the Xena discord, I and some others have been working on a FAQ for Lean/mathlib based issues, and it is located here. I'm more than happy to move this to some other system, but I think it'd be useful to help answer some features. It's (currently) hosted on Github's wiki feature, so anyone should be able to edit it, but if people would like me to add anything, please let me know! I hope this is helpful for common questions :)

[Mario Carneiro]

I think this should be relocated to the leanprover-community web site

[Eric Wieser]

I think leaving it around as a wiki for a week or so might be a good way to collect entries before cleaning them up for the website

[Eric Rodriguez]

this has now expanded a little - any questions I've missed? Bhavik's been tagging me in a lot of FAQs, but I probably missed some due to too-many-notifications. Otherwise I think it'd be nice to start moving this to the main website, and allowing zulip linkification: it'd be nice to just be able to reply to something with sth like "See faq#div_zero".

[Bhavik Mehta]

I think you caught all of mine! I'm sure others might have ideas though :)

[Julian Berman]

It's not a separate question, but maybe as part of moving it it's worth interlinking some terms to the glossary (and creating issues to define any that seem like they should be linked but don't exist yet)

[Julian Berman]

People reading one may be audience for the other

[Julian Berman]

I just dumped a few more onto the todo page too, in case any of those look worthy of addressing