Discussion: Functional Programming in Lean

Stream: general

[Mario Carneiro]

Discussion for #announce > "Functional Programming in Lean" update for Lean 4.18 @ 💬

[Mario Carneiro]

David Thrane Christiansen said:

The experience of reading it should be different, so please let me know if there's any regressions in your experience as a reader from the old version.

Dark mode?

[Mario Carneiro]

A bit more syntax highlighting would be good; the current version seems to be all black and white (is it optimized for print?)

[Mario Carneiro]

I also like it when code has a background which is visibly distinct from the body text

like here

[Chris Bailey]

What happened to the search functionality?

[David Thrane Christiansen]

I can get the quick-jump feature from the reference manual ported over pretty quickly. Full-text search would take a bit longer. Thanks, this is a good point.

[David Thrane Christiansen]

@Mario Carneiro Thanks :)

[Mario Carneiro]

@RalfJ reported to me that all the links appearing on google searches are now dead, such as https://lean-lang.org/functional_programming_in_lean/functor-applicative-monad/universes.html which has become https://lean-lang.org/functional_programming_in_lean/Functors___-Applicative-Functors___-and-Monads/Universes/#Functional-Programming-in-Lean--Functors___-Applicative-Functors___-and-Monads--Universes

[Shreyas Srinivas]

For what it is worth, I have never found google search useful for anything lean related. I always rely on loogle, moogle, leansearch, mathlib4_docs, zulip, discord, and the books directly

[ralfj]

apparently google would have been useful earlier this week when those links still worked^^

[ralfj]

it just creates unnecessary barriers for new people when things get moved around without setting up redirects

[ralfj]

(uh apparently I have two accounts here now, lol)

[Ching-Tsun Chou]

When will the search functionality in "Functional Programming in Lean" (https://lean-lang.org/functional_programming_in_lean/) be restored?

[Alexandre Rademaker]

A cleaner URL is also helpful when we want to share a particular page with others. A lengthy URL, such as the one below, is not user-friendly.

https://lean-lang.org/functional_programming_in_lean/Functors___-Applicative-Functors___-and-Monads/Universes/#Functional-Programming-in-Lean--Functors___-Applicative-Functors___-and-Monads--Universes

[David Thrane Christiansen]

Search should be there in about 3ish weeks - I'll be on vacation for the next two weeks, and getting the new full-text search upstreamed and working in FPiL and TPiL will be first on the list when I get back. In the meantime, site:lean-lang.org/functional_programming_in_lean/ works well in every search engine I've tried it with.