Zulip Chat Archive
Stream: Lean for the curious mathematician 2020
Topic: Tuesday afternoon
Rob Lewis (Jul 14 2020 at 10:59):
Heads up everyone, we'll start again soon, with Jeremy Avigad's talk on "Mathematics in Lean: logic"
Join Zoom Meeting
https://vu-live.zoom.us/j/95402085900
Meeting ID: 954 0208 5900
Password: 333537
Rob Lewis (Jul 14 2020 at 11:59):
We're now working in breakout rooms on @Jeremy Avigad 's exercises. Please let me know if you'd like to join a room, want to change rooms, or anything like that. We'll reconvene for my talk in an hour :)
Filippo A. E. Nuccio (Jul 14 2020 at 13:57):
What was the link for the exercices on norm_cast?
Alex J. Best (Jul 14 2020 at 13:57):
leanproject get lftcm2020
Filippo A. E. Nuccio (Jul 14 2020 at 13:57):
Thanks!
Rob Lewis (Jul 14 2020 at 14:03):
There's another tactic for dealing with natural numbers that you may find helpful: zify. Is your goal about nats but you want it to be about ints? Try zify!
Filippo A. E. Nuccio (Jul 14 2020 at 14:08):
@Rob Lewis Are your exercices on norm_cast in the Tuesday folder?
Rob Lewis (Jul 14 2020 at 14:08):
Rob Lewis (Jul 14 2020 at 14:09):
I'm sorry for the confusing location of the exercises!
Jeremy Avigad (Jul 14 2020 at 15:56):
The set exercises file was broken in the lftcm2020 repository, but it has been repaired now. So if you have been enjoying the set exercises, you can update the repository to find more of them.
Rob Lewis (Jul 14 2020 at 16:02):
It's 6pm, people are slowly trickling out. We can leave the rooms open for a while -- no need to end on the hour! Ping me if your room is too quiet or lacking a tutor and I'll move you around.
Rob Lewis (Jul 14 2020 at 16:17):
@Jeremy Avigad is the host now. Ping him if you need anything.
Floris van Doorn (Jul 14 2020 at 16:22):
I'm in a very quiet room now, so if a tutor wants to leave, I'm happy to have more participants in by room.
Jeremy Avigad (Jul 14 2020 at 17:00):
We're done for the day! Until tomorrow, everyone.
Danila Kurganov (Jul 14 2020 at 18:29):
Thanks for today! How do we update the set.lean file from today which includes any fixes?
Jalex Stark (Jul 14 2020 at 18:30):
git pull?
Johan Commelin (Jul 14 2020 at 18:30):
leanproject up
Vaibhav Karve (Jul 14 2020 at 18:30):
Are git pull and leanproject up equivalent?
Jalex Stark (Jul 14 2020 at 18:30):
no, I think i may be confused about what this file is
Johan Commelin (Jul 14 2020 at 18:31):
Not really... for this example, probably "yes"
Jalex Stark (Jul 14 2020 at 18:31):
in a project that depends on mathlib (e.g. one created by leanproject new or leanproject get), leanproject up will pull the latest mathlib into your _target folder
Jalex Stark (Jul 14 2020 at 18:31):
and find oleans, and update the leanpkg.toml to point to the version of mathlib you just downloaded
Jalex Stark (Jul 14 2020 at 18:31):
git pull will pull the source for the current project
Vaibhav Karve (Jul 14 2020 at 18:32):
Right. Thanks!
Jalex Stark (Jul 14 2020 at 18:32):
i don't know if the set.lean mentioned upthread is a mathlib file or a file in a project for lftcm notes
Jalex Stark (Jul 14 2020 at 18:33):
i would expect leanproject up to work for the former and git pull to work for the latter
Johan Commelin (Jul 14 2020 at 18:33):
I was assuming that the file in the lftcm repo was meant...
Johan Commelin (Jul 14 2020 at 18:33):
maybe leanproject up is doing too much...
Jalex Stark (Jul 14 2020 at 18:34):
oh, it didn't occur to me that leanproject up will also pull the source of the current project
Jalex Stark (Jul 14 2020 at 18:35):
Johan Commelin said:
I was assuming that the file in the lftcm repo was meant...
i think it's not doing too much; people who want to do less also know how
Kevin Buzzard (Jul 14 2020 at 18:49):
I thought that leanproject up will also bump mathlib. I often find myself in situations where I don't want this to happen
Patrick Massot (Jul 14 2020 at 19:08):
Noooo!
Patrick Massot (Jul 14 2020 at 19:09):
Doing leanproject up is orthogonal to the actual answer.
Patrick Massot (Jul 14 2020 at 19:09):
Abbreviations should be forbidden. leanproject up is short for leanproject upgrade-mathlib.
Patrick Massot (Jul 14 2020 at 19:10):
What you want to do is not to use a more recent version of mathlib, it's updating the project files.
Patrick Massot (Jul 14 2020 at 19:10):
So you simply want git pull
Johan Commelin (Jul 14 2020 at 19:11):
Ooops... sorry for the bad advice
Patrick Massot (Jul 14 2020 at 19:12):
And that's all, unless someone authoring this lftcm2020 project decided it needed a more recent mathlib, in which case leanproject get-mathlib-cache is needed to download the compiled version of this new mathlib.
Patrick Massot (Jul 14 2020 at 19:13):
Now we can see from https://github.com/leanprover-community/lftcm2020/commits/master/leanpkg.toml that Scott decided he needed a newer mathlib 13 hours ago. So if you ran leanproject get lftcm2020 more than 13 hours ago then you'll need leanproject get-mathlib-cache after the git pull.
Jeremy Avigad (Jul 14 2020 at 19:14):
Uh oh. As an exercise author, I may have done leanproject up at some point. I am not sure. But nobody seemed to have trouble today....
Patrick Massot (Jul 14 2020 at 19:14):
But only the authors of this Lean project ever need to leanproject up in it, and only if they want a cutting-edge mathlib
Patrick Massot (Jul 14 2020 at 19:16):
Maybe it's a good time to paste a link to the leanproject documentation
Jeremy Avigad (Jul 14 2020 at 19:17):
Got it. It looks like Scott was the last person to do it, 13 hours ago.
What happens if someone starts the project in VS Code, and they don't have the same version of mathlib?
Jeremy Avigad (Jul 14 2020 at 19:24):
Oh, sorry, I see the answer in the thread. Nevermind.
Floris van Doorn (Jul 14 2020 at 19:25):
In my talk I will remind everyone to do git pull and leanproject get-mathlib-cache before starting.
Kevin Buzzard (Jul 14 2020 at 19:27):
Alternatively, do leanproject up 15 minutes before and then fix all the errors :P
Sebastien Gouezel (Jul 14 2020 at 19:30):
What if I have some exercises that I want to upload to lftcm2020 but they depend on a yet unmerged PR to mathlib, aka #3387?
Floris van Doorn (Jul 14 2020 at 19:30):
I was always surprised that leanproject upgrade-mathlib got abbreviated, but leanproject get-mathlib-cache didn't. I use the latter way more often.
Patrick Massot (Jul 14 2020 at 19:42):
Kevin, we'll prepare a special breakout room for your and all the participants that won't understand you're joking. :stuck_out_tongue_wink:
Patrick Massot (Jul 14 2020 at 19:44):
Floris, I think this is mostly a historical accident.
Patrick Massot (Jul 14 2020 at 19:45):
Note that since release 0.0.9 you can use any unambiguous prefix of a command. So leanprojet get-m is good enough :wink:
Scott Morrison (Jul 15 2020 at 00:35):
@Sebastien Gouezel, my vote would be that we prematurely merge that PR, and deal with any problems next week. :-)
Scott Morrison (Jul 15 2020 at 00:35):
A slightly safer alternative would be we create an lftcm2020 branch of mathlib, merge your PR into that, and have lftcm2020 require that branch as its dependency.
Last updated: Dec 20 2023 at 11:08 UTC