Zulip Chat Archive

Stream: general

Topic: New website


view this post on Zulip Patrick Massot (May 11 2020 at 13:41):

There have been some work to redesign the Lean community website, trying to make is a bit more friendly. There are probably a couple of things that went weird in the migration, so don't hesitate to report things here or, even better, open a PR at the repository. Ideas about improving the website are also welcome (especially if they come as ready to merge pull requests). Also don't hesitate to add things to the bib file. Things tagged as either "about-lean", "about-mathlib" or "formalization" will appear on the papers page. You can also imitate Yury, Scott or Sébastien trying to beat leanprover-community-bot at mathlib commits speed (last graph of this page).

view this post on Zulip Jalex Stark (May 11 2020 at 13:56):

Wow! Even after hanging out here for a while I leaned several things

view this post on Zulip Patrick Massot (May 11 2020 at 13:57):

Good. I was thinking you will probably have ideas of things to add or tweak.

view this post on Zulip Kevin Buzzard (May 11 2020 at 13:59):

Hey this looks really good. Many thanks to whoever has done this. I was quite happy with the old version but this is even more user-friendly.

view this post on Zulip Kevin Buzzard (May 11 2020 at 14:11):

I wonder whether in "Formalized with Lean and mathlib" the last headline should be: "Independence of the continuum hypothesis" rather than just "the continuum hypothesis" (which could be interpreted as "definition of continuum hypothesis" or "proof of continuum hypothesis")

view this post on Zulip Kevin Buzzard (May 11 2020 at 14:12):

Why not "proof of cap set problem"?

view this post on Zulip Patrick Massot (May 11 2020 at 14:14):

Feel free to PR a change (maybe ask the authors of these formalizations first)

view this post on Zulip Kevin Buzzard (May 11 2020 at 14:15):

At https://leanprover-community.github.io/mathlib_stats.html there is Kenny Lau and kckennylau

view this post on Zulip Steffan (May 11 2020 at 14:16):

/me opens website and immediately says "Bootstrap!"

view this post on Zulip Steffan (May 11 2020 at 14:16):

Bootstrap websites look like bootstrap :P

view this post on Zulip Patrick Massot (May 11 2020 at 14:17):

Sure

view this post on Zulip Patrick Massot (May 11 2020 at 14:18):

Yeah, I'm also split in the statistics. That's because we have inconsistent git config across computers

view this post on Zulip Johan Commelin (May 11 2020 at 14:18):

At least it isn't http://contemporary-home-computing.org/prof-dr-style/

view this post on Zulip Johan Commelin (May 11 2020 at 14:18):

@Kevin Buzzard You will recognise a name on that page!

view this post on Zulip Patrick Massot (May 11 2020 at 14:19):

Steffan, the first message I sent to the other maintainers about that new website was:

I put all my web design science into one line:

wget https://github.com/twbs/bootstrap/archive/v4.4.1.zip

That's all I have

view this post on Zulip Steffan (May 11 2020 at 14:20):

Yep! Bootstrap is handy, not saying it's bad :)

view this post on Zulip Steffan (May 11 2020 at 14:21):

Especially when you don't want to bother with CSS

view this post on Zulip Steffan (May 11 2020 at 14:22):

I like Bulma better tho tbh

view this post on Zulip Patrick Massot (May 11 2020 at 14:25):

Feel free to PR a better design (I'm serious I don't care at all about bulma vs bootstrap)

view this post on Zulip Steffan (May 11 2020 at 14:38):

Maybe... I think I'll just make the dropdowns go on hover, so I can get rid of popper.js (get rid of extra bandwidth! :D). That's what I'll do, for now.

view this post on Zulip Sebastien Gouezel (May 11 2020 at 14:41):

Johan Commelin said:

At least it isn't http://contemporary-home-computing.org/prof-dr-style/

I don't see what's wrong with these pages! :)

view this post on Zulip Patrick Massot (May 11 2020 at 14:42):

Yours is not a true one Sébastien

view this post on Zulip Patrick Massot (May 11 2020 at 14:43):

The round border shouldn't be there

view this post on Zulip Patrick Massot (May 11 2020 at 14:43):

And the Annales Henri Lebesgue propaganda it totally out of style

view this post on Zulip Rob Lewis (May 11 2020 at 14:48):

Kevin Buzzard said:

Hey this looks really good. Many thanks to whoever has done this. I was quite happy with the old version but this is even more user-friendly.

"Whoever has done this" is @Patrick Massot , with @Bryan Gin-ge Chen setting up the GitHub integration. So let's direct our thanks in their directions :)

view this post on Zulip Shing Tak Lam (May 11 2020 at 14:49):

On https://leanprover-community.github.io/get_started.html

(although MacOS users will need to tell their system they really want to run it)

Should there be something similar for Windows? Since Microsoft Defender SmartScreen pops up with a warning.

view this post on Zulip Patrick Massot (May 11 2020 at 14:52):

I have no idea what should be said about Windows. Feel free to PR explanations

view this post on Zulip Shing Tak Lam (May 11 2020 at 14:59):

Gist of it is similar to what happens on MacOS.

There is a warning from Microsoft Defender when running the batch file. To allow it to run, select "More Info" then "Run anyway".

I'm happy to PR this once I figure out how it would fit into that paragraph.

view this post on Zulip Steffan (May 11 2020 at 17:47):

@Patrick Massot I submitted a PR btw.

view this post on Zulip Matt Earnshaw (May 11 2020 at 21:20):

in case it was not realised, stylesheet is broken on https://leanprover-community.github.io/archive/

view this post on Zulip Patrick Massot (May 11 2020 at 21:21):

oops

view this post on Zulip Patrick Massot (May 11 2020 at 21:21):

@Bryan Gin-ge Chen and @Rob Lewis do you understand what happens here?

view this post on Zulip Bryan Gin-ge Chen (May 11 2020 at 21:28):

archive/ is looking for https://leanprover-community.github.io/css/main.css which no longer exists in the new website. I'll see if I can add it back.

view this post on Zulip Alex J. Best (May 11 2020 at 21:28):

Looks like https://github.com/leanprover-community/archive/blob/master/_config.yml#L14 should have archive in?

view this post on Zulip Alex J. Best (May 11 2020 at 21:29):

As that baseurl is used to find https://leanprover-community.github.io/archive/css/main.css

view this post on Zulip Alex J. Best (May 11 2020 at 21:29):

If I manually edit the /archive/ path in it looks good.

view this post on Zulip Bryan Gin-ge Chen (May 11 2020 at 21:29):

Oh, that's probably a better solution. Do you mind making a PR?

view this post on Zulip Alex J. Best (May 11 2020 at 21:30):

sure, on it!

view this post on Zulip Alex J. Best (May 11 2020 at 21:34):

https://github.com/leanprover-community/archive/pull/1

view this post on Zulip Bryan Gin-ge Chen (May 11 2020 at 21:38):

I haven't set up Jekyll locally either so I also can't test it. In any case, it's probably a good idea to let @Rob Lewis take a look before merging.

view this post on Zulip Alex J. Best (May 11 2020 at 21:59):

https://alexjbest.github.io/archive/ shows the fixed version now, it looks like usual to me, but if people want to check too that would be great (note some links go to the official one so will still be broken).

view this post on Zulip Ryan Lahfa (May 11 2020 at 23:19):

Patrick Massot said:

Yeah, I'm also split in the statistics. That's because we have inconsistent git config across computers

You can maintain a mailmap to unify git stuff I think, something like this:

some name <some-mail> some alternative name <some-alternative-email> []

Git will then unify all names

view this post on Zulip Ryan Lahfa (May 11 2020 at 23:22):

Also, it looks super cool

view this post on Zulip Ryan Lahfa (May 11 2020 at 23:23):

Kudos to you, Patrick & Bryan!

view this post on Zulip Bryan Gin-ge Chen (May 11 2020 at 23:48):

I just made a cleaned up .mailmap for mathlib following this blog post. But now I'm a bit reluctant to add it to any of our repos since it contains everyone's email addresses. Of course, it doesn't contain anything which isn't available by just cloning the repo, so maybe some simple obfuscation will do.

view this post on Zulip Ryan Lahfa (May 12 2020 at 00:43):

Bryan Gin-ge Chen said:

I just made a cleaned up .mailmap for mathlib following this blog post. But now I'm a bit reluctant to add it to any of our repos since it contains everyone's email addresses. Of course, it doesn't contain anything which isn't available by just cloning the repo, so maybe some simple obfuscation will do.

Theorically, it's not that useful to obfuscate it: https://github.com/odoo/odoo/issues/13547
A maybe better way is to try to check if everyone is okay with those email addresses and ensure that people uses the correct emails addresses

view this post on Zulip Bryan Gin-ge Chen (May 12 2020 at 00:48):

I ended up going with a different solution. I committed the mailmap to a private repo under the leanprover-community org and gave access to the github actions workflow that generates the stats: mathlib_stats#2

view this post on Zulip Bryan Gin-ge Chen (May 12 2020 at 00:50):

I still think not making the mailmap so easily web-scrapable has some value, even if nothing there is really actually hidden.

view this post on Zulip Ryan Lahfa (May 12 2020 at 01:57):

That's a valid solution!

view this post on Zulip Ryan Lahfa (May 12 2020 at 02:00):

Does it deploy in realtime @Bryan Gin-ge Chen ? I don't see unification on Kenny nor Johan

view this post on Zulip Ryan Lahfa (May 12 2020 at 02:00):

ah it's a PR


Last updated: May 14 2021 at 22:15 UTC