## 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?

Yes, I think so

#### 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.

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!

#### 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.

@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: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!

Last updated: May 11 2021 at 22:14 UTC