reference manual

Stream: new members

[Alexandre Rademaker]

what is the repository of the reference manual source files? I found some typos in the https://leanprover.github.io/reference/tactics.html#basic-tactics and I would like to make some suggestions.

[Bryan Gin-ge Chen]

Here, possibly: https://github.com/avigad/reference

[Alexandre Rademaker]

Thank you @Bryan Gin-ge Chen , I made a PR but this is actually a fork from another repo. Let us see which one is the 'official'.

[Robert Watson]

Where can I find a complete version of the reference manual? Thanks.

[Mario Carneiro]

https://leanprover.github.io/reference/

[Robert Watson]

So, there aren't units 7 and 8 yet, then? At least this version doesn't have anything for units 7 and 8. What is the way to systematically learn Lean as a programming language? Tactics is only a surface layer. I can watch a few videos for sure, but that isn't the same as doing it abc from the beginning up.

[Robert Watson]

I've done quite a bit of tactics mode already, enough to get things done with them.

[Henrik Böving]

If you want to learn Lean as a programming language instead of as a you'll most likely want to take a look at Lean 4 instead of 3 since 4 is actually designed to be one unlike 3.

Unfortunately we don't really have extensive resources for teaching Lean as a programming language as of now. Basically everyone who knows Lean 4 learned it by reading Lean 4 source code that already exists. Most prominently compiler code and mathlib4 code. + Of course the theorem proving in Lean 4 port here https://leanprover.github.io/theorem_proving_in_lean4/ and the lean 4 manual here https://leanprover.github.io/lean4/doc/whatIsLean.html (which is even further away from completion than this reference manual)

If/Once you hit a road block because of some functional programming concepts like Functors, Monads etc. you can almost always just search for a Haskell resource about it since these abstractions are mathematical ones and hence translate easily across programming languages. If you have any questions the Lean 4 stream will be happy to help as well^^

[Robert Watson]

A reference manual isn't really teaching materials, it's documentation. Having spent a good deal of time on tactics and proofs, I would be able to work through documentation, but I would not be able to work through source code.

[Henrik Böving]

Do you have a computer science or math background? I can imagine its pretty hard to pull off with a math background but having a computer science one I can tell you, I used to think this way as well but the thing that was mostly stopping me was just thinking I wouldn tunderstand it, if you put in the time and especially patience it's very doable.

[Henrik Böving]

Especially since proving is just a subset of regular programming in Lean you actually already know a lot of things we do when we write regular programs in Lean 4, it's mostly just more syntax or concepts you can learn from Haskell docs and apply rather easily to Lean

[Robert Watson]

It's the syntax and language specification (a full list of everything that the core language can do) that, without a reference manual, are opaque.

[Henrik Böving]

They are opaque iff you are not willing to learn from source code yes

[Robert Watson]

Let me rephrase the question then: are there any resources for guiding newbies through the source code so that they can get a solid grounding in the core language, syntax and so on?

[Henrik Böving]

https://leanprover.github.io/theorem_proving_in_lean4/title_page.html does teach most of the basic mechanisms we use, the majority of other things is (lots of) syntactic sugar on top

[Henrik Böving]

If you start doing real programming with stuff like input output you also most likely want to read a Monad tutorial out of which there are an insane amount out there for Haskell trying to explain the concept in various ways...its a thing lots of new purely functional programmers get stuck on for a while in the beginning but once you understand it everything related to it feels rather easy, getting to that point can take a while though.

[Robert Watson]

Yeah, I can understand that! Not the issue I have though - am looking for a reference manual that sadly doesn't exist yet!! Thanks anyway...amazing super-on-the-ball community that's for sure. I might try to go through the source code as you have stated is necessary for my purposes. Have a good holiday weekend.

[Arthur Paulino]

I am building an interpreter for a language that I am creating in Lean 4. It's obviously simpler than Lean so it might serve as a smaller codebase to start off from:
https://github.com/arthurpaulino/FxyLang

[Arthur Paulino]

Eventually I will get it documented to serve as some sort of tutorial. But for now it's just code

[Robert Maxton]

I will just point out that the difference in mental overhead between reading source code, especially in a language you don't understand, and reading actual plain-english documentation, is tremendous
in much the same way that, I don't know, reading an unannotated proof is much harder than reading a textbook, or even a paper
'learn from the source code' isn't really a reasonable expectation, imo

[Ruben Van de Velde]

The lack of documentation at this point isn't a matter of policy, but just a lack of time while the implementation is finished

[Kevin Buzzard]

Lean is a project, not a finished product. People are writing what they can.

[Eric Wieser]

Right now the lean3 reference manual is in leanprover not leanprover-community, so presumably in this case we can't actually write any more of it?

[Robert Watson]

In the following video https://www.youtube.com/watch?v=-RQQxFVZnn4&t=0s "the documentation" is mentioned at 19.40ish. He even talks about what is in the documentation and it doesn't match anything in Theorem Proving in Lean as far as I can tell, whilst Programming in Lean seems to be mainly stubs, and you wouldn't refer someone to a series of stubs. So, I'm nodding along to him thinking "sure, sure, all I have to do is look up all the other related tactics in the documentation". Which sounds great! But I am confused as to what he is referring to.

[Henrik Böving]

Most likely this https://leanprover-community.github.io/mathlib_docs/ respectively this https://leanprover-community.github.io/mathlib4_docs/ for Lean 4. But you at least have to know a certain location to look at already

[Henrik Böving]

But @Rob Lewis is here so he probably knows best himself :P

[Chris B]

Or https://leanprover-community.github.io/extras/tactic_writing.html.

[Chris B]

Ch 7 of the hitchhikers guide is also in the description, so he might have meant that.

[Robert Watson]

That last one is certainly useful given the topic. In any case it gives some essential reference material I was looking for. Can I just clarify something that might seem dumb: where did the people who wrote the hitchhikers guide chapter 7 get their syntax information from without a reference manual?...my understanding is that they got their knowledge of the syntax straight from the source code (maybe because they contributed to writing it or some such)? Is that right?

[Chris B]

It's very difficult to say, documentation has changed over time and a lot of information probably travels between users informally. My guess is that the early adopters looked at the original research paper outlining the tactic system quite a bit since it's fairly in-depth and has been around since 2017: https://leanprover.github.io/papers/tactic.pdf

[Robert Watson]

OK. Interesting. I just found that paper myself referenced in one of the tactics_writing links above. I've also noticed that Programming in Lean chapter 8 (even this chapter is incomplete unfortunately) is mentioned in Hitchhikers chapter 7, and there is a paper mentioned there too...which is the same as this one I think. Looks like we've drilled down as far as this rabbit hole goes. Presumably there actually is enough here to dive into some of the source code as well, at least those parts written in Lean itself. Changing documentation which is never completed makes me feel a bit queasy though, but that just goes back to Kevin Buzzard's point about work-in-progress! Still, thanks for the help everyone.

[Arthur Paulino]

Of course it's not ideal, but in my experience it's always been worth the effort to dig Lean source code to understand how something works (I am talking about Lean 4 here). I often find new and better ways to do things

[Arthur Paulino]

It also depends on your learning style. I am a slow paced and long term learner

[Robert Watson]

@Henrik Böving advised looking at the mathlib documentation. Both Lean3 and Lean4 have some auto-generated documentation for both core (eg. Init, Std, Lean and such) as well as mathlib. OK I get that. I'm going to try to dig into that but my thoughts are that what is needed here is a reference manual for that core language, that is, once you have a handle on the core then the mathlib auto-generated documentation would make a whole deal more sense, or at least you could work through it slowly. You wouldn't necessarily need a full reference manual for mathlib at all at first. For example, the first thing I encounter when I look at core.lean is a command called 'prelude', it's also in some of the Init files. This is present in Lean3 and Lean4, so it must be pretty important. I really don't want to skip over that (don't answer here, I'll make a separate thread). Maybe I'm off the mark here, but that's where I feel I want to start, at least after all the great taster videos and newbie exercises: right at the beginning, from the ground up, in the core of the language!

[Henrik Böving]

(Actually the prelude command is almost completely irrelevant and you can ignore it, it merely means "dont import Init" wich is something the majority of lean users will never wanna do)