3.4.1 branch

Stream: general

[Patrick Massot]

Is there any reason the 3.4.1 branch of mathlib is stuck long before the actual move to 3.4.2?

[Patrick Massot]

Isn't https://github.com/leanprover-community/mathlib/commit/2c5bc214d1391659611591f4c6af222f2bea8e05 the actual end of compatibility with Lean 3.4.1?

[Patrick Massot]

This is important because CoCalc is currently stuck with Lean 3.4.1

[Patrick Massot]

It looks like I managed to get a reasonable mathlib running on CoCalc
cocalc.png
My students will love that

[Kevin Buzzard]

Patrick -- my experience says that more of them will like the Props than the tactics. The tactics are intimidating to most people, even though we find them easy. The propositions are very easy to understand.

[Patrick Massot]

Patrick -- my experience says that more of them will like the Props than the tactics. The tactics are intimidating to most people, even though we find them easy. The propositions are very easy to understand.

I'm not sure what you mean. Do you mean they will like the definition of limits better than the proofs? My goal is to teach them how to prove stuff about such definitions

[Kevin Buzzard]

I mean that after showing them a bunch of Lean I have learnt that students have little trouble understanding the tactic state but a lot of trouble understanding what the hell to type into VS Code because in the last year we accidentally learnt 1000 tactics and names of lemmas and techniques which are now second nature to us

[Patrick Massot]

I agree we also need that formatting mode where every Lean is hidden except for the tactic state. This is only a matter of finding time to implement it, there is no difficulty.

[Kevin Buzzard]

I'm not trying to rush you, I am just thinking about teaching next academic year :-)

[Scott Morrison]

@Patrick Massot, I would love to hear how you have CoCalc set up at the moment. I have students arriving soon!

[Scott Morrison]

@Patrick Massot, could you give a quick tutorial?

[Scott Morrison]

When I go to cocalc today, it seems to have lean 3.4.2 installed, and it works great from the command line. (e.g. I can compile a project with a dependency on mathlib, using leanpkg build)

[Scott Morrison]

However, the Lean editor built into cocalc just says it can't resolve the imports.

[Scott Morrison]

Sorry, false alarm, restarting the project makes everything work! Awesome sauce. :-)

[Scott Morrison]

Okay --- one defect: things only work perfectly if everything is in the root directory.

[Patrick Massot]

@Scott Morrison you've found https://github.com/sagemathinc/cocalc/issues/3589 which is the only thing that is slightly annoying with the current state of Lean in CoCalc. You can go there and ask for the current status of this issue

[Patrick Massot]

The workaround is pretty clear: ask students to create at the root of their project, a file leanpkg.path containing:

builtin_path
path /ext/lean/lean/mathlib/src/
path /home/user/assignments/

The last line is the only one you may want to change. In my workflow, I put all students assignments in folders like assignments/assignment1, assignments/assignment2 etc. Each folder assignment$i contains two files resources.lean containing all mathlib import, special teaching lemmas and tactics, and a file assignment$i.lean which starts with import assignment$i.resources

[Patrick Massot]

Unfortunately you cannot directly create leanpkg.path for your students because the root of their project is the only place you can't put a file in.

[Kevin Buzzard]

You can send them a setup script and ask them to run it I guess.

[Patrick Massot]

It's not much easier than tell them to copy paste three lines in a file with a given name

[Abhimanyu Pallavi Sudhir]

Scott Morrison you've found https://github.com/sagemathinc/cocalc/issues/3589 which is the only thing that is slightly annoying with the current state of Lean in CoCalc. You can go there and ask for the current status of this issue

I'm trying to get mathlib imports working on CoCalc right now -- what's the workaround mentioned in https://github.com/sagemathinc/cocalc/issues/3589? All my files are already in the home directory, but that doesn't seem to be enough.

[Abhimanyu Pallavi Sudhir]

Oops, found the workaround, couldn't see it in search, sorry. Got it -- it really is pretty great.