RFC: Upgrading Lean versions

Kha commented 6 years ago

Suggested plan:

Inject a leanpkg lean-upgrade <version> command into leanpkg (i.e. it will only be available when calling ~/.elan/bin/leanpkg). This is not just a convenience command for editing the leanpkg.toml file: It first has to resolve channel names like stable/nightly to specific Lean versions that are valid values for the lean_version field.
Override leanpkg add and leanpkg upgrade to add a warning on lean_version mismatches between the package and its dependencies. When connected to a TTY, offer to call lean-upgrade with an appropriate version to fix the conflicts (well, at least one of them).

With these changes, installing Lean and adding a mathlib dependency could be as simple as:

$ curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh
...
$ leanpkg new mypackage  # uses stable leanpkg, doesn't matter
$ cd mypackage
$ leanpkg add leanprover/mathlib
...
WARNING: Lean version "nightly-2018-04-06" of dependency "mathlib" does not match configured Lean version "3.4.0"
Do you want to set your package's Lean version to "nightly-2018-04-06"? [yN] y
...

cipher1024 commented 6 years ago

What would you do when you add a second package that specifies a different version of Lean?

Kha commented 6 years ago

What would you do when you add a second package that specifies a different version of Lean?

Select "an appropriate version", as I said :grin: . ...probably the lexically largest version string or something

cipher1024 commented 6 years ago

Sorry! I must have missed that!

leanprover / elan

RFC: Upgrading Lean versions #7