Survey: who uses `leanproject up`?

Stream: general

[Gabriel Ebner]

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]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Jesse Michael Han]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Jesse Michael Han]

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

[Johan Commelin]

Will there also be a leanproject bump-mathlib?

[Johan Commelin]

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

[Patrick Massot]

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

[Johan Commelin]

leanproject upper?

[Gabriel Ebner]

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

[Jesse Michael Han]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Johan Commelin]

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.