3.4.1

Stream: general

[Sebastian Ullrich]

I've updated the super, mini_crush, and smt2_interface packages to use Lean 3.4.1 via elan and pushed a lean-3.4.1 branch for each of them

[Kevin Buzzard]

Sebastian thank you for doing all this tedious infrastructure work. Things are really getting good now and hopefully things will be relatively stable really soon, with people sticking to 3.4.1.

[Kevin Buzzard]

One of my students last year said "this is all a bit beta isn't it" -- but this really might change in the near future. It would be interesting to see how easily we can make everything work in 3.4.1.

[Kevin Buzzard]

Could we even dream of a one-click install for Lean 3.4.1 + mathlib on Windows?

[Johan Commelin]

... + elan + git + vscode + ... ?

[Kevin Buzzard]

I'm not sure a generic mathematics undergraduate needs all that extra stuff

[Kevin Buzzard]

in fact that's exactly the problem

[Kevin Buzzard]

I have been installing git and msys2 on undergraduate's laptops

[Kevin Buzzard]

but in the future I don't think these will be necessary, we just stick with 3.4.1.

[Kevin Buzzard]

Mathlib 3.3.0 is so primitive in comparison.

[Kevin Buzzard]

No complex numbers and no norm_num and no ring tactic

[Kevin Buzzard]

all of which are essential tools for mathematicians

[Mario Carneiro]

Remember though that unlike lean 3, mathlib has no plans to stop at 3.4.1, so if you try to park yourself at the mathlib 3.4.1 tag then you will be missing stuff in a month

[Johan Commelin]

True, but Kevin's point is that Lean should now be stable. So there is only 1 moving target.

[Sebastian Ullrich]

@Mario Carneiro If you're not planning to fork Lean, you should really do development on a lean-3.4.1 branch. This is how leanpkg is supposed to be used. If you don't want to bother with keeping the master branch in sync, just delete it.

[Sebastian Ullrich]

lean.js 3.4.1 is now live at https://leanprover.github.io/live/latest/

[Johan Commelin]

@Sebastian Ullrich Wunderbar! Thanks for all your efforts.

[Kevin Buzzard]

lean.js 3.4.1 is now live at https://leanprover.github.io/live/latest/

...and you have mathlib there too? Which version of mathlib?

[Kevin Buzzard]

I was sitting here like a lemon waiting to be told that there was a version of mathlib which compiled against 3.4.1...

[Johan Commelin]

The leanpkg.toml says lean_version = "nightly-2018-04-20"

[Kevin Buzzard]

Are they the same? [modulo changes in docs etc]?

[Kevin Buzzard]

Why is the 3.4.1 build marked as failing for linux in the README?

[Mario Carneiro]

mathlib head should compile with 3.4.1 since nothing really changed, but updating is a bit of administrative work that I haven't got around to yet

[Kevin Buzzard]

@Mario Carneiro what is the situation here? I would like to tell the CoCalc people to install some version of mathlib (so we can have multiplayer lean), and I would like to tell my students to install some version of mathlib, and it would be easiest for me if I could point them to something called "3.4.1 stable", or some sort of release version of mathlib, rather than just pointing them to mathlib HEAD or some random commit. Of course, if you would rather leave things as they are for a while then I will just point them to a random commit (perhaps first asking you whether there are any mathlib commits which should be avoided for some reason).

[Mario Carneiro]

Sorry, I'm wrapping up my finals over here and haven't had time for mathlib. It is on top of my lean priorities.

[Kevin Buzzard]

Oh thanks for the update! Of course if you have proper academic stuff to do this comes first. I am happy to wait. I just didn't know where we were and part of me is desperate to see what CoCalc can do :-)

[Patrick Massot]

Don't we still need to come up with some answer to https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/CoCalc/near/126068881 ?

[Patrick Massot]

I really have no idea what a CoCalc interface to Lean could look like

[Kevin Buzzard]

There are several questions and my impression is that all of them are being worked on.

[Kevin Buzzard]

William Stein has been thinking about interfaces, but I am using the fact that we haven't got mathlib installed on CoCalc yet as an excuse to think about other things :-)

[Patrick Massot]

Actually I have no idea how CoCalc works. Will it use normal Lean running on a server or the JavaScript version?

[Kevin Buzzard]

normal lean running on a server. That's why it's interesting

[Kenny Lau]

I'm mainly interested by the fact that we can collaborate

[Patrick Massot]

Ok, so we could have something like https://stackblitz.com/

[Patrick Massot]

Really getting close to using VScode locally

[Kenny Lau]

interesting

[Johan Commelin]

@Patrick Massot That looks really cool!

[Johan Commelin]

@William Stein Do you know about stackblitz.com? If not, it might serve as some inspiration for a Lean IDE for CoCalc. But I don't know how hard it would be to get the collaborative features working with it. (And collaboration is awesome!)