Lean 4 vs 3? Binary / build system?

Stream: new members

[Daniel Patterson]

I'm wondering about Lean 4 vs Lean 3 for a course starting in January (with a couple hundred students). It _seems_ like Lean 4 is still somewhat unstable (though maybe that's more just about std4/mathlib4? At least I haven't managed to get a version of those that builds), but on the other hand, the package / build system seems a bit more refined. Concretely, Mac ARM binaries are distributed for Lean 4, but not (as far as I can tell) for Lean3, so the official (again, as far as I can tell) instructions involve Rosetta complexity, which doesn't seem ideal.

Assuming I don't need Mathlib (or much of it), is Lean4 stable enough at this point? Or will it be in a couple months? Or am I better off dealing with the (seemingly more clunky) build/setup for Lean 3?

[Adam Topaz]

What is the course about? I think the answer will heavily depend on that!

[Adam Topaz]

In any case, you may want to take a look at the #Lean for teaching stream as well

[Daniel Patterson]

It's a course introducing formal specification and logic to lower-level (computer science) undergrads -- I certainly don't need math results! Re-implementing things from scratch is also pretty much okay. The only library code that I'd really love to include (though could probably re-implement / port, though it does appear in the mathlib4 source tree) is slim_check, since we'll start with property based testing in a functional language the students are familiar with before transitioning to Lean.

[Moritz Doll]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Anything.20like.20QuickCheck/near/295995057 and I think that in general Lean 4 is better for CS-related things. I don't know enough about Lean 4 to judge the stability - it feels rather stable, but I have only used a very small part.