Zulip Chat Archive
Stream: general
Topic: website overview
Rob Lewis (Sep 01 2020 at 08:41):
The website build is broken again because of https://github.com/leanprover-community/mathlib/commit/551cf8e215a7d5194a77b906a197429717f919e8 , associates.prime no longer exists. Could someone update https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml ?
Rob Lewis (Sep 01 2020 at 08:41):
What do people think about moving the overview .yaml into mathlib so this stops happening?
Rob Lewis (Sep 01 2020 at 08:42):
It makes more sense to update the yaml file at the time the definitions change, than to notice post-hoc that the website build is broken and try to figure out why.
Johan Commelin (Sep 01 2020 at 08:44):
Rob Lewis said:
What do people think about moving the overview .yaml into mathlib so this stops happening?
I think this is really what we need to do.
Rob Lewis (Sep 01 2020 at 08:44):
cc @Patrick Massot / @Aaron Anderson
Patrick Massot (Sep 01 2020 at 08:48):
This is purely a CI/doc-gen question, so that's a question for Rob and Bryan.
Rob Lewis (Sep 01 2020 at 08:50):
It's a little roundabout, but I'd suggest this:
- move the overview, undergrad list, Freek list into mathlib with a CI script to check that all the declarations exist
- have doc-gen grab the yaml files and host them directly, no processing
- have the website build grab them from doc-gen along with the declaration info database
That way the database and yaml files should always be consistent.
Rob Lewis (Sep 01 2020 at 10:09):
https://github.com/leanprover-community/mathlib/tree/decl-lists should fail the tests stage if I did things right.
Rob Lewis (Sep 01 2020 at 10:13):
The failing entry is in the undergrad list, ring theory/divisibility in integral domains/prime nunbers. It was set to associates.prime but that got deleted. Should it just become prime?
Johan Commelin (Sep 01 2020 at 10:54):
Yes, I think so
Johan Commelin (Sep 01 2020 at 10:56):
https://github.com/leanprover-community/mathlib/commit/551cf8e215a7d5194a77b906a197429717f919e8 is the relevant commit
Rob Lewis (Sep 01 2020 at 11:24):
#4016 moves and fixes the yaml files. Then there's a doc-gen PR lined up, then a website PR
Johan Commelin (Sep 01 2020 at 11:34):
@Rob Lewis Thanks a lot for doing this!
Patrick Massot (Sep 01 2020 at 11:59):
I reviewed the python code.
Rob Lewis (Sep 01 2020 at 12:17):
Thanks, review addressed!
Patrick Massot (Sep 01 2020 at 12:29):
borsed
Bryan Gin-ge Chen (Sep 01 2020 at 13:24):
Seems like a good idea to me too, thanks Rob! Let me know if I can help with anything.
Rob Lewis (Sep 01 2020 at 14:39):
@Bryan Gin-ge Chen thanks for fixing the doc-gen PR! Now the website needs to be updated to pull the yaml files from there. Do you feel like doing that? If not I can later today.
Bryan Gin-ge Chen (Sep 01 2020 at 14:41):
I'm happy to do it, but it'd be later tonight if that's all right.
Rob Lewis (Sep 01 2020 at 14:43):
Of course, it's not exactly urgent, hah. I have some other things to do this afternoon too, let's see who gets there first.
Bryan Gin-ge Chen (Sep 01 2020 at 21:17):
@Rob Lewis FYI, I'm about to start working on this. Let me know if you've already got work in progress.
Rob Lewis (Sep 01 2020 at 21:19):
Nope, haven't had a chance, thanks!
Bryan Gin-ge Chen (Sep 01 2020 at 21:47):
@Rob Lewis https://github.com/leanprover-community/leanprover-community.github.io/pull/125
Patrick Massot (Jan 02 2021 at 21:31):
It would be nice to update the mathlib overview before the Lean Together workshop. There are instructions on how to do this on top of the webpage. I'm pretty sure a lot of new commutative algebra is missing for instance (Dedekind, DVR, Jacobson radical...).
Patrick Massot (Jan 02 2021 at 21:32):
And also some category theory probably.
Patrick Massot (Jan 02 2021 at 21:32):
@Bhavik Mehta
Eric Wieser (Jan 02 2021 at 21:35):
At least one of free- / tensor- / exterior- / clifford- algebras belong somewhere there, right? The last three could probably be linear algebra, but I'm not sure where to put the first
Patrick Massot (Jan 02 2021 at 21:39):
@Aaron Anderson, @Jalex Stark, @Kyle Miller , @Alena Gusakov I guess we could add some graph stuff too, right?
Patrick Massot (Jan 02 2021 at 21:39):
Tensor algebra already appears, right?
Patrick Massot (Jan 02 2021 at 21:40):
But free algebras and exterior algebras definitely need to go somewhere.
Eric Wieser (Jan 02 2021 at 21:42):
Huh, I guess that is already there, I guess it does slightly predate the other three. @Adam Topaz must have been ahead of the game. Done in #5579
Patrick Massot (Jan 02 2021 at 21:50):
Thanks! Could you use a lower case at the beginning of "exterior"?
Patrick Massot (Jan 02 2021 at 21:51):
Did you check you included all needed namespaces?
Eric Wieser (Jan 02 2021 at 22:00):
Yeah, they're unnamespaced
Eric Wieser (Jan 02 2021 at 22:01):
Whoops, I tried to lower-case that already but autocorrect had other ideas
Kyle Miller (Jan 02 2021 at 22:04):
Added a combinatorics section in #5581
Patrick Massot (Jan 02 2021 at 22:05):
Thanks! Could you switch to singular for consistency with the other categories?
Kyle Miller (Jan 02 2021 at 22:06):
For which one? pigeonhole principles?
Patrick Massot (Jan 02 2021 at 22:07):
No, that one is the only one that should stay plural.
Patrick Massot (Jan 02 2021 at 22:07):
I mean "simple graphs" -> "simple graph" etc.
Patrick Massot (Jan 02 2021 at 22:07):
(3 modifications)
Kyle Miller (Jan 02 2021 at 22:08):
Sure -- I think I managed to look at the two or three exceptions in the file when trying to figure out the convention
Patrick Massot (Jan 02 2021 at 22:08):
We may have inconsistencies, what are the examples you saw?
Eric Wieser (Jan 02 2021 at 22:09):
Also added docs#alternating_map in #5582, since there's precedent for listing those separately for bilinear forms.
Kyle Miller (Jan 02 2021 at 22:10):
Fixed. I looked at the "Affine and Euclidean geometry" section for guidance
Patrick Massot (Jan 02 2021 at 22:11):
Indeed that whole section is "wrong".
Patrick Massot (Jan 02 2021 at 22:11):
While you are editing this file, could you also fix that section?
Kyle Miller (Jan 02 2021 at 22:12):
Sure, I'll create a PR for it
Kyle Miller (Jan 02 2021 at 22:32):
#5583 normalizes the pluralizations for the whole file (hopefully I understood the convention correctly)
Patrick Massot (Jan 02 2021 at 22:34):
Wow, there are a lot of modifications actually. Did I dreamed up the convention?
Kyle Miller (Jan 02 2021 at 22:40):
It seems like most of the file followed the convention, and there didn't seem to be a good reason to make some things plural and others not.
Patrick Massot (Jan 02 2021 at 22:57):
Ok, thanks!
Eric Rodriguez (Aug 14 2023 at 23:23):
https://leanprover-community.github.io/mathlib-overview.html is currently broken - all the links don't work
Eric Wieser (Aug 14 2023 at 23:28):
Yes, this is a known issue caused by the doc-gen4 export files containing relative rather than the absolute links that the website scripts expect; it's relatively easy to fix the links on that page, but much more annoying on the 100 theorems page where we have to parse and modify the html snippets
Eric Wieser (Aug 14 2023 at 23:30):
The script lives in the website repository if anyone wants to have a go
Eric Wieser (Aug 21 2023 at 09:26):
https://github.com/leanprover-community/leanprover-community.github.io/pull/349 is most of the fix
Last updated: Dec 20 2023 at 11:08 UTC