New website

Stream: general

[Patrick Massot]

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

[Jalex Stark]

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

[Patrick Massot]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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")

[Kevin Buzzard]

Why not "proof of cap set problem"?

[Patrick Massot]

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

[Kevin Buzzard]

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

[Steffan]

/me opens website and immediately says "Bootstrap!"

[Steffan]

Bootstrap websites look like bootstrap :P

[Patrick Massot]

Sure

[Patrick Massot]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Steffan]

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

[Steffan]

Especially when you don't want to bother with CSS

[Steffan]

I like Bulma better tho tbh

[Patrick Massot]

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

[Steffan]

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.

[Sebastien Gouezel]

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

[Patrick Massot]

Yours is not a true one Sébastien

[Patrick Massot]

The round border shouldn't be there

[Patrick Massot]

And the Annales Henri Lebesgue propaganda it totally out of style

[Rob Lewis]

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 :)

[Shing Tak Lam]

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.

[Patrick Massot]

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

[Shing Tak Lam]

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.

[Steffan]

@Patrick Massot I submitted a PR btw.

[Matt Earnshaw]

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

[Patrick Massot]

oops

[Patrick Massot]

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

[Bryan Gin-ge Chen]

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.

[Alex J. Best]

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

[Alex J. Best]

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

[Alex J. Best]

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

[Bryan Gin-ge Chen]

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

[Alex J. Best]

sure, on it!

[Alex J. Best]

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

[Bryan Gin-ge Chen]

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.

[Alex J. Best]

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

[Ryan Lahfa]

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

[Ryan Lahfa]

Also, it looks super cool

[Ryan Lahfa]

Kudos to you, Patrick & Bryan!

[Bryan Gin-ge Chen]

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.

[Ryan Lahfa]

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

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Ryan Lahfa]

That's a valid solution!

[Ryan Lahfa]

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

[Ryan Lahfa]

ah it's a PR