## Stream: general

### Topic: New website

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

#### Jalex Stark (May 11 2020 at 13:56):

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

#### Patrick Massot (May 11 2020 at 13:57):

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

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

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

#### Kevin Buzzard (May 11 2020 at 14:12):

Why not "proof of cap set problem"?

#### Patrick Massot (May 11 2020 at 14:14):

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

#### Kevin Buzzard (May 11 2020 at 14:15):

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

#### Steffan (May 11 2020 at 14:16):

/me opens website and immediately says "Bootstrap!"

#### Steffan (May 11 2020 at 14:16):

Bootstrap websites look like bootstrap :P

Sure

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

#### Johan Commelin (May 11 2020 at 14:18):

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

#### Johan Commelin (May 11 2020 at 14:18):

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

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

That's all I have

#### Steffan (May 11 2020 at 14:20):

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

#### Steffan (May 11 2020 at 14:21):

Especially when you don't want to bother with CSS

#### Steffan (May 11 2020 at 14:22):

I like Bulma better tho tbh

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

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

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

#### Patrick Massot (May 11 2020 at 14:42):

Yours is not a true one Sébastien

#### Patrick Massot (May 11 2020 at 14:43):

The round border shouldn't be there

#### Patrick Massot (May 11 2020 at 14:43):

And the Annales Henri Lebesgue propaganda it totally out of style

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

#### Shing Tak Lam (May 11 2020 at 14:49):

(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 (May 11 2020 at 14:52):

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

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

#### Steffan (May 11 2020 at 17:47):

@Patrick Massot I submitted a PR btw.

#### Matt Earnshaw (May 11 2020 at 21:20):

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

oops

#### Patrick Massot (May 11 2020 at 21:21):

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

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

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

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

#### Alex J. Best (May 11 2020 at 21:29):

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

#### Bryan Gin-ge Chen (May 11 2020 at 21:29):

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

sure, on it!

#### Alex J. Best (May 11 2020 at 21:34):

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

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

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

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

#### Ryan Lahfa (May 11 2020 at 23:22):

Also, it looks super cool

#### Ryan Lahfa (May 11 2020 at 23:23):

Kudos to you, Patrick & Bryan!

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

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

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

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

#### Ryan Lahfa (May 12 2020 at 01:57):

That's a valid solution!

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

#### Ryan Lahfa (May 12 2020 at 02:00):

ah it's a PR

Last updated: May 14 2021 at 22:15 UTC