lake update does not pick up updates from transitive dependencies

[gebner]

For example mathlib3port depends on lean3port which depends on mathlib4. But running lake update in mathlib3port does not pick up the new mathlib4 version when lean3port updates its dependency.

We touched on this in another issue, but it's still an issue in the latest release. See #70 (comment):

My simplest solution to all of this is to append dependency's manifests to the top-level package's with their entries mark inherited and not update such dependencies during lake update.

"... but instead replace them with the current entry from the dependency's manifest." Otherwise sounds good to me.

[gebner]

it's still an issue in the latest release

Only partially. See #120

It turns out this already worked in some cases. Namely lake update would pick up changes in transitive dependencies, but only if the inputRev stayed the same. If the direct dependency switched to another branch of the transitive dependency, then lake update would not pick up the new revision.

[gebner]

Another issue: when updating mathport this happened:

git clone https://github.com/leanprover-community/mathport
cd mathport
git checkout db81206678e7a632e6a6490c680f4c466436b09d
lake update

Output:

Found dependency `Cli`
`mathlib` locked `master` at `112b35fc348a4a18d2111ac2c6586163330b4941`
Using `master` at `112b35fc348a4a18d2111ac2c6586163330b4941`
Found dependency `leanInk`
`mathlib` locked `master` at `439303af06465824588a486f5f9c023ca69979f3`
Using `master` at `439303af06465824588a486f5f9c023ca69979f3`
Found dependency `doc-gen4`
`mathlib` locked `main` at `a2345380e861332fabecc61591cb274e61163a97`
Using `main` at `a2345380e861332fabecc61591cb274e61163a97`
Found dependency `Unicode`
`mathlib` locked `master` at `25b32ef69fd6d8ae34300d51dc0b9403ffb1fd29`
Using `master` at `25b32ef69fd6d8ae34300d51dc0b9403ffb1fd29`
Found dependency `mathlib`
`mathlib` locked `master` at `ecd37441047e490ff2ad339e16f45bb8b58591bd`
Using `master` at `4a089ec3e1dd2953ff3242ed51a9fbed546c117a`
Found dependency `std`
`mathlib` locked `main` at `274cf5a5f906852b96bd8f4b045b243f2717edaf`
Using `main` at `23f8577169c049e6eb472a0354c11b9b934b4282`
Found dependency `lake`
`mathlib` locked `master` at `6cfb4e3fd7ff700ace8c2cfdb85056d59f321920`
Using `master` at `6cfb4e3fd7ff700ace8c2cfdb85056d59f321920`
Found dependency `CMark`
`mathlib` locked `master` at `8c0f9c1b16ee8047813f43b1f92de471782114ff`
Using `master` at `8c0f9c1b16ee8047813f43b1f92de471782114ff`

Note that the update for std4 is not picked up even though the branch stayed the same.

[tydeu]

@gebner

Found dependency `std`
`mathlib` locked `main` at `274cf5a5f906852b96bd8f4b045b243f2717edaf`
Using `main` at `23f8577169c049e6eb472a0354c11b9b934b4282`

Note that the update for std4 is not picked up even though the branch stayed the same.

Unless I am mistaken, 23f8577 is the latest version of std4. So it is updating it, it is just updating it to the latest version rather than the one mathlib locked it to. I think this is bug due to it already being in the root manifest prior to the update.

[tydeu]

Fixed by #138 (not sure why GitHub did not automatically close it already).