Zulip Chat Archive

Stream: general

Topic: Survey: who uses `leanproject up`?


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (May 06 2020 at 08:48):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 06 2020 at 08:50):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 06 2020 at 08:51):

Will there also be a leanproject bump-mathlib?

view this post on Zulip Johan Commelin (May 06 2020 at 08:52):

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

view this post on Zulip Patrick Massot (May 06 2020 at 08:52):

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

view this post on Zulip Johan Commelin (May 06 2020 at 08:52):

leanproject upper?

view this post on Zulip Gabriel Ebner (May 06 2020 at 08:53):

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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (May 06 2020 at 08:54):

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

view this post on Zulip 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

view this post on Zulip 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: May 12 2021 at 03:23 UTC