Zulip Chat Archive

Stream: general

Topic: Survey: who uses `leanproject up`?


Gabriel Ebner (May 06 2020 at 08:34):

We would like to change leanproject up so that it always does the equivalent of git pull && leanproject get-mathlib-cache and we would like to know if this breaks anybody's workflow. https://xkcd.com/1172/
(The only difference is if you're in a project that is not mathlib, but has a mathlib dependency. Right now leanproject up automatically upgrades the mathlib dependency.)
Are you using leanproject up in a project that is not mathlib? What do you think about this change?

Kevin Buzzard (May 06 2020 at 08:43):

I have used leanproject up as a one-stop solution to students problems ("who l why does this code I cut and pasted from Zulip not work?") and this will break it

Kevin Buzzard (May 06 2020 at 08:45):

Students are very likely to be working on projects which are not mathlib, which depend on mathlib, and which are several months old

Kevin Buzzard (May 06 2020 at 08:45):

As long as there is a super-simple way for them to do whatever leanproject up currently does that's great

Kevin Buzzard (May 06 2020 at 08:46):

They never need git pull because they never push, they don't have a clue what git is

Kevin Buzzard (May 06 2020 at 08:47):

In my experience updates to mathlib are unlikely to break their code, and needing the newest tactics is more important

Jesse Michael Han (May 06 2020 at 08:48):

Does the proposed change make leanproject up's effect on a mathlib dependency equivalent to old update-mathlib?

Patrick Massot (May 06 2020 at 08:48):

Not quite, because it also pulls the latest version of the mathlib dependent project

Patrick Massot (May 06 2020 at 08:49):

Gabriel's idea is that leanproject up is a dangerous command so it shouldn't be the easiest to type

Patrick Massot (May 06 2020 at 08:50):

His proposal would make it roughly equivalent with the old git pull && leanpkg configure && update-mathlib

Jesse Michael Han (May 06 2020 at 08:51):

i agree with this change, as it's likely nontrivial projects will suffer breaking changes from downstream versions of mathlib

Johan Commelin (May 06 2020 at 08:51):

Will there also be a leanproject bump-mathlib?

Johan Commelin (May 06 2020 at 08:52):

Ideally it should fix any errors that show up...

Patrick Massot (May 06 2020 at 08:52):

The current leanproject up would be renamed to something else of course

Johan Commelin (May 06 2020 at 08:52):

leanproject upper?

Gabriel Ebner (May 06 2020 at 08:53):

It already has two aliases: leanproject update-mathlib and leanproject upgrade-mathlib

Jesse Michael Han (May 06 2020 at 08:54):

what about leanproject update for the proposed version, and leanproject up/upgrade for the current one?

Patrick Massot (May 06 2020 at 08:54):

I'm strongly against having update and upgrade doing different things.

Patrick Massot (May 06 2020 at 08:55):

This would be extremely confusing. I put both as aliases because the world is very inconsistent here

Johan Commelin (May 06 2020 at 08:57):

Patrick Massot said:

I'm strongly against having update and upgrade doing different things.

Strongly agree with Patrick. This sounds too much like apt. And it's horrible.


Last updated: Dec 20 2023 at 11:08 UTC