Zulip Chat Archive

Stream: general

Topic: 3.4.1 branch


view this post on Zulip Patrick Massot (Feb 13 2019 at 21:52):

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

view this post on Zulip Patrick Massot (Feb 13 2019 at 21:52):

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

view this post on Zulip Patrick Massot (Feb 13 2019 at 21:53):

This is important because CoCalc is currently stuck with Lean 3.4.1

view this post on Zulip Patrick Massot (Feb 13 2019 at 22:36):

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

view this post on Zulip Kevin Buzzard (Feb 13 2019 at 22:56):

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.

view this post on Zulip Patrick Massot (Feb 14 2019 at 16:47):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 16:49):

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

view this post on Zulip Patrick Massot (Feb 14 2019 at 17:24):

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.

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 17:43):

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

view this post on Zulip Scott Morrison (Feb 15 2019 at 03:50):

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

view this post on Zulip Scott Morrison (Feb 26 2019 at 01:42):

@Patrick Massot, could you give a quick tutorial?

view this post on Zulip Scott Morrison (Feb 26 2019 at 01:42):

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)

view this post on Zulip Scott Morrison (Feb 26 2019 at 01:43):

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

view this post on Zulip Scott Morrison (Feb 26 2019 at 01:47):

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

view this post on Zulip Scott Morrison (Feb 26 2019 at 01:59):

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

view this post on Zulip Patrick Massot (Feb 26 2019 at 07:42):

@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

view this post on Zulip Patrick Massot (Feb 26 2019 at 07:47):

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

view this post on Zulip Patrick Massot (Feb 26 2019 at 07:48):

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.

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 09:07):

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

view this post on Zulip Patrick Massot (Feb 26 2019 at 09:27):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Mar 16 2019 at 10:14):

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.

view this post on Zulip Abhimanyu Pallavi Sudhir (Mar 16 2019 at 10:22):

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


Last updated: May 18 2021 at 16:25 UTC