8
$\begingroup$

The syntax of Lean 3 is documented in the Lean Reference Manual chapters on expressions, match expressions, declarations, other commands, attributes, and so forth. It's spread out, and I don't think everything is fully covered (patterns, for example), but this material was very helpful.

Lean 4 has different syntax. Where is it documented?

A formal grammar would be ideal. I'm interested in the parts of the syntax that are fixed, not syntax extensions.

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ By design, basically everything in Lean4 is a syntax extension. The Lean prelude file is the only one I know without any extensions whatsoever and it illustrates all the basic syntax features. github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean $\endgroup$
    – François G. Dorais
    Commented Jul 14, 2023 at 2:19
  • $\begingroup$ "basically everything in Lean4 is a syntax extension" Yes and no. The tactics language is very much like that. Expressions are halfway like that. But the five links in the question show that a lot of the most fundamental, important syntax, stuff users will use constantly and need to understand, is built in. $\endgroup$
    – Jason Orendorff
    Commented Jul 14, 2023 at 16:04
  • $\begingroup$ What is your application? I think François’s point is that even if you had such a formal grammar, it would quickly fail since you would quickly run into extensions to the syntax. Is this for parsing Lean or just to understand how Lean syntax works? $\endgroup$
    – Jason Rute
    Commented Jul 14, 2023 at 16:07
  • $\begingroup$ Just to understand how Lean syntax works, in order to understand code I'm reading, and/or use Lean for anything at all, however basic -- to prove simple theorems of first-order logic, for example. $\endgroup$
    – Jason Orendorff
    Commented Jul 14, 2023 at 18:33
  • 4
    $\begingroup$ I think it is entirely reasonable to ask "what is the formal grammar of this language?" Answering the question with "you don't want the formal grammar" just avoids the fact that the designers of the language should pay someone to write the reference manual. It's no fun to get information as a trickle on Zulip. $\endgroup$
    – Andrej Bauer
    Commented Jul 15, 2023 at 21:27

1 Answer 1

Reset to default
5
$\begingroup$

It seems in general there are two approaches to learning a programming language. I think an older approach is a complete encyclopedic reference manual which lays out the whole language in one go, mentioning all the possible declarations, all the attributes, all the syntax at once. I can tell that is what you prefer.

Another approach, which seems more common to me today is a tutorial which progressively introduces the most common features and maybe never gets to the obscure ones. Things aren’t as easy to look up for reference, they can be tediously slow for experts, and some features get missed.

I think in July 2023 the closest to a reference manual is the very incomplete Lean 4 manual. It references a lot, especially the newer features not available in Lean 3. But it is not complete or even as encyclopedic as you would like. If you already know Lean 3, then you may find the part on significant differences from Lean 3 helpful.

As for tutorials, there are at least three:

  • Theorem Proving in Lean 4 is a tutorial on theorem proving in Lean 4. It covers in a lot of detail both the basic Lean syntax and how to prove theorems in Lean. Since your goal is to “understand code I'm reading, and/or use Lean for anything at all, however basic -- to prove simple theorems of first-order logic, for example”, I think this would go a long way to fulfilling your needs. Chapters 1-4 cover how to prove theorems in FOL without tactics. The next chapter covers tactics.
  • Functional programming in Lean focuses on Lean 4 as a fully capable Lean functional programming language. Again it takes a fairly slow approach and likely misses important features.
  • Metaprogramming in Lean 4 covers more advanced topics for those who want to do things like make their own tactics. It’s less official.

There are also other resources as well for learning Lean 4.

But again, I am sorry to say I don’t think there yet exists exactly what you are looking for.

Improve this answer
$\endgroup$
6
  • 5
    $\begingroup$ The reference manuals are not "the old way' but "the correct way" that allows people to actually get the information they seek. The so called "tutorials" are some sort of cheap marketing gimmick for the Tik Tok generation. You may call me an old fart. $\endgroup$
    – Andrej Bauer
    Commented Jul 15, 2023 at 21:25
  • 3
    $\begingroup$ In the 90s we had books. Those worked pretty well too. $\endgroup$
    – Andrej Bauer
    Commented Jul 16, 2023 at 6:43
  • 2
    $\begingroup$ Thanks for this kind answer. I love tutorials, but they aren't very helpful when I'm trying to write a proof and struggling to remember some bit of syntax I think I saw once. The tutorials are (quite properly) organized around the concepts they're trying to teach, not the syntax. This makes the syntax hard to find. Searching for have or · in a tutorial doesn't work. $\endgroup$
    – Jason Orendorff
    Commented Jul 16, 2023 at 12:48
  • 1
    $\begingroup$ @JasonOrendorff Fair enough. I deleted the second half of my answer. $\endgroup$
    – Jason Rute
    Commented Jul 16, 2023 at 15:51
  • 2
    $\begingroup$ Why should you choose between tutorial and reference manual? I believe we need both, the first to have a reasonable path to learning a new language, the second for experts/advanced users who want a quick path to a precise and complete description of a feature… Maybe they've seen it somewhere and want to learn how it works, maybe they use it already but don't remember some detail, but in all cases, a tutorial simply does not do that job. On the other hand, learning from a reference manual clearly is a horrible and painful experience. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Jul 20, 2023 at 9:53

Not the answer you're looking for? Browse other questions tagged or ask your own question.