Zulip Chat Archive

Stream: general

Topic: website overview


view this post on Zulip 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 ?

view this post on Zulip Rob Lewis (Sep 01 2020 at 08:41):

What do people think about moving the overview .yaml into mathlib so this stops happening?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Sep 01 2020 at 08:44):

cc @Patrick Massot / @Aaron Anderson

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Sep 01 2020 at 10:54):

Yes, I think so

view this post on Zulip Johan Commelin (Sep 01 2020 at 10:56):

https://github.com/leanprover-community/mathlib/commit/551cf8e215a7d5194a77b906a197429717f919e8 is the relevant commit

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 01 2020 at 11:34):

@Rob Lewis Thanks a lot for doing this!

view this post on Zulip Patrick Massot (Sep 01 2020 at 11:59):

I reviewed the python code.

view this post on Zulip Rob Lewis (Sep 01 2020 at 12:17):

Thanks, review addressed!

view this post on Zulip Patrick Massot (Sep 01 2020 at 12:29):

borsed

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Sep 01 2020 at 21:19):

Nope, haven't had a chance, thanks!

view this post on Zulip Bryan Gin-ge Chen (Sep 01 2020 at 21:47):

@Rob Lewis https://github.com/leanprover-community/leanprover-community.github.io/pull/125

view this post on Zulip 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...).

view this post on Zulip Patrick Massot (Jan 02 2021 at 21:32):

And also some category theory probably.

view this post on Zulip Patrick Massot (Jan 02 2021 at 21:32):

@Bhavik Mehta

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jan 02 2021 at 21:39):

Tensor algebra already appears, right?

view this post on Zulip Patrick Massot (Jan 02 2021 at 21:40):

But free algebras and exterior algebras definitely need to go somewhere.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jan 02 2021 at 21:50):

Thanks! Could you use a lower case at the beginning of "exterior"?

view this post on Zulip Patrick Massot (Jan 02 2021 at 21:51):

Did you check you included all needed namespaces?

view this post on Zulip Eric Wieser (Jan 02 2021 at 22:00):

Yeah, they're unnamespaced

view this post on Zulip Eric Wieser (Jan 02 2021 at 22:01):

Whoops, I tried to lower-case that already but autocorrect had other ideas

view this post on Zulip Kyle Miller (Jan 02 2021 at 22:04):

Added a combinatorics section in #5581

view this post on Zulip Patrick Massot (Jan 02 2021 at 22:05):

Thanks! Could you switch to singular for consistency with the other categories?

view this post on Zulip Kyle Miller (Jan 02 2021 at 22:06):

For which one? pigeonhole principles?

view this post on Zulip Patrick Massot (Jan 02 2021 at 22:07):

No, that one is the only one that should stay plural.

view this post on Zulip Patrick Massot (Jan 02 2021 at 22:07):

I mean "simple graphs" -> "simple graph" etc.

view this post on Zulip Patrick Massot (Jan 02 2021 at 22:07):

(3 modifications)

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jan 02 2021 at 22:08):

We may have inconsistencies, what are the examples you saw?

view this post on Zulip 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.

view this post on Zulip Kyle Miller (Jan 02 2021 at 22:10):

Fixed. I looked at the "Affine and Euclidean geometry" section for guidance

view this post on Zulip Patrick Massot (Jan 02 2021 at 22:11):

Indeed that whole section is "wrong".

view this post on Zulip Patrick Massot (Jan 02 2021 at 22:11):

While you are editing this file, could you also fix that section?

view this post on Zulip Kyle Miller (Jan 02 2021 at 22:12):

Sure, I'll create a PR for it

view this post on Zulip Kyle Miller (Jan 02 2021 at 22:32):

#5583 normalizes the pluralizations for the whole file (hopefully I understood the convention correctly)

view this post on Zulip Patrick Massot (Jan 02 2021 at 22:34):

Wow, there are a lot of modifications actually. Did I dreamed up the convention?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jan 02 2021 at 22:57):

Ok, thanks!


Last updated: May 11 2021 at 22:14 UTC