website

Stream: general

[Patrick Massot]

Jasmin Blanchette said:

"Lots of wonderful things on the community web site, all hidden under two layers of links." -- Anonymous (Gabriel E.)

I took time to map the website (using a small python script) links.pdf. I'm sure this will motivate people to work on this issue.

[Rob Lewis]

For indexing purposes, we should also generate a sitemap and file it with the relevant search engines, e.g. https://leanprover-community.github.io/mathlib_docs/sitemap.txt

[Patrick Massot]

Yes, but first we need a cleaner structure.

[Patrick Massot]

In particular decide something about https://leanprover-community.github.io/theories.html which is currently very hard to find

[Bryan Gin-ge Chen]

I think improving the links in the header (maybe including more and organizing them into menus?) will make a big difference.

[Patrick Massot]

Actually it looks like there are bugs in my script

[Patrick Massot]

There should be more links coming out of mathlib-overview

[Patrick Massot]

But I need to go for family chore now. I'll be back tonight.

[Mario Carneiro]

I assume the links aren't actually a tree?

[Mario Carneiro]

because that would be really weird

[Patrick Massot]

I'm back with a less bad approximation: links.pdf

[Patrick Massot]

The trouble is I reused an old script whose purpose was to detect dead links without rechecking multiple times the same file, so I ended up with a covering tree.

[Patrick Massot]

This graph really makes me wonder how people can still fail to meet https://leanprover-community.github.io/install/project.html

[Patrick Massot]

Maybe we should tweak the site building script so that it adds a link to that page every two lines.

[Patrick Massot]

Or maybe have some javascript trickery that redirects the first ten requests from a given IP to this page.

[Jiekai]

Patrick Massot said:

Or maybe have some javascript trickery that redirects the first ten requests from a given IP to this page.

That sounds too much trickery.

[Shing Tak Lam]

Patrick Massot said:

This graph really makes me wonder how people can still fail to meet https://leanprover-community.github.io/install/project.html

Right now it's just a link at the bottom of the install pages and it's quite easy to miss. Might be worth promoting it to an <h3> with it's own section or something like that so people are less likely to miss it.

[Madeleine Sydney]

hello! i was encouraged to forward some criticisms from the functional programming discord server to this channel:
TL;DR: a few of us believe that lean's landing page should tell you more about what lean is about, and why you should be interested.

madeleine sydney: the new site feels very much like corporate testimonial-buzzword-soup. little is said about lean itself. if this were my first impression of lean, i would immediately lose most or all potential interest. based off the landing page, i see generic statement about lean does (personally, i have learned to discard these testimonials and news articles as meaningless), and i see a single sentence about what lean is: 1. a functional programming language 2. open source; neither of these things are what sets lean apart.

madeleine sydney: i would compare this with https://haskell.org/, which includes a similar one-sentence description of the language, but uses few more keywords for detail; a snippet of some real haskell code; a repl with a brief tutorial and some example expressions; then the testimonials and videos; and most importantly, a list of features that make haskell unique.

madeleine sydney: i think a simplified explanation of how lean offers you "trust, efficiency, and extensibility" (dependent types, a fancy compiler, and macros) would do a lot. some example code is the equivalent of a novel's hook. haskell's prime snippet is incredibly alluring — i first saw it as a C programmer, and thought "is that an infinite sequence? they say it's statically typed, but i don't see any types! set builder notation?" a brief tour of the language can give the reader a lot. the new site tells me next to nothing about why i should be interested in lean. just a couple quick summaries could fix that, in my opinion.

GalacticColourisation: it looks like it's marketing lean for managers or something rather than programmers

madeleine sydney: exactly! perhaps that's valuable for something, but all i can say is that it disgusts me, as a programmer. if i, the lean-unaware reader, could be bothered to venture further into the "learn" tab, i'm slapped with a selection of books and (unfinished) manuals.

Jack o Lantern: the new website feel like a CRM website, filled with corporate buzzwords, in the news is just AI, there is three testimonies but you can move them left and right for some reasons

[Notification Bot]

A message was moved here from #general > Website by Madeleine Sydney.

[Asei Inoue]

icon issue in mobile still exists.

FAA2690F-EB4E-4928-A2DE-7EC0230F2CDA.jpg

[Asei Inoue]

text displaying issue in iOS safari

51D4CC0E-7E30-44DF-A456-7BF5935088E4.jpg

[Naruyoko]

iPad; Chrome
IMG_1361.jpeg

[Naruyoko]

Also, why do the buttons on the "Learn" page have just slightly different label than the name of the thing they link to?

[Bharat Bhat]

Thanks so much for the input on the website. We are looking through all your feedback and seeing how we can address the topics and recommendations shared here. Please stay tuned for updates.

[mars0i]

I like the new website! Is this the place for further suggestions, or is there a better place?

If it's here, here are some minor suggestions:

• On the "Learn" page, FPIL is described as "standard reference", but it's not a reference; it's textbook or tutorial. It's also doesn't seem like it's the standard resource for people whose primary goal is learning to prove theorems. :smile:
• I personally would favor adding the API documentation (https://leanprover-community.github.io/mathlib4_docs/) under "Tools". Loogle and Moogle are already there, and the Lean Community page that's linked has a link to the API docs, but the API page has its own benefits. For example, you can browse the libraries, menu-style, on the left. (I wanted to know what sorts of map data structures were available in standard libraries. Searching on possible function names was less useful than clicking on libraries to see whether they had a Data module, and then checking inside it.)

[Niels Voss]

I would personally like to see at least one snippet of Lean code near the top of the home page, kind of like the Haskell website, preferably something that few other languages can do (for example, indexing a list using Fin to guarantee at compile time that we have a valid index, or proving a List sorting function is correct). That's just a suggestion though

[Niels Voss]

Perhaps it might even be a good idea to have a whole page dedicated to examples of Lean code (although that sounds like a lot of work to create, and it probably wouldn't be as important as an example on the home page)

[Shreyas Srinivas]

This is a more content intensive feature request, but one that lean could really benefit from, if we can replicate this cookbook feature of ocaml's website: https://ocaml.org/cookbook

[Shreyas Srinivas]

A lot of the frequently asked questions on Zulip and their answers can be turned into a cookbook format

[Shreyas Srinivas]

For example the termination_by and decreasing_by proofs, some metaprogramming snippets,

[Sebastian Ullrich]

Hey all, after taking all your helpful feedback above into account, we have decided to revert to the old design. Once DNS is updated, you should see the familiar website with some minor textual changes backported. Look forward to similar small refinements addressing further feedback in the near future.

[Sofia Rodrigues]

When I think about a programming language website, I think something like this:
image.png

[Sofia Rodrigues]

I’m not a designer, so it probably has a bunch of issues, but this idea was stuck in my head for days, and I just had to share it.

[Shreyas Srinivas]

Is there a higher res image?

[Sofia Rodrigues]

Shreyas Srinivas said:

Is there a higher res image?

I have the figma that I can share, It's just an incomplete sketch though.

https://www.figma.com/design/1GrVmNKUTpoPpyGMoD7KjU/Lean-Lang?node-id=1-3&t=epKSbf3g3K03ABW2-1

[Shreyas Srinivas]

This design is really neat. The navbar is not intrusive, everything is well spaced. The font seems nice. We could use a slightly brighter shade of blue, but I personally find it a huge improvement over the previous new website, as well as the current one (which is also nice).

[Shreyas Srinivas]

The brighter colour with a bit more red will allow it to blend well in dark mode as well.

[Shreyas Srinivas]

In that code snippet we should put up a statement of FLT, a sorry, and a comment that "We have a truly marvelous proof that the code box is too narrow to contain" (borrowed from the FLT channel).

[Sofia Rodrigues]

Shreyas, now you have permission to edit the figma file, feel free to edit whatever u want.

[Shreyas Srinivas]

Thanks

[Utensil Song]

This is really a neat design.

As Shreyas Srinivas has shared earlier, brand color choice is important. Developers usually come with a health level of OCPD, and are somewhat sensitive to syntax-highlighting themes. Such an audience could build their impression on theming choice to quite an extent, just like their preference on syntax and other tiny details affecting ergonomics.

I like the original Lean design (black and white) which conveys a certain sense of a mathematical paper, which suits Lean as a theorem prover. I also like @Sofia Rodrigues 's choice of blue, it conveys a sense of refreshing and at the same time steady, which suits Lean as both a programming language (a sense of friendly to use) and a theorem prover (a sense of thoroughly considered). The overall design is clean, via proper layout and spacing.

As someone who naturally assigns colors to numbers and symbols since childhood, I have been wondering which color was my impression of Lean since the last iteration of website, I don't have an immediate answer. After seeing this design, I can also relate to this choice of blue, with the blue squiggly line of tactics like aesop?, which suits Lean as equipping more and more automation.

[Utensil Song]

About the choice of code snippet, maybe it could be a piece of functional programming plus a concise proof of its property using a bit of automation?

Writing such a snippet to fit in the code box, and particularly the width of mobile (notice that the current code snippet overflows on mobile) is an interesting challenge.

[Utensil Song]

The short explanation of “Trust” is on point, its improvements and what to write for “Efficiency” and “Extensibility” are left as exercises. :wink: