lean3 support

Stream: general

[Stavros]

has support for lean3 disappeared completely from the lean community website? (lean3 installation instructions, online version, etc)

[Patrick Massot]

No, the old site is still there at https://leanprover-community.github.io/lean3/

[Patrick Massot]

There is a link on the main site landing page.

[Patrick Massot]

But you should try really hard to switch to Lean 4. Lean 3 has no future at all.

[Stavros]

thank you. i considered switching to LEAN4 but i use LEAN for teaching undergrads, and there are some design choices in LEAN4 (e.g., elimination of begin .. end, elimination of some tactics like left/right, etc) which make it less appealing for teaching undergrads

[Patrick Massot]

You can bring begin and end back. Lean 4 is flexible enough to handle that. And I don't understand what you say about left and right.

[Patrick Massot]

Maybe left/right are only in Mathlib

[Patrick Massot]

But even if you don't want to use Mathlib those particular tactics are trivial to write.

[Patrick Massot]

Indeed they are in Mathlib: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/LeftRight.lean

[Stavros]

thanks. how do i "bring begin and end back"?

[Patrick Massot]

https://github.com/leanprover/lean4/blob/master/tests/lean/beginEndAsMacro.lean

[Patrick Massot]

More generally, undergrad teaching is a rather important target for Lean, and Lean 4 is meant to be better than Lean 3 also for this (or least is meant to become better). So feel free to tell us more about what you need. There is a whole stream devoted to using Lean for teaching.

[Kevin Buzzard]

@Stavros I just tell students that it's now called by ... done. The advantage of done is that if you're not done, then the error is on done, which is far easier or a beginner to spot than an error on by.

[Arthur Paulino]

If I were an undergrad student and were supposed to learn how to use some tool, I would want to use it the way that its community uses it. I wouldn't enjoy being taught Lean 3 if ppl are already using Lean 4. And I wouldn't want to be taught some different syntax when the community has already moved on

[Stavros]

Arthur Paulino said:

If I were an undergrad student and were supposed to learn how to use some tool, I would want to use it the way that its community uses it. I wouldn't enjoy being taught Lean 3 if ppl are already using Lean 4. And I wouldn't want to be taught some different syntax when the community has already moved on

true, but the purpose of my course is not to teach LEAN. the purpose is to teach formal specification and software verification to 2nd year undergraduate students. lean is just a means to an end. not an end in itself.

in terms of language simplicity, lean4 in my view is a step backwards in terms of making this technology as accessible as possible to 2nd year undergraduates. in terms of installation simplicity, lean has always been more difficult than coq. compare the nightmare of lean installation to the simplicity of coq installation.

[Jireh Loreaux]

Honest question: what do you feel is complicated about Lean 4 installation? Asking so we can consider improvements.

[Arthur Paulino]

Coq is also much older. Probably like two decades older?

My take on Jireh's question: Rust has a close to ideal setup. It takes a 1-liner command on terminal to install basically everything needed. Then there's also a centralized host for packages and people can add dependencies by their names. Going in the direction of Rust setup would be a good target IMO.

Imagine the following:

$ lake new foo
$ cd foo
$ lake add mathlib

[Scott Morrison]

If you already have git / curl / VS Code installed, then installing Lean just consists of:

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

and

code --install-extension leanprover.lean4

[Scott Morrison]

And then

lake new my_project math

for a new project.

[Scott Morrison]

lake add mathlib4 is probably a good idea!

[Stavros]

Jireh Loreaux said:

Honest question: what do you feel is complicated about Lean 4 installation? Asking so we can consider improvements.

sorry, i was primarily referring to lean3. although i vaguely remember trying to install lean4 about 1 year ago and failing (and giving up). that was 1 year ago, so the situation is probably different now.

btw, i'm using windows. not sure if this is the source of the complexity (it shouldn't be). but having something that runs fine, and coming 6 months later and seeing something different (squiggly blue lines where none were there, for example) is unacceptable user experience. and unforgiving student experience.

[Arthur Paulino]

The "closer to ideal" (in my opinion) would be dropping the dependency on Git and having something like a lakes.io. That would enable calling packages by their names more consistently.

@Stavros Lean 4 is still new. We should expect even more changes for the better now that the Lean FRO is alive. If you don't want your dev environment to change, keep the toolchain file stable.

[Arthur Paulino]

@Scott Morrison here's another thing, but I apologize upfront for recurring to the Rust setup model so often (I just find it so organized and clean).

If you go to the Rust setup page, it only teaches you how to install the core of the language support. It doesn't mention particular text editors or their extensions.

The Lean 4 setup seems to take the opposite path and focuses on VS Code support. A more natural order (to me!) would teach the core language setup first and then present extra tooling: extensions for VS Code, Emacs and NeoVim

[Scott Morrison]

I don't think this is a good idea. Using Lean for anything beyond "hello world" requires an editor with LSP support.

[Arthur Paulino]

Yes, and that can be explicitly mentioned. It's just that the order in which things are presented influences on how people understand the structure of what they're installing on their machines.

If the instructions start with the extension, I imagine "is Lean 4 a VS code extension?". Then I see a command to install the backend (the language server) and all of a sudden it feels backwards

Note that I am trying to make an effort to see this through the eyes of someone who has no preconceived ideas about the Lean 4 development environment

[Scott Morrison]

There are two conflicting things going on here:

• we have users who would prefer (or we would prefer) not to use the command line
• we have users who very much understand the command line, and would like to know what is happening

For non-command line users, the instructions:

• install VSCode
• install the Lean4 extension
• click OK in a dialogue asking if you want to install Lean4
  has a certain appeal!

[Eric Wieser]

Often that second path is best even for the command line users, as otherwise they often start asking how to run lean non-interactively from the command line, and we have to explain how much harder this will make learning the language.

[Eric Wieser]

(which is to say, we likely lose some of these users immediately post-installation)

[Patrick Massot]

The issue with the install through VSCode path is that it doesn't play nice with getting the cache.

[Arthur Paulino]

I will say an idea because I don't think it's too radical: a mathlib vs code extension. It could do pretty much everything with buttons, from installing Lean 4, to downloading mathlib to getting the cache. Also: performing Git operations, running tests, linters, synchronizing Mathlib.lean etc etc

[Scott Morrison]

Patrick Massot said:

The issue with the install through VSCode path is that it doesn't play nice with getting the cache.

This is something we are looking forward to fixing by getting lake and cache fast enough that we can just invoke cache get on every lake build, so users don't need to think about it.

[Scott Morrison]

But we're not quite there.

[Yaël Dillies]

Stavros said:

in terms of language simplicity, lean4 in my view is a step backwards in terms of making this technology as accessible as possible to 2nd year undergraduates.

I must say Stavros has a point here. Lean 4 syntax is less forgiving, refine and have complain when they can't figure out metavariables instead of making them new goals (this is particularly harmful when figuring out a proof), error squiggles are often not placed where you would modify the proof to fix them, it's hard to know what to hover to see the info you want, etc...

[Yaël Dillies]

And those observations are corroborated by the level of questions asked by beginners at Lean workshops: they are much more basic now that we're on Lean 4 than when we we're in Lean 3.

[Mario Carneiro]

refine and have complain when they can't figure out metavariables instead of making them new goals (this is particularly harmful when figuring out a proof)

you can use refine' and have' , these are core tactics intended for the purpose

[Mario Carneiro]

error squiggles are often not placed where you would modify the proof to fix them

I assume you are thinking of something specific for this

[Mario Carneiro]

As always, the answer to all of these problems is to come up with a particular (specific) solution and propose it in an RFC issue on lean 4

[Yaël Dillies]

Mario Carneiro said:

you can use refine' and have' , these are core tactics intended for the purpose

Okay but:

• You yourself said that you were hoping to kill them all in one fell swoop. Is that not on the roadmap anymore?
• Those tactics actually suffer the same problem that, when typeclass inference is stuck on a metavariable, they don't create new goals for the type and its typeclass assumptions, but instead fail and don't let me see the goal.

[Yaël Dillies]

The squiggle problem I'm thinking of typically appears when you use a focusing dot. If the focused goal isn't solved, the squiggle appears on the dog, which is not where you would modify the proof to finish off the focused goal! I appreciate that there's no closing curly bracket to put the squiggle on anymore, but I'd think that squiggling the last line of the focused goal is strictly better than squiggling the focusing dot.

[Kevin Buzzard]

This is why I am constantly telling people to use done -- it solves that problem. The same issue existed in Lean 3 but people didn't notice it because end was compulsary whereas done is not.

[Kyle Miller]

@Yaël Dillies Here's a frown operator for expressing displeasure about synthesis failure while at the same time turning failures into plain metavariables.

import Lean
import Mathlib.Data.Fintype.Card

section
open Lean Elab Term Meta

/-- `:-( t` elaborate `t` but turn all synthesis problems into metavariables. -/
syntax (name := frown) ":-( " term : term

@[term_elab frown]
def elabFrown : TermElab := fun stx expectedType? =>
  withTheReader Term.Context (fun ctx => { ctx with ignoreTCFailures := true }) do
    withSynthesize do
      let e ← Term.elabTerm stx[1] expectedType?
      synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
      return e

example : Prop := by
  refine' _ + _ = _
  /-
  typeclass instance problem is stuck, it is often due to metavariables
  HAdd ?m.1578 ?m.1579 ?m.1588
  -/

example : Prop := by
  refine' :-( _ + _ = _
  /-
  case refine'_1
  ⊢ ?refine'_4
  case refine'_2
  ⊢ ?refine'_5
  case refine'_3
  ⊢ ?refine'_7
  case refine'_4
  ⊢ Type ?u.1896
  case refine'_5
  ⊢ Type ?u.1895
  case refine'_6
  ⊢ HAdd ?refine'_4 ?refine'_5 ?refine'_7
  case refine'_7
  ⊢ Type ?u.1894
  -/

example (α : Type _) : True := by
  have' := :-( Fintype.card α = 1
  /-
  case refine'_2
  α: Type ?u.1938
  this: Prop
  ⊢ True
  case refine'_1
  α: Type ?u.1938
  ⊢ Fintype α
  -/

[Yaël Dillies]

Thanks, I love it!

[Yaël Dillies]

This still doesn't quite match Lean 3 behavior, where the latter wouldn't work because we know there's no Fintype alpha in sight. But that works for my purposes!

[Kevin Buzzard]

Running a tactic which you know wouldn't work is definitely not lean's problem :-)

[Mario Carneiro]

Yaël Dillies said:

Mario Carneiro said:

you can use refine' and have' , these are core tactics intended for the purpose

Okay but:

• You yourself said that you were hoping to kill them all in one fell swoop. Is that not on the roadmap anymore?

That's something else. You said that they are useful for proof exploration, and I said that I want them to not be preferred in completed mathlib proofs. Both things can be true

[Mario Carneiro]

exact? is also something that is useful for writing proofs that we don't want in mathlib

[Mario Carneiro]

Besides, if there is a code action that automatically converts your refine's into refines then there is no downside to just using them and letting the computer clean up afterward

[Yaël Dillies]

Ah! That I can stand behind. :smile:

[Shreyas Srinivas]

Stavros said:

Jireh Loreaux said:

Honest question: what do you feel is complicated about Lean 4 installation? Asking so we can consider improvements.

sorry, i was primarily referring to lean3. although i vaguely remember trying to install lean4 about 1 year ago and failing (and giving up). that was 1 year ago, so the situation is probably different now.

btw, i'm using windows. not sure if this is the source of the complexity (it shouldn't be). but having something that runs fine, and coming 6 months later and seeing something different (squiggly blue lines where none were there, for example) is unacceptable user experience. and unforgiving student experience.

Squiggly "blue" lines are usually suggestions of some sort (like with simp? And exact?). They are an upgrade, not a downgrade.

I am surprised to hear that coq is considered easy to install. I had to fight with coq-platform for a few days before vscoq worked without a problem and even then I had to spend a lot of time to understand how to make _CoqProject files work.

Point being, even though lean has much room for improvement, I think the install and UX experience is at least somewhat subjective, and maybe there is a generation gap (where generation does not refer to age, but to the tools a person first got comfortable with when they started out, like the paper tape generation, vim/emacs generation, the atom/vscode generation, etc).

[Jireh Loreaux]

Shreyas, there was a bug about a year ago where the extension underlined everything in blue, which is super annoying. I think that's probably what the OP experienced.

[Miguel Marco]

About the difficulty of installation, this thread is related:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/trylean.20bundle.20for.20lean4