Discussion thread for Lean Language Reference

Stream: general

[David Thrane Christiansen]

Please discuss the announcement and the contents here!

[Matthew Ballard]

This is great. Thanks so much @David Thrane Christiansen

[David Thrane Christiansen]

Thank you all - without the enthusiastic community of Lean users, there wouldn't be a way for me to get to write both my dream documentation tool and the manual I always wanted - and as my day job!

[Max Nowak 🐉]

Oh wow this is amazing! I know so many friends who have complained before about a lack of reference. Now I can just link them this :D. Thank you so much!

Small suggestion: "Flatten" the hierarchy a little, for example maybe introduce chapters to strip one level of depth? 3.2.4.1.2. Example Inductive Types is a bit hard to refer to.

[Joachim Breitner]

is it ever useful to externally refer to sections by their numbers? I'd expect that that isn't going to be very stable as the text grows.

[David Thrane Christiansen]

Great suggestion!

The Verso setup has support for stable links to chapters, docstrings, etc, but it's not yet easy to find them from the UI. Ideally, the stable internal ID (eg example-inductive-types) would be the unit of link sharing.

But the hierarchy is certainly not fixed, and I'll keep track of these things as the text grows.

[Julian Berman]

For like 10 years it was a not-completely-rare occurrence to tell someone "you are asking about section 4.9.1 of the python tutorial" when someone would ask about a particular common gotcha.

[Yaël Dillies]

Do we have the #ref and ref#example-inductive-types linkifiers on Zulip yet? EDIT: No, can someone add them? :pray:

[David Thrane Christiansen]

How to do it is a bit undocumented right now - I can fix that tomorrow

[David Thrane Christiansen]

The Verso manual genre has multiple namespaces for stable identifiers (so libraries can compose), so we may need a bit of discussion about the best Zulip UI

[Max Nowak 🐉]

Is there a search function? I was going to look up compile_inductive% but how do I search.

[Matthew Ballard]

Julian Berman said:

For like 10 years it was a not-completely-rare occurrence to tell someone "you are asking about section 4.9.1 of the python tutorial" when someone would ask about a particular common gotcha.

We do this math also. Oh “that’s SGA 4, Expose XVIII, Thm 1.7” or “that is Hartshorne Exercise III.3.7” Once a reference becomes canonical-enough.

[Kyle Miller]

@Max Nowak 🐉 compile_inductive% is a Mathlib command. See Mathlib/Util/CompileInductive.lean

[Shreyas Srinivas]

In the tactic docs, there are a few tactics like no_match and no_fun whose documentation says "this is short for exact no_match" , but doesn't link to the no_match theorem/def in question

[Shreyas Srinivas]

A small design quibble,: Even on desktop, the font size is too small, as is the spacing between lines. Could we get an mdbook like style again? That style remains very convenient

[Julian Berman]

Matthew Ballard said:

Julian Berman said:

For like 10 years it was a not-completely-rare occurrence to tell someone "you are asking about section 4.9.1 of the python tutorial" when someone would ask about a particular common gotcha.

We do this math also. Oh “that’s SGA 4, Expose XVIII, Thm 1.7” or “that is Hartshorne Exercise III.3.7” Once a reference becomes canonical-enough.

(out of complete offtopic curiosity, were these two examples real? if so I'm curious to go look up what they refer to.)

[David Thrane Christiansen]

Max Nowak 🐉 said:

Is there a search function? I was going to look up compile_inductive% but how do I search.

Not yet! It's planned, but we figured it made sense to write the text to be searched before building the feature. Once this gets a link from the main Lean site, I suspect the usual engines will index it, but that's definitely not as good as a built-in one.

My plan is to build a combined index/search field, so that registered "things of interest" like technical terms, names of docstring'ed things, and tokens in syntax rules will have special support in the search field, making it easy to jump to their specification, with a fallback to full text search engine like lunr. This'll just take a bit of coding to get right.

Thanks for your patience :)

[Max Nowak 🐉]

Sounds awesome, I'm hyped!

[David Thrane Christiansen]

Shreyas Srinivas said:

In the tactic docs, there are a few tactics like no_match and no_fun whose documentation says "this is short for exact no_match" , but doesn't link to the no_match theorem/def in question

This was covered under the announcement caveat:

Rendered Markdown docstrings don't yet have Lean highlighting.

but I recognize that this was a quite obscure way to say it :-) Right now, content from outside of Verso isn't yet parsed r elaborated; my plan is to build some heuristics to make this possible so that the links will happen on their own most of the time. The internal links are generated from the parser's and elaborators' outputs.

[David Thrane Christiansen]

Shreyas Srinivas said:

A small design quibble,: Even on desktop, the font size is too small, as is the spacing between lines. Could we get an mdbook like style again? That style remains very convenient

Thanks for the feedback! The reference manual currently uses CSS that's copy-pasted from the Lean website, and I want to keep them in sync. I'll work on improving this aspect for both. Does your browser's zoom feature work for you in the meantime?

[David Thrane Christiansen]

Yaël Dillies said:

Do we have the #ref and ref#example-inductive-types linkifiers on Zulip yet? EDIT: No, can someone add them? :pray:

Tracking issue for the needed docs: https://github.com/leanprover/reference-manual/issues/113

[Bryan Gin-ge Chen]

Yaël Dillies said:

Do we have the #ref and ref#example-inductive-types linkifiers on Zulip yet? EDIT: No, can someone add them? :pray:

I have added #ref, but I'll wait to set up ref#example-inductive-types until the dust has settled on that front.

[Joachim Breitner]

Matthew Ballard said:

Julian Berman said:

For like 10 years it was a not-completely-rare occurrence to tell someone "you are asking about section 4.9.1 of the python tutorial" when someone would ask about a particular common gotcha.

We do this math also. Oh “that’s SGA 4, Expose XVIII, Thm 1.7” or “that is Hartshorne Exercise III.3.7” Once a reference becomes canonical-enough.

Sure, for a printed book with maybe an revision every few years. But a constantly evolving online resource? Anyways, it will happen when and if it works, we'll see :-)

[Kevin Buzzard]

Presumably the python tutorial is also a constantly evolving online resource?

[Julian Berman]

Yes, and in those 10/15 years the number never changed, though of course it's likely someone intentionally avoided doing so at some point.

[Asei Inoue]

https://lean-lang.org/doc/reference/latest/The-Lean-Language/Module-Contents/#The-Lean-Language-Reference--The-Lean-Language--Module-Contents

Manual.example command is typo of example command?

[Asei Inoue]

btw its great work! Im looking forward to see verso v1 release!

[Niels Voss]

Thanks so much for this!
Is it intentional that if you go to a URL without adding the slash at the end, it breaks the CSS? For example, https://lean-lang.org/doc/reference/latest/Basic-Types/Strings is broken for me, but https://lean-lang.org/doc/reference/latest/Basic-Types/Strings/ is fine. I found this because the former was linked in your announcement.

[Joseph Myers]

One thing I've seen mentioned occasionally, but never found documentation for, is unification hints. Is documentation of those planned for this reference?

[Joseph Myers]

The tactic documentation looks promising, though not complete (it's missing clear and revert, for example, and might well be missing other core Lean tactics). What I'd really like is for the official mathlib4 API documentation to get a version of mathlib3's https://leanprover-community.github.io/mathlib_docs/tactics.html - comprehensively listing all tactics available when you use mathlib, without regard to whether they come from core or mathlib or any of mathlib's dependencies (of course each tactic's documentation should say what imports it needs, but splitting by where the tactic is implemented isn't the most helpful thing for users) - the lack of this seems like the biggest weakness in mathlib4 documentation compared to mathlib3. Is this Lean reference set up to allow the tactic documentation to be extracted automatically for inclusion in such integrated core+mathlib+dependencies documentation if mathlib4 gets it in future?

[Mario Carneiro]

Is there a way to go to the next chapter? I would have expected a button at the end of chapter 1 to take me to chapter 2, but there isn't one that I can see, and the sidebar is also limited to just chapter 1 so you have to go back to the TOC to find chapter 2

[Mario Carneiro]

Lean's kernel is written in C++. There is an independent re-implementation in Rust, and the Lean project is interested in having as many implementations as possible so that they can be cross-checked against each other.

You should mention the Lean implementation of the kernel here, and also link the Rust implementation.

[EdwardW]

Wow it's great to have a comprehensive manual, i remember learning lean being very challenging without it !

[David Thrane Christiansen]

Mario Carneiro said:

Is there a way to go to the next chapter? I would have expected a button at the end of chapter 1 to take me to chapter 2, but there isn't one that I can see, and the sidebar is also limited to just chapter 1 so you have to go back to the TOC to find chapter 2

There is now! You can see it at https://lean-reference-manual-review.netlify.app/, and it'll be in the next release. Thanks for the feedback!

[Patrick Massot]

This is really wonderful news for the Lean community. Thank you so much David!

[David Thrane Christiansen]

Thanks for the discussions along the way, @Patrick Massot :-)

[David Thrane Christiansen]

EdwardW said:

Wow it's great to have a comprehensive manual, i remember learning lean being very challenging without it !

It is not _yet_ comprehensive - but I'm working on it! Please create/ :+1: issues in the repo that matter to you.

[David Thrane Christiansen]

Joseph Myers said:

One thing I've seen mentioned occasionally, but never found documentation for, is unification hints. Is documentation of those planned for this reference?

Yes, they're planned, but not in the immediate future (things like Array seem higher priority for now).

Here's an issue that you can watch: https://github.com/leanprover/reference-manual/issues/118

[David Thrane Christiansen]

Joseph Myers said:

The tactic documentation looks promising, though not complete (it's missing clear and revert, for example, and might well be missing other core Lean tactics).

This must be a bug in the tool that I use to track coverage of tactics. Thanks for letting me know - I'll investigate!

[David Thrane Christiansen]

Joseph Myers said:

comprehensively listing all tactics available when you use mathlib, without regard to whether they come from core or mathlib or any of mathlib's dependencies (of course each tactic's documentation should say what imports it needs, but splitting by where the tactic is implemented isn't the most helpful thing for users)

This is a useful thing to have, but I don't think it belongs in the language reference.

I think that there are situations where a document that describes a particular library (or Lean itself) is the most useful, and others that list everything available for import in a project are useful. For instance, if I'm evaluating whether to add a dependency on a library, then I want to see what's in it (and only what's in it), while if I am knee-deep in a proof, then I want to know what all my available tools are.

I added a system to track tactics a while back that can be used to build what you're looking for, at the request of users. It's since proven very handy for the manual too.

[David Thrane Christiansen]

Niels Voss said:

Is it intentional that if you go to a URL without adding the slash at the end, it breaks the CSS? For example, https://lean-lang.org/doc/reference/latest/Basic-Types/Strings is broken for me, but https://lean-lang.org/doc/reference/latest/Basic-Types/Strings/ is fine. I found this because the former was linked in your announcement.

Thanks for pointing this out - the link is fixed now in the announcement.

This is an issue with relative paths - it's definitely not intended, but I've been struggling a bit to get our web host to emit redirects from "/Ch1/Sec1" to "/Ch1/Sec1/". I'll continue looking into it. Thanks!

[David Thrane Christiansen]

Asei Inoue said:

https://lean-lang.org/doc/reference/latest/The-Lean-Language/Module-Contents/#The-Lean-Language-Reference--The-Lean-Language--Module-Contents

Manual.example command is typo of example command?

Thanks for catching this - I've fixed it, and the fix will be in the next release.

[Julian Berman]

I don't see it, but just in case -- is there perhaps an easy way to jump from a page to the source of the page, like Sphinx's Show Source functionality (e.g. in the sidebar on https://docs.python.org/3/reference/index.html)

[David Thrane Christiansen]

There is not, but it would be convenient. I don't think it's higher priority than content at this point - are there any really important use cases that I'm missing?

[Julian Berman]

No it absolutely isn't high priority seeming to me, was just curious!

[Francisco Giordano]

I was just about to bring up the same thing. For me a link to the source is useful to quickly report an issue in the content or contribute a fix, otherwise it's often difficult to know where to do that.

Very happy to see the reference being developed!

[Eric Wieser]

Is the plan for https://lean-lang.org/doc/reference/latest/Notations-and-Macros/#language-extension to include documentation of syntax quotations and antiquotations?

[t-shibata]

@David Thrane Christiansen
It's great works! I'm studying Lean4 about one year and still don't have enough knowledge, so this is very helpful for me.

And since I'm not good at English, and it would also help japanese Lean users if this manual was in Japanese, I would like to translate and release it on web.
The translation repository and release page is hosted on lean-ja, and the entire process is non-profit.

Could you please permit us to do so?

[David Thrane Christiansen]

Francisco Giordano said:

I was just about to bring up the same thing. For me a link to the source is useful to quickly report an issue in the content or contribute a fix, otherwise it's often difficult to know where to do that.

I don't doubt that it's useful, but I still think that it's a fairly small benefit, which is why I'm down-prioritizing it. Other than it taking a few more steps, how is it much better than typing the sentence in question into the GitHub search box to find the source file?

For instance, let's say I was on <https://lean-reference-manual-review.netlify.app/elaboration-and-compilation/> and wanted to contribute some additional text to the section on info trees, specifically the paragraph that starts with "Info trees relate metadata to the user's original syntax.". GItHub's search takes me right to it in the source. Certainly one click is better than a click followed by a copy-paste with quote marks and then another click, but how much better is it?

I feel like I may be missing an angle here.

[David Thrane Christiansen]

Eric Wieser said:

Is the plan for https://lean-lang.org/doc/reference/latest/Notations-and-Macros/#language-extension to include documentation of syntax quotations and antiquotations?

Yes, that's an important topic to describe in detail.

[Yaël Dillies]

David Thrane Christiansen said:

For instance, let's say I was on <https://lean-reference-manual-review.netlify.app/elaboration-and-compilation/> and wanted to contribute some additional text to the section on info trees, specifically the paragraph that starts with "Info trees relate metadata to the user's original syntax.". GItHub's search takes me right to it in the source. Certainly one click is better than a click followed by a copy-paste with quote marks and then another click, but how much better is it?

I feel like I may be missing an angle here.

You are missing the most time taking step on my experience: Find out what repo the documentation is built from.

[David Thrane Christiansen]

That is indeed important - I think I can solve that one with very little work, and will do so soon.

[Francisco Giordano]

David Thrane Christiansen said:

Certainly one click is better than a click followed by a copy-paste with quote marks and then another click, but how much better is it?

I think it's fine to deprioritize it! I'll point out though that at the moment there is no link to the GitHub repo in the website, which I think could be a good intermediate step to point people in the right direction to contribute.

[Iván Renison]

Hi, is it possible to download The Lean Language Reference as PDF or some other way to read it with out connection?

[Kevin Buzzard]

You'll lose all the fabulous
Versoality that way!

[Floris van Doorn]

Reading a pdf will definitely be an inferior experience compared to the online version. I think it's still valuable to support a pdf format for offline use (though not high priority - IMO).

[Eric Wieser]

A zip download for offline use might be a better approach, assuming this is digital-but-offline and not paper reading

[Shreyas Srinivas]

Most browsers offer an option to save a webpage. The zip download option also sounds good. What's ideal would be having an installation of the docs with each toolchain which can be opened with elan docs

[Floris van Doorn]

Topic request (low priority): pretty-printing, including delaborators, unexpanders, formatters, ...

[Shreyas Srinivas]

(deleted)

[Jannis Limperg]

Floris van Doorn said:

Topic request (low priority): pretty-printing, including delaborators, unexpanders, formatters, ...

Long-term, it would be great if all major metaprogramming topics were covered in the reference. Reliable conceptual and overview documentation for the metaprogramming APIs is still hard to come by. But of course this is a very big topic.

[Eric Wieser]

Maybe these docs could absorb the monad map from the mathlib wiki too?

[David Thrane Christiansen]

Francisco Giordano said:

I think it's fine to deprioritize it! I'll point out though that at the moment there is no link to the GitHub repo in the website, which I think could be a good intermediate step to point people in the right direction to contribute.

Indeed, that's the "very little work" way that I was talking about above.

[David Thrane Christiansen]

Floris van Doorn said:

Topic request (low priority): pretty-printing, including delaborators, unexpanders, formatters, ...

Definitely important. Here's the tracking issue: https://github.com/leanprover/reference-manual/issues/122

If you have nice examples for the docs, or aspects that you think are particularly important, please post them there so they don't get lost!

[David Thrane Christiansen]

Eric Wieser said:

Maybe these docs could absorb the monad map from the mathlib wiki too?

That's this one, right? That'd be great information to have in the language reference.

[David Thrane Christiansen]

Iván Renison said:

Hi, is it possible to download The Lean Language Reference as PDF or some other way to read it with out connection?

Right now, the easiest way to read it without a connection is to build the HTML locally. This is definitely not ideal, and it will be improved. People need to be able to work on airplanes.

For proofreading on my Remarkable, I usually generate the whole thing as one giant HTML file then print to PDF, and you'll find a bit of a print stylesheet in the repo. The results are not beautiful, but they do let me sit with a red pen and see things in enough of a different format to catch mistakes that disappear in the browser version.

This is an area where the right kind of external contribution could be useful. Verso 's manual genre already supports generating LaTeX, but basically none of the documentation tools used in the reference manual support TeX output. I won't have time to improve this in the near future, but it'd be easy code to review. The only hard part would be implementing the rendering of the highlighted code examples to LaTeX, but I think the right combination of fancyvrb and hyperref could make it work pretty well in maybe 2-3 days of work. Epub output would also be really useful.

[David Thrane Christiansen]

And if Verso can one day be useful for writing papers, then it'd better support TeX rendering of Lean code :-)

[Utensil Song]

Thanks for the great work on documentation infrastructure, and the well written manual! :heart:

Just skimmed through the contents, a few nitpicks:

1. while internal fuzzy searching is desirable, currently the index is a good place to search for terms of interest; some entries with long namespace could be further grouped by the last namespaces, e.g. String.*, Nat.*, Lean.Elab.Tactic.*, Lean.Meta.Simp.*.
2. blue boxes for reference entries have tall top and bottom margins, tall enough to break reading "flow", a smaller margin that's proportional to the line height would be nice.
3. would love to see more entries for symbols, there are currently 7 of them, it's one of the top things a newcomer needs the reference manual for, with good discoverability.

[Utensil Song]

And a general question: in the long term, how would the manual be kept in sync with code and doc string when features evolve? Is it something the Lean-native Verso can help to solve, so it's easier for maintainers to ensure that they are in sync, and readers are more assured that they are in sync, and when it's not, it's one-click away to the most up-to-date source of documentation (the relevant code)?

[Edward van de Meent]

at the explanation for the requirements for inductive types, the example claims that the defined Fix (fun a => a -> a) would be equivalent to Bad... i've given a shot, but i couldn't seem to prove that you can construct Bad.rec function from Fix.rec? Maybe it would be easier to say that Fix (. -> Empty) is an inconsistent type (as you're creating a fixpoint for negation)?

[Kim Morrison]

Utensil Song said:

And a general question: in the long term, how would the manual be kept in sync with code and doc string when features evolve? Is it something the Lean-native Verso can help to solve, so it's easier for maintainers to ensure that they are in sync, and readers are more assured that they are in sync, and when it's not, it's one-click away to the most up-to-date source of documentation (the relevant code)?

One of the amazing things about Verso is that it completely solves this problem. All the code samples in Verso are "live", and tested at build time.

[David Thrane Christiansen]

Utensil Song said:

1. while internal fuzzy searching is desirable, currently the index is a good place to search for terms of interest; some entries with long namespace could be further grouped by the last namespaces, e.g. String.*, Nat.*, Lean.Elab.Tactic.*, Lean.Meta.Simp.*.

Very good idea! Here's the tracking issue.

[David Thrane Christiansen]

Utensil Song said:

2. blue boxes for reference entries have tall top and bottom margins, tall enough to break reading "flow", a smaller margin that's proportional to the line height would be nice.

This would be a nice improvement.

Utensil Song said:

3. would love to see more entries for symbols, there are currently 7 of them, it's one of the top things a newcomer needs the reference manual for, with good discoverability.

Yes, good point!

[Jannis Limperg]

Edward van de Meent said:

at the explanation for the requirements for inductive types, the example claims that the defined Fix (fun a => a -> a) would be equivalent to Bad... i've given a shot, but i couldn't seem to prove that you can construct Bad.rec function from Fix.rec? Maybe it would be easier to say that Fix (. -> False) is an inconsistent type (as you're creating a fixpoint for negation)?

I looked into this and indeed Lean generates a recursor without an induction hypothesis for Fix.rec:

unsafe inductive Fix (f : Type u → Type u) where
  | fix : f (Fix f) → Fix f

#check Fix.rec
-- Fix.rec.{u_1, u} {f : Type u → Type u} {motive : Fix f → Sort u_1}
--   (fix : (a : f (Fix f)) → motive (Fix.fix a))
--   (t : Fix f) : motive t

So I guess the Fix that comes out of the unsafe inductive declaration is an accidentally consistent but non-inductive type.

[Edward van de Meent]

it's still not consistent, using f := (. -> Empty)

[Edward van de Meent]

my point is that the argument as to why it isn't consistent is wrong (or at least not clear)

[David Thrane Christiansen]

Utensil Song said:

And a general question: in the long term, how would the manual be kept in sync with code and doc string when features evolve? Is it something the Lean-native Verso can help to solve, so it's easier for maintainers to ensure that they are in sync, and readers are more assured that they are in sync, and when it's not, it's one-click away to the most up-to-date source of documentation (the relevant code)?

@Kim Morrison gave half of the answer above (the examples are all checked at documentation build time).

There's a few other ways in which Verso has been designed to make the manual maintainable:

1. When output from Lean is included in the docs (error messages, proof states, etc) it is also included in the source code. This means that if the output changes, the build breaks. Code actions allow it to be updated easily, but someone has to look at it and approve it.
2. When empirical claims about the language are made, they're often backed up by little tests that are not included in the output at all. Here's an example.

I hope this keeps maintenance affordable over time, so we can focus mostly on new content!

[David Thrane Christiansen]

@Edward van de Meent, @Jannis Limperg Thanks! I just created this issue for this problem.

[David Thrane Christiansen]

t-shibata said:

David Thrane Christiansen
It's great works! I'm studying Lean4 about one year and still don't have enough knowledge, so this is very helpful for me.

And since I'm not good at English, and it would also help japanese Lean users if this manual was in Japanese, I would like to translate and release it on web.
The translation repository and release page is hosted on lean-ja, and the entire process is non-profit.

Could you please permit us to do so?

Please feel free to translate the reference! Thanks!

I'd appreciate it if there was a clear indication that it's an unofficial translation, and a link to the original.

There will be major changes and additions to the text in the coming months. How do you plan to keep up with them and keep your translation synchronized with the upstream version?

[Jannis Limperg]

Edward van de Meent said:

it's still not consistent, using f := (. -> Empty)

How do you prove False with this? I'm not seeing it atm.

[Edward van de Meent]

set_option autoImplicit false

universe u v

axiom Fix : (f:Type u → Type u) → Type u
axiom Fix.mk : {f:Type u → Type u} → f (Fix f) → Fix f

axiom Fix.rec : {f:Type u → Type u} → {motive : Fix f → Sort v} →
  (mk: (a:f (Fix f)) → motive (Fix.mk a)) → (a:Fix f) → motive a

noncomputable def Bad.toEmpty : Fix (· → Empty) → Empty := fun b =>
  Fix.rec (motive := fun _ => Empty) (fun v => v b) b

noncomputable instance : Inhabited (Fix (· → Empty)) := ⟨Fix.mk (Bad.toEmpty)⟩

example : False := (Bad.toEmpty.{u} default).elim

[Edward van de Meent]

i also posted this at the issue

[David Thrane Christiansen]

Thanks!

[t-shibata]

David Thrane Christiansen said:

I'd appreciate it if there was a clear indication that it's an unofficial translation, and a link to the original.

There will be major changes and additions to the text in the coming months. How do you plan to keep up with them and keep your translation synchronized with the upstream version?

Thanks a lot! I am very honored that you commented on my proposal.
I also understood the note about translations and the link to the original text. I will take care of this.

As a matter of fact, I do not have an efficient plan for keeping translations up to date.
This is because machine translation from English to Japanese is not very accurate(it's still very helpful, of course), so I prefer steady manual translation.
Therefore, I will rebase from the original repository every few months, and translate the updated content each time.
I have been translating Mathematics in Lean with this policy, and it seems to be working relatively well for me.

[David Thrane Christiansen]

That's great to hear! I look forward to seeing the results, even though I can't read Japanese :-)

[Utensil Song]

Kim Morrison said:

All the code samples in Verso are "live", and tested at build time.

David Thrane Christiansen said:

There's a few other ways in which Verso has been designed to make the manual maintainable (...omitted...)

Good to know these ways to keep examples, outputs, claims in sync, these are truely remarkable. I've also noticed that doc for many types of reference entries (options, type classes, structures etc.) are automatically extracted from docstring to keep in sync, that's what I was asking about before learning about this from the source of manual.

Exceptions to these are signature, grammar etc., these are hard-coded in the manual, which might be out-of-sync with the actual implementation.

[Asei Inoue]

my Lean documentation (in Japanese) has ability of jumping to Lean 4 playground.

https://lean-ja.github.io/lean-by-example/

This enables reader to run each file and code block.

is there a plan for verso to support such features?

[David Thrane Christiansen]

@Utensil Song:

The signature block elaborates the provided signature and checks that it's equivalent to the actual signature. It then uses the way it's written in the source for display, rather than pretty-printing it, so that the formatting can be chosen in a way that's most useful for showing how the parts relate. So that should be pretty maintainable over time.

Similarly, the syntax/grammar blocks invoke the Lean parser on what's written in them. This doesn't check coverage - it might miss new alternatives added - but it does check that what's written does successfully parse. And we don't want something that checks complete coverage, because many things are parsed successfully and then later rejected by the elaborator, sometimes to get better error messages and sometimes to get better completion. For instance, import Foo.Bar. is valid import syntax according to the grammar to enable completion, but the trailing dot isn't really part of the syntax that it makes sense to document.

[David Thrane Christiansen]

Asei Inoue said:

is there a plan for verso to support such features?

There is a desire, but not a concrete plan right now. The difficulty is tracking dependencies across examples - sometimes a single example contains a few bits of code, and the playground button should load all the dependencies but no more. This would be great, it's just not currently on the immediate short path.

This is an area where an external contribution would be welcome.

[David Thrane Christiansen]

All right, based on your feedback, a second preview is up. Content-wise, it's mostly the same (apart from the links suggested by @Mario Carneiro), but it now has the following:

• Section headers and documentation boxes now have permalink indicators, from which the permanent link can be copied
• There are links to the source repository and issue tracker on every page
• There are relative navigation buttons in the left-side table of contents, allowing movement upwards in the tree, or to the previous or next chapter/section

[David Thrane Christiansen]

Thanks for your feedback so far, and please let me know if there's other things that get in the way of reading.

[Joachim Breitner]

Nice. Trying to use the section links I get “# No target provided, This script expects a 'target' query parameter, along with documentation domains.”

[David Thrane Christiansen]

Wow, that was fun to diagnose! Seems to be the GH cache preserving an older version of some JS. I'll think about how to make the build/cache process more robust.

[Joachim Breitner]

“There are two hard problems in compuer science…”

[David Thrane Christiansen]

Thanks for the heads up

[Utensil Song]

I've noticed a weird style issue earlier: I can scroll past the bottom, so it will look like this:

image.png

Today I observe that it can be stably reproduced for pages like https://lean-lang.org/doc/reference/latest///Elaboration-and-Compilation/ and https://lean-lang.org/doc/reference/latest///The-Lean-Language/The-Type-System/ i.e. it seems to only happen to pages with margin notes.

[Daniel Weber]

What browser are you using? I can't reproduce this on Firefox (on Ubuntu)

[Utensil Song]

Chrome on Mac

[Daniel Weber]

image.png
On Chromium (129.0.6668.100) I get two scroll bars

[David Thrane Christiansen]

Thanks for the reports! I'll see what I can figure out.

Tracking issue

[Yuri]

@David Thrane Christiansen are you planning a chapter/section on FFI? I don't see it yet in the current draft.

[Edward van de Meent]

there is some of it mentioned in the part about inductive types

[Edward van de Meent]

here

[David Thrane Christiansen]

Yuri de Wit said:

David Thrane Christiansen are you planning a chapter/section on FFI? I don't see it yet in the current draft.

The current plan is to have a short section on the general principles of the FFI, and then have type-specific FFI information as part of the API reference for said types. Some of that information is present, but it's a lower priority than some other topics at the moment.

[David Thrane Christiansen]

(here "type-specific FFI information" refers to things like this)

[David Thrane Christiansen]

If there's specific information about the FFI that would be particularly valuable for you, please create an issue that describes it!

[Daniel Weber]

The links in the index https://lean-lang.org/doc/reference/latest/the-index/#The-Lean-Language-Reference--Index aren't working, because the links are to #---index-hdr-X but there is <base href="/doc/reference/latest/">. This can be fixed by using the-index/#---index-hdr-X in the links

[Shreyas Srinivas]

Can we retain some of the examples from the old manual?

[Shreyas Srinivas]

I think there were examples for De Bruijn indices, and HOAS

[David Thrane Christiansen]

The plan right now is to replace the sections labeled "Language Manual" on https://lean-lang.org/lean4/doc/ , not the entire contents of that site. The examples aren't part of what's being replaced. Thanks for checking!

[David Thrane Christiansen]

Daniel Weber said:

The links in the index https://lean-lang.org/doc/reference/latest/the-index/#The-Lean-Language-Reference--Index aren't working, because the links are to #---index-hdr-X but there is <base href="/doc/reference/latest/">. This can be fixed by using the-index/#---index-hdr-X in the links

Thanks for pointing this out! Not sure how I missed it when you posted the comment here, and sorry for the slow reply. It's now issue #150.

[Heather Macbeth]

I already find myself turning to this reference regularly, thanks! I find it a bit hard to navigate, though. A search functionality (already discussed above) would help. But another thing I think would help would be a typed index. For example, it would be great to have individual indexes for each of the following kinds of items:

• options
• commands
• declarations
• tactics

[David Thrane Christiansen]

I completely agree - thank you! #151

[David Thrane Christiansen]

I think the overall structure could also use a bit of reorganization. The current table of contents is based on an initial guess, but now that there's content, it's worth revisiting to improve it.

[Asei Inoue]

@David Thrane Christiansen
is there a plan to write about user widget?
Now documents for user widget is only seen in Lean manual…

[Eric Wieser]

I find the recent

abbrev T.{u} : Unit := (fun (α : Sort u) => ()) PUnit.{u}

set_option pp.universes true

def test.{u, v} : T.{u} = T.{v} := rfl

example quite strange; the fact that

def test.{u, v} : T.{u} = T.{v} := by
  unfold T
  rfl

works as a proof makes it almost seem like this is a bug!

[Joseph Myers]

Heather Macbeth said:

I already find myself turning to this reference regularly, thanks! I find it a bit hard to navigate, though. A search functionality (already discussed above) would help. But another thing I think would help would be a typed index. For example, it would be great to have individual indexes for each of the following kinds of items:

• options
• commands
• declarations
• tactics

I previously mentioned that I'd like the mathlib API reference to automatically extract the tactic documentation from this manual and combine it with documentation for all the tactics in mathlib and its dependencies in a single place, like with had in the mathlib3 docs (we still don't have a mathlib4 tactic reference on the leanprover-community site). Much the same would also apply to the other things you listed: a combined reference would be desirable, in addition to reference material in the Lean manual. I'd also like to add

• attributes (i.e. the individual attributes one might put on a definition, as opposed to documentation of the underlying attribute mechanism as a whole)
• custom expression elaborators such as mod_cast or congr()
  to the list of such things for which a combined reference would be desirable (in addition to the Lean reference manual covering whatever instances of such things do come from core Lean).

[Daniel Weber]

The view with the sidebar on mobile isn't great, especially since it's is open by default:
Screen Shot 2024-11-16 at 07.46.08.png
Some suggestions:

• the sidebar should be closed by default on small screens
• clicking outside of the sidebar should close it
• the page outside the sidebar should be grayed out and/or unscrollable

[Daniel Weber]

Also, when the sidebar is hidden, when refreshing the page it appears for a split second and then disappears again - perhaps disabling the animation when that happens would make it less noticeable

[Arthur Adjedj]

Eric Wieser said:

I find the recent

abbrev T.{u} : Unit := (fun (α : Sort u) => ()) PUnit.{u}

set_option pp.universes true

def test.{u, v} : T.{u} = T.{v} := rfl

example quite strange; the fact that

def test.{u, v} : T.{u} = T.{v} := by
  unfold T
  rfl

works as a proof makes it almost seem like this is a bug!

Right. It looks to me like this part should return undef when the universe equality is false.

[David Loeffler]

Totally trivial remark: in the section

https://lean-lang.org/doc/reference/latest//The-Lean-Language/The-Type-System/#implicit-functions

last sentence of the paragraph "Strict implicit parameters" has a typo: "Ordinary implicit parameters are written..." should be "Strict implicit parameters are written..."

[David Thrane Christiansen]

Asei Inoue said:

David Thrane Christiansen
is there a plan to write about user widget?
Now documents for user widget is only seen in Lean manual…

The feature is definitely in-scope, but it's not likely to be written about for quite some time. It's a much higher priority to document fundamental language features, like the elaboration of recursive functions, the basic types, and so forth. This language reference won't replace that section of the old manual, which is outside the "language manual" header; if it ever does, then the prior material will at a bare minimum get ported over verbatim.

[David Thrane Christiansen]

@Eric Wieser, @Arthur Adjedj - thanks for scratching at this one. It's now lean4#6117.

[Shreyas Srinivas]

Can we have a section or chapter on proving things in monadic code with Satisfies? It seems sufficiently fundamental and important that it ought to be documented and explained

[Kim Morrison]

SatisfiesM is not part of the core language, it is an experimental extension (which I like!) in Batteries. So it won't be in the Lean manual for now.

[David Thrane Christiansen]

Daniel Weber said:

Some suggestions:

• the sidebar should be closed by default on small screens
• clicking outside of the sidebar should close it
• the page outside the sidebar should be grayed out and/or unscrollable

Also, when the sidebar is hidden, when refreshing the page it appears for a split second and then disappears again - perhaps disabling the animation when that happens would make it less noticeable

We've now implemented all of these suggestions and pushed an update to the preview release. Thank you very much for the feedback!

[David Thrane Christiansen]

@Joseph Myers All of your suggestions are very good, and a combined index for the documentation of the complete transitive dependencies of a project would be extremely valuable. It's not part of this particular effort, which is to get one piece of that data in good shape, but I'm absolutely working with an eye towards integration. Thanks again!

[David Thrane Christiansen]

David Loeffler said:

Totally trivial remark: in the section

https://lean-lang.org/doc/reference/latest//The-Lean-Language/The-Type-System/#implicit-functions

last sentence of the paragraph "Strict implicit parameters" has a typo: "Ordinary implicit parameters are written..." should be "Strict implicit parameters are written..."

Thank you! This is not so trivial, really - that kind of mistake has the potential to confuse new users. It's important to get it right. Much appreciated!

[David Thrane Christiansen]

Eric Wieser said:

I find the recent

...

example quite strange ...

This example is now correct as of this PR - thank you very much for the feedback!

[Floris van Doorn]

Very nice, I'm still reading through the chapter.

One remark: in the example of 11.5.3 it is not clear in Firefox that the code can be horizontally scrolled.
image.png
(when moving my mouse over the code a very thin scroll bar appears, but not otherwise)

In Chrome this is indicated much more clearly
image.png

[David Thrane Christiansen]

That's no good! I think the solution here is to format the examples such that they don't overflow on the vast majority of screens. This is now #163.

[Eric Wieser]

Can Std.Format be converted into auto-wrapping HTML?

[Eric Wieser]

(which would be useful in the infoview too)

[David Thrane Christiansen]

In principle, yes - I set up a Haskell pretty printing library to render to Javascript about a decade ago, so that it reflowed when resizing a webpage (and even measured the rendered width of the text, so it could use proportional fonts). It used an algorithm essentially similar to the one in Std.Format (though reformulated as a shallow rather than deep embedding of the document language). It was fun, and I agree it'd be nice in the infoview and in Verso HTML output.

But that wouldn't fix this issue, because this is source code rather than pretty printer output, and the associated info tree is a big part of getting the highlighting and such to work. I'd rather lay out instructive source code examples by hand. I just need to figure out a column target and have Verso complain when I exceed it.

[Antoine Chambert-Loir]

A remark on the navigation buttons: when one lands on the first page, that with the table of contents, the Prev and Up buttons do not work, as they should, but the Next doesn't neither, and it could lead to section 1.

[David Thrane Christiansen]

Thanks for the feedback!

Would you also expect "Prev" to take you from section 1 to the site root?

[Antoine Chambert-Loir]

I have to admit, I don't know, because but probably yes (unless "Prev" doesn't switch sections).

[Antoine Chambert-Loir]

For the case of the toc, it's more sensible, because one has to guess that there is no other thing to do than starting to read section 1.

[David Thrane Christiansen]

Today, it only navigates between sections at the same level.

I'm of two minds on this - you're absolutely right that there's nowhere to go but down from the ToC. On the other hand, this special case doesn't make sense for any subsections, and I worry about having features that work differently in different areas. I'll think about it for a while.

How do other readers in this thread feel about this point?

[Antoine Chambert-Loir]

exactly, I was at the head of section 7, showing the toc after a short introduction, and I clicked next, because I wanted to read 7.1, but that led me to 8. So maybe it's me not understanding the intent of these buttons.

[David Thrane Christiansen]

The intent is that they navigate the document's table of contents: "next" on a chapter goes to the next chapter, or on a subsection it goes to the next subsection. But perhaps that's not what most readers expect, in which case it should change - I do have a very "programmer"y view of things sometimes. Perhaps "next" and "prev" should be a preorder traversal instead.

[David Thrane Christiansen]

OK, having asked a few others and thought about it, I think it should be changed. verso#231. Thanks!

[Kevin Buzzard]

In the stacks project there are "parts" e.g. https://stacks.math.columbia.edu/tag/0ELP, and it doesn't say "next"/"previous" it says "next part", "previous part". You then go down into "chapters" e.g. https://stacks.math.columbia.edu/tag/01QL and the buttons say "next chapter" and "previous chapter". You then go down into "sections" e.g. https://stacks.math.columbia.edu/tag/056H and now the buttons say "next section" and "previous section". To go "up" you can look at the bar at the top, and to go "down" you can look at the links on the page if the page is a part or a chapter.

[David Thrane Christiansen]

That's how the Lean reference works today (though adding "part/chapter/section" would make it much more clear). mdbook and Scribble both do the preorder traversal version. Having asked around and thought about it some more, I think that we should change it to fit the latter group of tools.

[Julian Berman]

I haven't read the whole thread (so apologies if this is already covered) but do you have plans/thoughts for how versioning will work, or how it already does in case I missed it? Specifically how can I answer which version of Lean I'm reading the reference for, and/or potentially view it for other versions in the future (if I want to retroactively see it for an older Lean version)? I know if I click the introduction it says it's for 4.14.0-rc1 -- (n.b. in Sphinx there's a simple dropdown typically for switching versions... in Rust I see the reference telling you to do this by editing the URL?! https://doc.rust-lang.org/stable/reference/#rust-releases)

[David Thrane Christiansen]

We have a strategy/plan for versioning, but we don't have a concrete UI for picking versions yet. I like the way readthedocs does it.

Right now, all focus is on getting the content written, and the reference manual is tracking upstream development reasonably closely. It mentions which version it's for, but it's only for that version.

Once we feel like there's enough content for it to make sense to do so, the plan is to have a reference manual for each compiler version. Some nightlies may not end up with their own snapshot, because all the tests integrated into the manual mean that language changes can cause it to fail when it gets out of date, but it will be tracked as closely as possible. Certainly it will be a blocker for RCs and thus releases.

We haven't yet decided whether the generated output will be part of the release tarball or a separate archive, nor have we decided how the reference manual for nightlies will be hosted/distributed. Once we reach that phase of the project, I'll be reaching out for feedback.

[David Thrane Christiansen]

Antoine Chambert-Loir said:

A remark on the navigation buttons: when one lands on the first page, that with the table of contents, the Prev and Up buttons do not work, as they should, but the Next doesn't neither, and it could lead to section 1.

Update: this is now fixed in Verso, and will be part of the next reference manual release. Thanks again for the feedback!

[Julian Berman]

Another minor bit of link feedback -- it'd be useful if clicking on a heading always got you to the fragment for that heading (again a la Sphinx/RTD). I might be missing something, but right now I don't see how to get a link for all levels of sections. Specifically what I mean is that clicking in the left sidebar on 3.3.1 gets you https://lean-lang.org/doc/reference/latest/The-Lean-Language/Module-Contents/#The-Lean-Language-Reference--The-Lean-Language--Module-Contents--Commands-and-Declarations i.e. a link to that third-level section, but nothing will get you a link to a level down, 3.3.1.1. itself, even though in the source I see it has an anchor (https://lean-lang.org/doc/reference/latest/The-Lean-Language/Module-Contents/#The-Lean-Language-Reference--The-Lean-Language--Module-Contents--Commands-and-Declarations--Definition-Like-Commands).

[Max Nowak 🐉]

Let me say again how much I love having a reference, especially one that is so well-written.

The examples being collapsed by default somehow bothers me, probably because I can't know whether it is a small example or a huge one. Often when I scroll through large documents, the first thing I look at are the examples and the general "shape" of them, sometimes without even reading the text itself. I can't do this when I have to click on every example to first unfold. Hence... can we simply have all examples non-collapsed by default?

[mars0i]

I would have expected that I could find a simple explanation of the semantics of to the various ways of defining functions, including the syntax

def foo (x : t) (...) (...) : ReturnType :=
  ...

and what the difference is between this and putting a function type after the main colon. (I know the difference now, but I was puzzled at first. You can say that I was corrupted by some other languages.) Manuals have different purposes, and maybe the kind of documentation that I hoped for doesn't belong in this manual.

The only place I see, so far, that this kind of description might belong at present is section 3.2.1, which is part of the section 3.2 "The Type System". I'm not sure whether the syntax above is mentioned at all in this section, or whether it's implied by the BNF. There is mention of anonymous functions using fun (though the familiar term "anonymous function" isn't used), and a remark that "Function definitions defined with keywords such as def desugar to fun." That's all I see so far. The section talks about Currying and pattern-matching definitions, which is good, but these ideas are mostly conveyed with BNF. That's is all worth including, but this section is not a great reference for someone who's following a tutorial or experimenting with the language, but who wants to check their understanding or clarify their thinking about the way that function definitions work. And maybe that's consistent with the goals of the manual, which is OK. However, there are other sections (e.g. 3.2.1) that make me think that the goals might be broader. I understand that a manual is not a tutorial.

(If what I'm looking for is already in the manual--even as a stub to be filled in--my apologies. I haven't found it yet.)

[David Thrane Christiansen]

Julian Berman said:

Another minor bit of link feedback -- it'd be useful if clicking on a heading always got you to the fragment for that heading (again a la Sphinx/RTD). I might be missing something, but right now I don't see how to get a link for all levels of sections. Specifically what I mean is that clicking in the left sidebar on 3.3.1 gets you https://lean-lang.org/doc/reference/latest/The-Lean-Language/Module-Contents/#The-Lean-Language-Reference--The-Lean-Language--Module-Contents--Commands-and-Declarations i.e. a link to that third-level section, but nothing will get you a link to a level down, 3.3.1.1. itself, even though in the source I see it has an anchor (https://lean-lang.org/doc/reference/latest/The-Lean-Language/Module-Contents/#The-Lean-Language-Reference--The-Lean-Language--Module-Contents--Commands-and-Declarations--Definition-Like-Commands).

Thanks for this! The plan is to have a section in the left table of contents pane that contains the important items on the current HTML page. This includes:

• All the headers and sub-headers
• API and syntax references (documented symbols, tactics, grammar productions, etc)

• Named examples
  Depending on how it turns out with a bit of experimentation, it may include:

  • Technical terms defined on the page
  • Figures

It's not implemented yet, because it seems more important to get the content written right now, but I hope to get to it relatively quickly. Would this address the concern?

[David Thrane Christiansen]

Max Nowak 🐉 said:

Hence... can we simply have all examples non-collapsed by default?

I've gone back and forth on this one a few times. Collapsed by default lets some of the examples be longer when it's useful, without it getting in the way of reading the contents. Expanded by default makes it easier to skim for them, as you're describing.

Maybe we need a little "settings" button at the top like Rustdoc recently got that pops up a panel with widgets for things like "expand all examples"?

[David Thrane Christiansen]

@mars0i The content you're looking for will go in 3.3, which will have a general subsection on how to interpret signatures. This is because signatures are very consistent between the various kinds of declarations, so I'd like to explain them in one place along with the principle "parameters on the left of the colon are in scope in the whole declaration. Given those parameters' local context, the type to the right of the colon describes the thing being declared" and then cross-reference them from the descriptions of each type of declaration.

The sections that are mostly grammar specs will also include proper textual descriptions.

[Niels Voss]

I finished reading through Sections 1.1 to 3.2, "The Type System", and I want to say I really liked the new reference, and I now know a lot more about how Lean actually works than I previously did. I did find a couple typos and I do have a few questions (mostly minor nitpicks). Should I make a PR on github for typos (and if so, how should it be split up), or should I post here? Should I post my questions here as well?

[David Thrane Christiansen]

A PR for typos would be great, thanks! If they're all obvious typos (like "the the" or "tpe systm"), one PR is fine. If some of them are more stylistic or less certain, it's helpful to have them in a separate PR so that the obvious fixes can just be merged immediately and other things can support some discussion.

[David Thrane Christiansen]

Questions work well here or as issues, depending on their nature - if they're questions about the content ("what does this sentence mean? what about this implication?") then an issue would be great, because that indicates that something about the text is incomplete or confusing. If they're more general curiosity, like "why did you do it this way?" then I think the thread is better.

But don't worry too much about it - I can make issues for things on this thread, after all! This is how you make my life easiest, but I recognize that you have other priorities too :-)

[Niels Voss]

My lake build doesn't seem to work when building the manual (it is giving me #guard_msgs errors when building Verso) so for now I'm just going to PR the typos that probably don't require testing. Do you know how to represent $2^{32}$ in Verso, as opposed to $2^32$, which is what it includes right now? (decided to report as issue on GitHub)

[Niels Voss]

I just opened a bunch of issues on GitHub, sorry if it's too many right now. I'll open a few more when I get the time.

[David Thrane Christiansen]

It's perfect, thanks! Will review on Monday

[Julian Berman]

David Thrane Christiansen said:

It's not implemented yet, because it seems more important to get the content written right now, but I hope to get to it relatively quickly. Would this address the concern?

I think like most of the other minor feedback that I definitely agree it's lower priority than the content! So no expectations there.

In terms of whether the sidebar helps -- if I visualize what you mention right, I think that sounds great, but I do think both would be nice honestly -- I think UX-wise that there's lots of precedent for "click the heading and you change the address bar to a fragment which gets you there", and mouse-over to hint that that's a link -- GitHub headings work this way as well.

(So yeah I'd probably do both, but I think it's not a major issue of course, and having some way is of course nice).

[David Thrane Christiansen]

@Julian Berman Now I get what you mean! The term "fragment" was throwing me off.

I don't want to propagate unstable links if it can be avoided, so I'd rather not base copyable links on the phrasing that happens to be used for a header today. So right now, permalinks are assigned to headers when they've been given unique internal identifiers; those headers have the kind of behavior you're describing. I think what I need to do is sit down and assign IDs to all headers, and add a pass in CI that makes sure they all have them.

[David Thrane Christiansen]

@Niels Voss Thank you for the great issues!

[Jason Rute]

Can we now mention/cite the reference manual in public like on this Zulip and PA.SX?

[David Thrane Christiansen]

It's completely public now. Thanks for checking!

[Shreyas Srinivas]

will the manual be updated with each toolchain release (or RCs?)

[David Thrane Christiansen]

For now, it will be updated on a regular basis, at least as often as the RCs/releases. Once there's enough content, we will additionally begin taking snapshots for each release.

[mars0i]

Will a link be added to lean-lang.org?

Maybe with a note about the relationship to the Lean 4 Manual? I've been assuming that the Reference is intended to supercede the manual in the end. Is that correct?

Very happy about this. It's great.

[David Thrane Christiansen]

mars0i said:

Will a link be added to lean-lang.org?

Yes - that should certainly be there!

[David Thrane Christiansen]

mars0i said:

Maybe with a note about the relationship to the Lean 4 Manual? I've been assuming that the Reference is intended to supercede the manual in the end. Is that correct?

Sort of - the page marked "manual" before really contained a few things: a developers' guide, a language reference, a collection of documentation links (TPiL, FPiL, etc), examples, and smaller documents like the widget description. This language reference supersedes the prior one, which was the big middle part of the page. I've installed redirects from the old content of that page to the permalinks in the new one, so they'll follow along automatically. But the language reference won't have all those things - it should do one job and do it well.

Once there's even more content in the reference, we'll take a look at how to improve the integration between all those documents and figure out how we ideally want everything organized. One step at a time...

[eyelash]

11.17. Arrays says

There is array literal syntax for writing strings.

Should this be arrays instead of strings?

[David Thrane Christiansen]

Yes! I'm out on vacation, but I'll fix it when I get back. Thanks for catching it :)

[Bryan Gin-ge Chen]

I'm not sure if I just have bad timing or not, but the links to some of the chapters seem to be intermittently broken.

For example, starting at https://lean-lang.org/doc/reference/latest, clicking on "3. The Type System" leads to a Page not found at https://lean-lang.org/the-type-system/#type-system. Oddly, the URL in the HTML points to https://lean-lang.org/doc/reference/latest/The-Type-System/#type-system, and according to my browser network request history, that's being 301 redirected to the previous URL.

Now that I've gone to the trouble of writing all that out, it seems that that specific link works again, but then links to other chapters seem to be broken for me in the same way (at the moment, the links to chapters 4. and 5. are broken). Is anyone else seeing this or is it just me?

Edit: this is on Firefox 133.0.3 on macOS 15.1.1

[Kevin Buzzard]

I just reproduced. Starting at https://lean-lang.org/doc/reference/latest I clicked on 3. The Type System in the index on the left and it worked fine. I then went back with the browser button and clicked on 4. Source files in the index on the left, and was sent to https://lean-lang.org/source-files/#The-Lean-Language-Reference--Source-Files which is a 404. Hovering over the link instead of clicking says it points to https://lean-lang.org/doc/reference/latest/Source-Files/#The-Lean-Language-Reference--Source-Files which is a different link but clicking on that seems to redirect to the earlier link which doesn't work. Now clicking on 3. The Type System doesn't work either. This on Chrome Version 130.0.6723.116 (Official Build) (64-bit) on Ubuntu.

[Michael Stoll]

When I click on "3. The Type System", I get a 404 error (from https://lean-lang.org/the-type-system/#type-system). This is on Firefox / Debian. A click on "4. Source Files" brings me to a page listing contents.

[Michael Stoll]

... but clicking on "4.2 Module Contents" (on the left) gives again a 404 (https://lean-lang.org/source-files/module-contents/#The-Lean-Language-Reference--Source-Files--Module-Contents).

[Johan Commelin]

Cc @David Thrane Christiansen

[David Thrane Christiansen]

Thanks for the reports and the @-mention - I've been AFK with family, but I'm looking into it now and will report back

[David Thrane Christiansen]

All right, I've got a workaround in place that seems to have fixed things (it was intermittently failing before, but I've just clicked a lot of links and they were all OK). Thanks again for letting me know!

[Bryan Gin-ge Chen]

Thanks! However, I'm still seeing an issue on "6. Type Classes", unfortunately, even after force-refreshing a few times.

[David Thrane Christiansen]

Hmm, I can't reproduce it from here. I wonder if the CDN is caching the bad response.

What happens if you click this link, @Bryan Gin-ge Chen?

[Bryan Gin-ge Chen]

Clicking your link works for me! I'll wait a few more hours and hopefully things will work by then.

[David Thrane Christiansen]

One more experiment: what if you go to the root of the manual, then click the link in the left?

[Bryan Gin-ge Chen]

The type classes chapter works now from the root of the manual! I clicked around on the other chapters and got a handful of errors, but after hitting back and clicking again they all seem to be working for now. Thanks again!

[David Thrane Christiansen]

Thanks for the help diagnosing it!

[Filippo A. E. Nuccio]

In section 3.4.2.4 I read

When the new structure extends existing structures, the new structure's constructor takes the existing structure's information as additional arguments. Typically, this is in the form of a constructor parameter for each parent structure type. If the parents' fields overlap, however, then the subset of non-overlapping fields from one or more of the parents is included instead to prevent duplicating field information.

and I have troubles to understand what the final "instead" refers to. I would say that including a non-overlapping field would not, at any rate, cause duplication and that including it is in accordance with the second sentence (hence my difficulty with the "instead"). What am I reading wrong?

PS: Is this the right place/stream where asking this kind of questions?

[Kyle Miller]

@Filippo A. E. Nuccio Here's how it's supposed to mean:

Suppose you have

structure A where
  a : Nat
  b : Nat
structure B where
  a : Nat
  c : Nat
structure C extends A, B

If A and B didn't share the field a, then C would be represented like

inductive C where
  | mk (toA : A) (toB : B)

However, since they share fields, instead C is represented like

inductive C where
  | mk (toA : A) (c : Nat)

and it derives a toB projection:

def C.toB (self : C) : B :=
  match self with
  | .mk toA c => { a := toA.a, c := c }

[Filippo A. E. Nuccio]

Oh, I see! So the "constructor parameter for a structure" is the whole Structure.mk with its fields embedded, whereas if some overlapping occurs, one needs to populate the explicit fields. Thanks!

[Kyle Miller]

Yeah, it tries to embed parents if possible in mk, and when it's not possible it embeds fields.

If instead Lean 4 used a "flat structures" approach (like in Lean 3) it would not embed parents, and instead it would always embed fields:

inductive C where
  | mk (a : Nat) (b : Nat) (c : Nat)

[Filippo A. E. Nuccio]

Great, thanks!

[Filippo A. E. Nuccio]

I was reading "constructor parameter for a structure" to mean "constructor parametere for each field of a structure", forcing the flatness approach in my mind.

[David Thrane Christiansen]

@Filippo A. E. Nuccio I believe that https://github.com/leanprover/reference-manual/pull/254 clarifies the text. Thanks for pointing this out!

[Filippo A. E. Nuccio]

Yes, I find this much clearer. Thank you for this beautiful book.

[Julian Berman]

(I don't see an issue for this, which I'm happy to open if the answer is "yes") -- Is describing Lean's language server functionality a topic that the reference manual might cover?

In particular at this very moment I want to interlink to Lean's docs on semantic tokens, and I know https://lean-lang.org/lean4/doc/semantic_highlighting.html?highlight=semantic#semantic-highlighting exists, but perhaps a general section covering how Lean's LS implements various language server protocol functionality is a broader topic worth covering.

[David Thrane Christiansen]

That could certainly be in scope in principle, but I don't expect that topic to be at the top of the priority list anytime soon. Very few people implement editor plugins, and I'm prioritizing topics that deliver the most benefit to the most people.

[Julian Berman]

Yes 100% understandable of course. Is it high enough to warrant filing at least or low enough that realistically it's not useful to have on the list until/unless some other use case comes up? (For my part I honestly find the LSP parts of Lean easy enough that I'm fine reading the source still so I'm not personally clamoring for this, it just occurred to me anyhow to ask.)

[David Thrane Christiansen]

I think it's fine to have an issue for this, if only so people can search for it and see that it's not likely in the near future

[David Thrane Christiansen]

Thanks!

[Alok Singh]

David Thrane Christiansen said:

That could certainly be in scope in principle, but I don't expect that topic to be at the top of the priority list anytime soon. Very few people implement editor plugins, and I'm prioritizing topics that deliver the most benefit to the most people.

I would like to bump this request since obscure topics like this and FFI are relatively easy for AI tools to implement (code isn't that complicated, but lots of background knowledge required), and encourages people to build more tools. This of course depends on how you feel about the ability of AI tools, but I've found them helpful in this regard.

[Julian Berman]

https://github.com/leanprover/reference-manual/issues/255

[David Thrane Christiansen]

Regardless of how easy it is to get something auto-generated (I haven't had good luck at the level that I think @Julian Berman is describing, vs smaller docstring-scale prose which seems to be promising), it'd still require time to set up the workflow to make it, implement tests and checked examples to keep it up to date, and review it for accuracy and comprehensiveness. It's more important to get topics of wider interest that essentially every Lean user will have a use for done first.

[Jon Eugster]

@David Thrane Christiansen inspired by the very useful language reference, I've tried to create a copy which would contain most mathlib tactics. Immediately I've stumbled on technical limitations, which I'm now "solving" with

set_option maxHeartbeats 0
set_option maxRecDepth 100000000000000000

I only have about 30 :::tactic statements in a file, which doesn't seem unreasonable. Do you think this is something that will be fixed in a more mature version of Verso+Lean-Language-Reference or will this be an inherit feature of how you've implemented the custom parsers for this project?

Also, there is no option to fold/unfold a :::tactic block (yet), is there?

[Malvin Gattinger]

I was just reading the if-then-else page and noticed that in the "Checking Array Bounds" example also this last code piece has an error that seems unintended. (It does not make the step ¬xs.size ≥ 3 ⊢ 2 < xs.size.) I thought verso would check/catch such things when generating HTML because error=false is the default for all lean blocks?

[David Thrane Christiansen]

Jon Eugster said:

I only have about 30 :::tactic statements in a file, which doesn't seem unreasonable. Do you think this is something that will be fixed in a more mature version of Verso+Lean-Language-Reference or will this be an inherit feature of how you've implemented the custom parsers for this project?

This is definitely something I've seen, but usually not for such a small file. In the end, it'd mostly depend on the complexity of the code examples being rendered. I believe this is fixable, in part by improving the code that renders Lean syntax and in part by improving Verso's integration with incremental processing of Lean files, but fixing it right now is taking a back seat to writing more content.

Jon Eugster said:

Also, there is no option to fold/unfold a :::tactic block (yet), is there?

I see them locally:
Screenshot 2025-01-24 at 23.05.10.png
Screenshot 2025-01-24 at 23.05.29.png

Have I misunderstood what you're asking for?

[David Thrane Christiansen]

Malvin Gattinger said:

I was just reading the if-then-else page and noticed that in the "Checking Array Bounds" example also this last code piece has an error that seems unintended. (It does not make the step ¬xs.size ≥ 3 ⊢ 2 < xs.size.) I thought verso would check/catch such things when generating HTML because error=false is the default for all lean blocks?

You're absolutely right, and this is disconcerting. I'll investigate! This particular error is fixed now, at least.

Thank you very much!

[Jon Eugster]

@David Thrane Christiansen thanks for the explanation, that makes sense. I think some docstrings of mathlib tactics have examples which do not parse/elaborate correctly, that might definitely add to the heartbeats.

What I meant is the folding/unfolding in the final HTML/CSS. If there already was an option to make them fold like examples to, I would have use that

Screenshot 2025-01-25 at 00.38.28.png

[David Thrane Christiansen]

Ahh, that makes sense!

To reduce the work done rendering docstrings, you can turn off the heuristics that try to understand code blocks. There's an option for that (I can look it up when I'm at the computer again).

As far as collapsible text, I get it. Right now, there's no option. I hope that some of the long text will be on its way out of docstrings, because hovers are a terrible place for reading involved paragraphs! I think a link to a manual with appropriate context is better in the long run. But we're not there yet.

In the meantime, you can make your own variant of the Verso docstring renderer and use it - that's the good thing about an extensible system. Ironically, that process is not yet so well documented - please feel free to ask questions here!

[Asei Inoue]

@David Thrane Christiansen

The concept referred to as an "inductive family" in TPiL seems to be called an "indexed family" in the language reference. I believe these refer to the same thing. Could you consider unifying the terminology? (This inconsistency in terminology has caused some confusion within the Japanese Lean community.)

TPiL: https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html#inductive-families
Reference: https://lean-lang.org/doc/reference/latest//The-Type-System/Inductive-Types/#inductive-datatypes-parameters-and-indices

[David Thrane Christiansen]

Unified terminology is a good thing!

TPiL also uses the terminology "indexed family of types" in that very section.

Issue: https://github.com/leanprover/reference-manual/issues/262

[Daniel Weber]

Is the list in https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=inductive-types-runtime-special-support exhaustive? I was under the impression that Int also has special support

[David Thrane Christiansen]

Thanks for pointing out this oversight! It's been fixed in the development repository and that'll be part of the imminent release.

[Yaël Dillies]

Could the repo's "About" link to the webpage?

[David Thrane Christiansen]

Done! Thanks!

[Yaël Dillies]

In 13.4 Defining New Syntax, it's written

The parser sets the `info` field to `none`. The parser sets the `info` field to `none`, with position retrieval continuing recursively.

[David Thrane Christiansen]

@Jon Eugster fixed this last week, and the fix will be in the imminent release. Thanks!

[Damiano Testa]

It was lucky that the text was not

The parser sets the `info` field to `none`, with position retrieval continuing recursively.
The parser sets the `info` field to `none`, with position retrieval continuing recursively.
The parser sets the `info` field to `none`, with position retrieval continuing recursively.
The parser sets the `info` field to `none`, with position retrieval continuing recursively.
...

[David Thrane Christiansen]

@Max Nowak 🐉 , @Heather Macbeth - the upcoming release has a version of the index that's a live fuzzy search box. If you'd like to give it a spin, this recent preview has it enabled - it's the box labeled "Jump to" in the upper right. Does this match what you were looking for?

[Yaël Dillies]

I tried to look in #ref for information about how import statements are stored in the AST, but could not find it. Should such information be there or is it out of scope?

[Derek Rhodes]

@Yaël Dillies, It's easier to look in the recent preview ref, linked in the previous post ^^^, there is a search bar, (yay!). According to the grammar, imports are located inside of headers, as implemented in the parser

[Yaël Dillies]

Great! I guess all I need now is knowing how to retrieve this information and then I can implement a code action for #min_imports

[Damiano Testa]

If you need position information for the imports, I think that you will have to parse the imports again.

[Damiano Testa]

You can look at parseImports', I think.

[Damiano Testa]

The header linter should do something like this and also the minImports linter, not the command.

[Jireh Loreaux]

@David Thrane Christiansen this is probably low priority, but it seems that in-text cross references get html anchors with terrible names, such as: https://lean-lang.org/doc/reference/latest/Build-Tools-and-Distribution/Lake/#--tech-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next-next

Would you like me to create an issue?

[David Thrane Christiansen]

It's a known thing that will be fixed in due time

[David Thrane Christiansen]

Thanks!

[Edward van de Meent]

i'm reading the new docs for partial_fixpoint, and have a small suggestion about the following part:

An expression is in tail position in the function body if it is:

• the function body itself,

• the branches of a match expression that is in tail position,

• the branches of an if expression that is in tail position, and

• the body of a let expression that is in tail position.

this enumeration starts as "an expression [...] is tail position if any of the following are true:", but ends as if started by "the following kinds of expressions are in tail position:". As a result, a reader might expect something to be both a branch of an if-expression and the body of a let expression...

I think getting this wording consistent is a nice improvement... should i open an issue?

[David Thrane Christiansen]

Sure!

[David Thrane Christiansen]

Thanks!

[Jireh Loreaux]

Thanks for all this new material by the way. I've been wanting good documentation on lake for a while, and it's super helpful we have it now.

[David Thrane Christiansen]

This isn't all me - @Joachim Breitner wrote the partial_fixpoint and wf-rec chapters, and @Mac Malone spent a bunch of time helping me with the Lake one. They deserve thanks too!

[Jireh Loreaux]

Then thanks also to them!

[David Thrane Christiansen]

(not to mention lots of great feedback both internally in the FRO and from here - thank you all!)

[Edward van de Meent]

reference-manual#281

[Asei Inoue]

@David Thrane Christiansen

How should I cite the Language Reference? In particular, how should I write the author's name? Should I use David Thrane Christiansen, or should it be Lean FRO?

[David Thrane Christiansen]

I'll get back to you on that one.

[David Thrane Christiansen]

@Asei Inoue Please cite the author as "The Lean Developers" - thanks for checking!

[Shreyas Srinivas]

is there a standard bibtex entry?

[David Thrane Christiansen]

There is not yet one

[Michael Rothgang]

Today, I wondered: inside a namespace Foo, does scoped instance : True := sorry do the same as scoped[Foo] instance : True := sorry. (I assume the answer is yes.)
The section on scoped does not seem to answer this at all.

[Kyle Miller]

scoped[Foo] is mathlib syntax, in Mathlib/Tactic/ScopedNS.lean

I think the answer is ~yes, but there are probably small differences

[Michael Rothgang]

So I should have done #find_syntax first (and realised this was not a question about core) - thanks!

[Mario Carneiro]

Syntax errors are shown with a stop sign that partially covers the thing that is causing the syntax error: image.png

[Mario Carneiro]

it's also not clear by looking at this whether there is another character hiding underneath the stop sign

[suhr]

In “Inductive Types” there's an explicit part for the ι-reduction. In contrast, in “Quotients” the reduction rule is mentioned in different parts of the text. Moreover, the quotient reduction rule does not have a name and is not listed in https://lean-lang.org/doc/reference/latest/The-Type-System/.

[David Thrane Christiansen]

Mario Carneiro said:

it's also not clear by looking at this whether there is another character hiding underneath the stop sign

Thanks! We'll take a look at improving that.

[David Thrane Christiansen]

suhr said:

In “Inductive Types” there's an explicit part for the ι-reduction. In contrast, in “Quotients” the reduction rule is mentioned in different parts of the text. Moreover, the quotient reduction rule does not have a name and is not listed in https://lean-lang.org/doc/reference/latest/The-Type-System/.

Thanks! Tracking issue

[David Thrane Christiansen]

@Mario Carneiro Thanks again for the feedback. This is fixed on main:

Screenshot 2025-03-14 at 09.46.30.png

[Kevin Buzzard]

Here in the discussion of the node constructor for Lean.Syntax we see "(Remark: the node constructor did not have an info field in previous versions. this caused a bug in the interactive widgets, where the popup for a + b was the same as for a. ..." Or at least
I think it says that: the two as are in different fonts, and one is hoverable whereas the other isn't. Is this intentional? (i.e. one is supposed to be some kind of atom and the other isn't?). I don't understand enough about what is going on to know whether this is supposed to be the point, or an oversight.

[Kevin Buzzard]

There are universe inconsistencies in the two examples in section 2.4. In the "Equational Lemmas" example we're shown some code with no universes mentioned, and the equational lemmas are peppered with references to universe u_1, except for thirdOfFive.eq_1 which is all about universe u. (except for when you hover, in which case you see u_1 again). Conversely the other example, "Recursive Equational Lemmas", again is a discussion about code written where no universes are mentioned, but all the equation lemmas use universe u consistently in the text (although all hovers talk about universe u_1). I don't know if this is confusing for new users, I guess my instinct is to make it consistent (and consistency within the first example would surely be desirable rather than thirdOfFive.eq_1 being the odd one out).

[Kevin Buzzard]

I think the first mention of lean4checker is a couple of paras before section 2.4.1? If I'm right, maybe there should be a link?

[Kevin Buzzard]

In the description of funext in section 3.1.3, I can hover over pretty much everything in the blue box containing the statement of the theorem (including the left and right side of colons) except for Sort u, which randomly doesn't work. Is this expected?

In the description, it says "note the Quot.sound in the proof", but I have no idea how to see the proof within the context of the reference manual.

[David Thrane Christiansen]

Thanks, @Kevin Buzzard! I'll get back to you with details tomorrow!

[Kevin Buzzard]

Let me know if you'd rather I be opening issues.

[David Thrane Christiansen]

Please do what you find easiest - when I'm on the computer tomorrow I'll go through your comments here and either fix them immediately or make issues for them.

[David Thrane Christiansen]

Thanks again!

[Kevin Buzzard]

OK perhaps in the future I'll open issues. I stopped for now because I have other things to do today. In general I really love the popups (is that the right word?) on hover, they seem to be super-effective here. They are sufficiently sparse that you don't get that phenomenon which I sometimes see in Lean code where wherever you put the cursor some (possibly huge and irrelevant) text window appears, but conversely it is a super-efficient way to get information without even having to click (and then click back).

[David Thrane Christiansen]

Thank you again for the feedback!

[David Thrane Christiansen]

Kevin Buzzard said:

Here in the discussion of the node constructor for Lean.Syntax we see "(Remark: the node constructor did not have an info field in previous versions. this caused a bug in the interactive widgets, where the popup for a + b was the same as for a. ..." Or at least
I think it says that: the two as are in different fonts, and one is hoverable whereas the other isn't. Is this intentional? (i.e. one is supposed to be some kind of atom and the other isn't?). I don't understand enough about what is going on to know whether this is supposed to be the point, or an oversight.

I'm in the process of going through every single documented item shown in the manual to make their style consistent and add the ones that are missing. Docstrings are in Markdown right now, which doesn't provide a way to indicate whether inline code is intended to be valid Lean or not, so the manual essentially guesses, applying various heuristics. What you're seeing there is a failure mode of that process, and part of my review here is adjusting them so that it succeeds. I did that docstring today, so this issue will be gone very soon.

[David Thrane Christiansen]

Kevin Buzzard said:

There are universe inconsistencies in the two examples in section 2.4. In the "Equational Lemmas" example we're shown some code with no universes mentioned, and the equational lemmas are peppered with references to universe u_1, except for thirdOfFive.eq_1 which is all about universe u. (except for when you hover, in which case you see u_1 again). Conversely the other example, "Recursive Equational Lemmas", again is a discussion about code written where no universes are mentioned, but all the equation lemmas use universe u consistently in the text (although all hovers talk about universe u_1). I don't know if this is confusing for new users, I guess my instinct is to make it consistent (and consistency within the first example would surely be desirable rather than thirdOfFive.eq_1 being the odd one out).

Getting these to all show up consistently will require a bit of work with the delaborator, getting it to show universe variables in just the right way. This kind of thing is indeed important, but I think there's higher-priority things to improve at the moment, so I created a tracking issue. Thanks!

[David Thrane Christiansen]

Kevin Buzzard said:

I think the first mention of lean4checker is a couple of paras before section 2.4.1? If I'm right, maybe there should be a link?

It's not really thought into the manual at the moment, but it should be. Issue for tracking

[David Thrane Christiansen]

Kevin Buzzard said:

In the description of funext in section 3.1.3, I can hover over pretty much everything in the blue box containing the statement of the theorem (including the left and right side of colons) except for Sort u, which randomly doesn't work. Is this expected?

In the description, it says "note the Quot.sound in the proof", but I have no idea how to see the proof within the context of the reference manual.

Two parts here:

1. The lack of hovers on Sort, Type, and Prop is just a matter of the hover-insertion code being incomplete - more an intentional choice of priorities than an oversight _per se_. It'll get better. Thank you for being vigilant there! Universe variables are also not yet highlighted in them.
2. The funext docstring itself needed revision - one principle for the review I'm doing is that all docstrings should make sense independently of the file in which they're found. This Lean PR updates the text.

[Kevin Buzzard]

Nice! It was really fun interacting with your manual!

[David Thrane Christiansen]

@Kevin Buzzard The newly-released snapshot of the manual contains the updated funextand Syntax docstrings. Thanks again!

[Julian Berman]

I don't quite know where to put this, its minor and extends beyond just the reference clearly, so feel free to tell me to move it to a new thread or file a bug obviously:

I was trying to answer the question "does the stop tactic exist" (side context: because I noticed we don't syntax highlight it in lean.nvim, and I see VSCode does, though VSCode's highlighting like mine contains things which don't exist anymore so it always requires double checking.)

So I found https://lean-lang.org/doc/reference/latest///Tactic-Proofs/Tactic-Reference/#stop -- great, it exists! Then I tried it, I thought following the doc there, writing:

example : 37 = 37 := by
  stop

and got:

  └──── unexpected end of input; expected '{'

I happen to know that error message is code for "I expect a tactic sequence and don't see one", but is there some clearer way of specifically denoting syntax in the reference planned -- in particular I see the text say "it's defined as repeat sorry", but putting that in this spot indeed works fine -- I saw the words "helper tactic" but I guess that didn't signal to me "it expects something after".

I assume longer term that maybe the reference will include BNFs or something saying the exact syntax for each tactic too?

[Mario Carneiro]

Yeah, in lean 3 this was addressed by showing the (automatically generated) BNF in the hover documentation

[Mario Carneiro]

Making BNFs should be possible by introspecting on the syntax declaration. Maybe I can interest @Kyle Miller in taking this up?

[Kyle Miller]

I know David is interested in showing BNF @Julian Berman, and for tactics I imagine that it's somewhere farther along the roadmap.

I'm not sure if there's some automatic system somewhere, but in the manual source code there are some hand-crafted simplified grammars, e.g. https://github.com/leanprover/reference-manual/blob/8bc04276e7fb1702a3789f2fb36ee5e622380e02/Manual/Language/InductiveTypes.lean#L48 appears as https://lean-lang.org/doc/reference/latest////The-Type-System/Inductive-Types/#inductive-declarations

With stop, even if there's a parse error you can do "go to definition" and see

macro "stop" tacticSeq : tactic => `(tactic| repeat sorry)

Possibly having it be a tacticSeq rather than (tacticSeq)? is a bug. (I think I'm tackling allowing empty tactic sequences this quarter, so it's possible it will work as a last tactic in the not-too-distant future.)

[David Thrane Christiansen]

I'm definitely interested in showing the grammars!

For Lean as a whole, automatically generating them really doesn't work. The problem is that the implementation of the parser doesn't necessarily match the grammar as we'd want to show it to users, because the parser takes other considerations into account. As an example, the parser accepts import A.B. (with the trailing .), even though it's not valid, with the error message generated later - this is to allow completion at that point. In other cases, two separate parsers may be implemented for something that we'd want to present to users as the "same" syntax.

These are problems that can probably be solved. The way it's solved in the manual right now is a little DSL for writing the grammar that's checked against the parsers - this ensures that the described grammar matches the parser, but not that it fully describes all valid syntax. More can certainly be done here, especially for "easy" parsers that don't do anything that's too strange.

[David Thrane Christiansen]

But writing down the grammar of each tactic using the little DSL would certainly be a nice improvement!

[Mario Carneiro]

While I think it is great that one can manually define the grammar for complicated tactics and tactics which are doing trickery, I think it is also important to have an automatic grammar generator so that even user-written tactics (and old projects unaware of the existence of grammar functionality) get BNFs without additional work

[Mario Carneiro]

I would rather have manual BNFs be an override over automatic BNFs, rather than requiring them to get docs

[David Thrane Christiansen]

I think we share the same dream and merely differ in our assessment of the work required to get there :)

[Julian Berman]

Is the reference offline? https://lean-lang.org/doc/reference/latest/ gives me a 404, which is the link shown on https://lean-lang.org/documentation/ and in the sidebar of https://github.com/leanprover/reference-manual

[Rémy Degenne]

https://lean-lang.org/doc/reference/latest/ works for me. But https://lean-lang.org/doc/reference/latest (without the final /), which is the link from the documentation page, gives me a blank page.

[Julian Berman]

Neither seem to work here.

[David Thrane Christiansen]

I'm investigating - thanks!

[Julian Berman]

Let's see whether that's my internet connection's fault...

[David Thrane Christiansen]

Looks like something went wrong with hosting, I re-ran the deploy and it seems good now

[David Thrane Christiansen]

Does it look good on your end too?

[Julian Berman]

It does, thanks for the quick fix!

[David Thrane Christiansen]

I appreciate you letting me know!

[Julian Berman]

(And now a totally unrelated question) -- what decides whether a type is clickable in the manual? E.g. on https://lean-lang.org/doc/reference/latest//Build-Tools-and-Distribution/Lake/#Lake___findModule___ I can click on say Lake.MonadWorkspace or Functor or Option, but I cannot click on e.g. Lean.Name or Lake.Module if I want to know what it is. Is that related to whether the declaration is marked public or private?

[Julian Berman]

Oh or does it just have to do with whether those appear somewhere in the reference, that'd make more sense. Yeah never mind!

[David Thrane Christiansen]

Names that occur elsewhere in the document are clickable, where "occur" can be "is documented in" or "is defined in an example". I'm currently working on porting _Functional Programming in Lean_ to Verso, where names will link either to the local book or to the reference, depending on where they come from.