Printable form of language reference?

Stream: new members

[Hannah]

Hi all. Is there a PDF or otherwise printable form of the Lean language reference? The web version is impossible to print in any sensible format, and I am not good enough at Lean yet to understand how to turn the source code into something useful for me - this seems like low-hanging fruit for lowering the barrier to entry for new people! Thanks.

[Kyle Miller]

David's mentioned that it's a goal, but not a short-term one: #general > A plea from a newbie concerning future Unicode use @ 💬

The lowest-hanging fruit so far has been the writing of the reference

[Hannah]

I'm not sure I understand. Does the Lean reference really only exist in this custom file format, which can be read only by this unfinished piece of software, which requires knowledge of Lean to use? And has no export features, compatibility with other document formats, accessibility options, and so on? Baffling, if so. Thanks.

[Kyle Miller]

Yes, it is a custom format being developed by the Lean FRO to support rich interactive documents.

No, you do not need to understand Lean to be able to read the documentation online.

[Hannah]

Sure, but I'm not asking how to read it online: that's not an option for me. I'm asking how to print it. What do I need to understand to make this document printable?

[Kyle Miller]

You need to understand that David will have this feature at some point, that's all. (Edit: At least this is my understanding, I could be mistaken.)

[Kyle Miller]

(The last sentence of my comment before the last one is not completely fair, sorry. I just don't like to see anyone pop in and be 'baffled' about other people's design decisions. There's a lot of neat stuff about Verso, but both it and the Lean Language Reference are works in progress.)

[Kyle Miller]

I'm sorry I don't have any better answer. Maybe @David Thrane Christiansen has something that could help in the short term.

[Hannah]

Kyle Miller said:

(The last sentence of my comment before the last one is not completely fair, sorry. I just don't like to see anyone pop in and be 'baffled' about other people's design decisions. There's a lot of neat stuff about Verso, but both it and the Lean Language Reference are works in progress.)

I understand the defensiveness. I don't want to make unreasonable demands of a community that I'm not even really a part of yet. I know it's a huge amount of effort, and a long and thankless slog, to make something new and cool that works well, and I commend the effort. But, right now, a key document of the community has been released only in a niche format that lacks the most basic accessibility features, and that is a baffling choice to me. I'm sure I'll love Verso once it's feature-complete, but until then, I would love a parallel version in any format I could actually work with. Markdown, Word, PDF, LaTeX, anything at all.

[David Thrane Christiansen]

Can you say a bit more about how the current HTML is lacking accessibility?

My understanding was that most screen readers and other assistive technology worked better with HTML than most other formats, but if there's anything that can be improved there, then it's certainly worth doing.

[Hannah]

David Thrane Christiansen said:

Can you say a bit more about how the current HTML is lacking accessibility?

My understanding was that most screen readers and other assistive technology worked better with HTML than most other formats, but if there's anything that can be improved there, then it's certainly worth doing.

Hi David. I don't use a screenreader, so I can't comment on that. But as a simple illustration of how I usually navigate documents on a computer: have you tried increasing the font size? When I do this, the (non-resizable) left-hand menu takes up half of the screen, the lines of code don't wrap, the huge tooltips take over the whole screen, and most importantly, they regularly run off the screen (sometimes up, sometimes down), and sometimes don't have the necessary horizontal / vertical scrollbars for me to be able to read them in full. If I increase or decrease the font size to try to read a tooltip or a line of code, it jumps randomly around the page, so I lose what I was reading and have to search for it again.

I do see what you're going for here, and I love the idea, but I find myself constantly clicking and dragging and scrolling and zooming just to get through a single paragraph, because they're so densely packed with custom artefacts (all the various wavy and dotted lines and pill icons, which all seem to indicate tooltips of various kinds). I've added a few screenshots. I can't speak to everyone's needs: what I can say is that people are typically very good at adapting documents to their own needs if you let them, and this uneditable custom format without any export options prevents that.
image.png
image.png
image.png
image.png

[David Thrane Christiansen]

Thanks, this is very helpful feedback! I'm sorry for the frustration that this is causing. I think these specific issues can be addressed fairly quickly. As I see it, the following would take care of the biggest problems you're describing:

1. Make it easier to get the table of contents out of the way, either by adjusting the width threshold at which it is hidden or by adding a toggle.
2. Make it possible to disable the tooltips or make them less likely to accidentally trigger (e.g. via requiring a click).
3. Ensure that the tooltips never exceed the size of the viewport.

It's not the solution you're asking for, but would it help?

As far as generating other output formats, that's certainly something on the todo list, but it's not planned in the next few months.

In the very short term, it might be useful for you to zoom in a bit further, which triggers the alternative layout where the table of contents is hidden. This doesn't address the other issues you're experiencing, but I hope it's better than nothing for now:

Screenshot 2025-05-27 at 11.16.11.png
Screenshot 2025-05-27 at 11.17.11.png

[Hannah]

Thanks! On your suggestions: number 1 sounds helpful, and I'm sure 2 would be helpful to some people too. 3 is really the key thing for me: I don't want the tooltips disabled, because they clearly contain a huge amount of important information, so I just want them somewhere I can read them. My ideal situation is that they occur in the text itself (in a box or something), but ensuring that they don't exceed the size of the viewport, that they choose a sensible direction to appear (e.g. not opening downwards when my mouse is over a link at the bottom of the page, or upwards at the top), and that they have scrollbars when necessary would be a huge improvement, thanks.

One other suggestion, which may or may not be easy to implement: can there be a way of expanding the whole document and viewing it all on one page, rather than having to click through sections on the menu? That's not perfect either (it might mean I have to forego the tooltips), but I could then copy and paste the document into Word and print it from there.

[David Thrane Christiansen]

The contents of the tooltips mostly already occur in the text, because they're the signatures and API docs of the Lean library. Those that don't yet occur are on their way. Clicking a name should jump you right to its documentation and signature. The tooltips are really intended to be an extra redundant way to get to this information, without the overhead of clicking a link and leaving a context, rather than the primary source of it.

The document can be rendered as a single HTML page. That mode has a few issues for ordinary browsing, which is why it's not published anywhere, but you can build it by checking out the manual repository and running lake exe generate-manual --without-html-multi --with-html-single. If that causes you any difficulties, let me know, and I can send you a zip file.

[David Thrane Christiansen]

A word of warning: the document is about 221,000 words of text outside of the API reference boxes. This can cause issues for copy-paste implementations.

[Freek Wiedijk]

As a boomer, I would like to print a paper copy of The Lean Language Reference. How do I get this? Is there a reasonably looking pdf version of this? Or can I get a printable version in some other way?

[Notification Bot]

A message was moved here from #new members > Printable manual? by Ruben Van de Velde.

[Ruben Van de Velde]

I'll merge this with the same question from Hannah

[David Thrane Christiansen]

There's not yet a good way to do a printed version, I'm afraid. The foundations for it are there, and the implementation doesn't assume HTML is the only format, but generating a quality PDF will still require significant effort to be invested.

[Freek Wiedijk]

Thanks! I'll wait patiently (or invest a significant effort myself :-))

[David Thrane Christiansen]

If you're serious about that, then I'd be very happy to point you in the right direction.

Verso is an extensible document language, in that sense a bit like LaTeX (though more like Scribble or Sphinx). But what that means is that each additional documentation structure needs to be implemented for each backend. Some are easy, but not all. If emitting LaTeX is something you'd like to do, I'll show you how to get started.

[suhr]

Emitting typst could be also an option. I would like to know more about how to add a backend to verso as well.

[Freek Wiedijk]

I made the mistake to try to download this latest directory using wget -r -np. That turned out to be more than a gigabyte (why?!), and now I can't access the manual at all anymore. Well, I hope that's temporary :shrug:

[Hannah]

David Thrane Christiansen said:

The document can be rendered as a single HTML page. That mode has a few issues for ordinary browsing, which is why it's not published anywhere, but you can build it by checking out the manual repository and running lake exe generate-manual --without-html-multi --with-html-single. If that causes you any difficulties, let me know, and I can send you a zip file.

Thanks for your reply, and sorry for the delay in getting back to you. I am finding all of this intensely frustrating. I keep pouring hours and hours into it, getting nowhere, and finding myself having to step away.

I tried running the command given above, as well as lake exe generate-manual --depth 2 as given on the github page, and got 10 errors:

✖ [557/565] Building Manual.IO.Console
trace: .> LEAN_PATH=C:\reference-manual\.lake\packages\subverso\.lake\build\lib\lean;C:\reference-manual\.lake\packages\MD4Lean\.lake\build\lib\lean;C:\reference-manual\.lake\packages\verso\.lake\build\lib\lean;C:\reference-manual\.lake\build\lib\lean c:\Users\Hannah\.elan\toolchains\leanprover--lean4---v4.22.0-rc2\bin\lean.exe C:\reference-manual\Manual\IO\Console.lean -o C:\reference-manual\.lake\build\lib\lean\Manual\IO\Console.olean -i C:\reference-manual\.lake\build\lib\lean\Manual\IO\Console.ilean -c C:\reference-manual\.lake\build\ir\Manual\IO\Console.c --setup C:\reference-manual\.lake\build\ir\Manual\IO\Console.setup.json --json
error: Manual/IO/Console.lean:40:0: When running 'lake env which subverso-extract-mod', the exit code was 1
Stderr:
error: no such file or directory (error code: 2)

and

error: Manual/BuildTools/Lake/Config.lean:216:0: Mismatched elaborated configuration output:
   [~100 lines of rubbish here, including lots of diff pairs like this:]
-     {toWorkspaceConfig := { packagesDir := FilePath.mk ".lake/packages" },
+     {toWorkspaceConfig := { packagesDir := FilePath.mk ".lake\\packages" },

and so on. So I tried something else: I tried building Theorem Proving in Lean, which I see you're also the author of, using the very simple command lake exe tpil on its github page. This time I only got one error:

trace: .> LEAN_PATH=C:\theorem_proving_in_lean4\book\.lake\packages\MD4Lean\.lake\build\lib\lean;C:\theorem_proving_in_lean4\book\.lake\packages\subverso\.lake\build\lib\lean;C:\theorem_proving_in_lean4\book\.lake\packages\verso\.lake\build\lib\lean;C:\theorem_proving_in_lean4\book\.lake\build\lib\lean c:\Users\Hannah\.elan\toolchains\leanprover--lean4---v4.21.0-rc3\bin\lean.exe C:\theorem_proving_in_lean4\book\.lake\packages\subverso\src\\SubVerso\Compat.lean -R C:\theorem_proving_in_lean4\book\.lake\packages\subverso\src\ -o C:\theorem_proving_in_lean4\book\.lake\packages\subverso\.lake\build\lib\lean\SubVerso\Compat.olean -i C:\theorem_proving_in_lean4\book\.lake\packages\subverso\.lake\build\lib\lean\SubVerso\Compat.ilean -c C:\theorem_proving_in_lean4\book\.lake\packages\subverso\.lake\build\ir\SubVerso\Compat.c --json
error: no such file or directory (error code: 2)
  file: C:\theorem_proving_in_lean4\book\.lake\packages\subverso\.lake\build\lib\lean\SubVerso\Compat.olean
Some required builds logged failures:
- SubVerso.Compat
error: build failed

but I have no idea what to do with it. There is a discussion here that seems as though it could be related, but obviously I can't make head nor tail of it. I tried deleting the subverso directory and re-cloning it from github, but I have no idea how to build it, and the suggestion on the github page that I add the line

require subverso from git "git@github.com:leanprover/subverso.git"

to my lakefile did nothing but make lake complain that it didn't understand what I meant. I tried mimicking what was already in there and adding

[[require]]
name = "subverso"
git = "https://github.com/leanprover/subverso.git"
rev = "main"

instead, but no luck. Finally, I tried just reinstalling Lean altogether: since most of the official instructions are for VS Code integration, and that wouldn't get me any closer to be able to work on the command line as I seem to need to here, I tried following the instructions to set up elan, and all was going well until:

error: could not create link from 'C:\Users\Hannah\.elan\bin\elan.exe' to 'C:\Users\Hannah\.elan\bin\lake.exe'
Elan failed with error code 1
1

Is this a fail state? I'm not actually sure: it seems to have generated binaries and added itself to my path, so maybe not. But I tried all the above again after it, and it still gave the same errors. In fact, I have tried all of the above on both Windows 10 and Debian 12, over and over, in various different orders and configurations. I find it hard to believe that there's anything wrong with my toolchain - I've barely done anything since I first installed Lean a couple of months ago.

Please make this just a little bit easier. I am not new to programming, but I'm not a professional software engineer, and I can't spend weeks debugging these things. I just want to prove some theorems. I have been really excited about getting stuck into Lean for ages, but I am finding this all so disheartening.

[Louis Cabarion]

@Hannah I agree that getting a PDF version of the reference manual is currently a bit cumbersome, to say the least. Hopefully, a proper PDF version will be available for direct download on the official documentation site in the future.

In the meantime, does the following manual process work for you? I'm not sure about Windows, but it should work under macOS and Linux.

[Louis Cabarion]

% git clone https://github.com/leanprover/reference-manual
% cd reference-manual/
% lake exe generate-manual --with-html-single
% pandoc _out/html-single/index.html -o reference.pdf --pdf-engine=lualatex
% open reference.pdf

[Kevin Buzzard]

I tried this (in an attempt to help) but got hundreds of warnings in the pandoc step:

...
[WARNING] Missing character: There is no α (U+03B1) (U+03B1) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no ∈ (U+2208) (U+2208) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no ⟨ (U+27E8) (U+27E8) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no ⟩ (U+27E9) (U+27E9) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no β (U+03B2) (U+03B2) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no β (U+03B2) (U+03B2) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no β (U+03B2) (U+03B2) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no β (U+03B2) (U+03B2) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no β (U+03B2) (U+03B2) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no β (U+03B2) (U+03B2) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no ✝ (U+271D) (U+271D) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no ✝ (U+271D) (U+271D) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no ✝ (U+271D) (U+271D) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no ✝ (U+271D) (U+271D) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no ✝ (U+271D) (U+271D) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no ⊢ (U+22A2) (U+22A2) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no β (U+03B2) (U+03B2) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no β (U+03B2) (U+03B2) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no β (U+03B2) (U+03B2) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no β (U+03B2) (U+03B2) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no β (U+03B2) (U+03B2) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no β (U+03B2) (U+03B2) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no ⊢ (U+22A2) (U+22A2) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no ✝ (U+271D) (U+271D) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no 🔗 (U+1F517) (U+1F517) in font [lmroman10-bold]:+tlig;!
[WARNING] Missing character: There is no α (U+03B1) (U+03B1) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no α (U+03B1) (U+03B1) in font [lmmono10-regular]:!
[WARNING] Missing character: There is no ∅ (U+2205) (U+2205) in font [lmmono10-regular]:!
...

I think the resulting 1872-page pdf is not really usable as a consequence.

[Hannah]

Isak Colboubrani said:

% git clone https://github.com/leanprover/reference-manual
% cd reference-manual/
% lake exe generate-manual --with-html-single
% pandoc _out/html-single/index.html -o reference.pdf --pdf-engine=lualatex
% open reference.pdf

No, I'm afraid it fails on the line lake exe generate-manual --with-html-single, with all the same errors as I mentioned above, mostly When running 'lake env which subverso-extract-mod', the exit code was 1. This is clearly an error with Subverso, or how it's integrated here, or something.

Have you succeeded in turning the reference manual into a PDF? Or David, or anyone? I'd appreciate it if one of you could upload it here.

[Joscha Mennicken]

I've managed to produce a somewhat usable PDF of the entire language reference [Edit: better PDF at #new members > Printable form of language reference? @ 💬]. It has 1715 pages.

The Lean Language Reference.pdf

I've produced the PDF as follows:

1. Generate the single-page HTML version
2. Edit the CSS to remove some UI elements and tweak some others (this could be part of the default style sheets using media queries)
3. Print to PDF using Chromium (the PDF created by Firefox would fail to open in my PDF viewer)

Most text is readable, and links to other parts of the reference seem to be working.

Where code blocks are too wide, there's a (non-functional) scroll bar instead of the text wrapping. This could probably be fixed in the print CSS.

Footnotes are also presented inline in the text and look somewhat broken. A footnote starts with a number overlapping the text, then the footnote itself follows, and then the footnote reference (the same number, but slightly smaller and not overlapping) concludes the footnote. Not sure how one would fix this in print mode, but at least it's readable.

This image shows a footnote with number 5 that spans "More details […] on the topic."
image.png

[Joscha Mennicken]

It doesn't seem like footnotes can be improved by scaling the page down in the PDF. Even though there's enough space, they're still displayed weird. A more elaborate fix might be needed.

[Joscha Mennicken]

The scroll bars might be fixable by setting

pre { white-space: pre-wrap; }

[Joscha Mennicken]

After a few tweaks, the generated PDF now looks a bit nicer. I opened a PR with the results of my experiments: https://github.com/leanprover/reference-manual/pull/527

The Lean Language Reference.pdf

[Kevin Buzzard]

Hannah said:

No, I'm afraid it fails on the line lake exe generate-manual --with-html-single, with all the same errors as I mentioned above

FWIW that line worked fine for me (on Ubuntu), it was the pandoc line which gave me warning about missing characters.

[David Thrane Christiansen]

@Hannah Those build errors you're seeing are almost certainly due to the build process not having been tested on Windows, and it thus relying on certain fairly standard Unix utilities which are unfortunately only standard on Unix. Portability of the code that produces the output has not been a priority thus far, though it sounds like this should perhaps change.

If you run it under WSL, then the which command will likely be available and get this step un-stuck. I also get that this isn't so satisfying. I'm out for the next two weeks, but I can look into making the build Windows-friendly when I get back.

Thanks for the print stylesheet fixes, @Joscha Mennicken - they're greatly appreciated!

[David Thrane Christiansen]

@Joscha Mennicken I think that you could probably set the width of the margin notes to something like 80% in the print stylesheet and then set paragraphs to clear: both to get them to display separately.

[Joscha Mennicken]

As far as I can tell, clear is about floating values, and float does not work when printing, so I don't see how that would work (and, trying out what I think you said, it doesn't seem to work).

[Joscha Mennicken]

Once more, and hopefully without any nonfunctional scroll bars:
The Lean Language Reference.pdf

[Mauricio Collares]

Kevin Buzzard said:

I think the resulting 1872-page pdf is not really usable as a consequence.

Does something like pandoc -V monofont='DejaVu Sans Mono' -V mainfont='DejaVu Sans' --pdf-engine=xelatex _out/html-single/index.html -o reference.pdf work better?

[Mauricio Collares]

Unfortunately line breaks in code get all messed up