Updating should use manifests from dependencies

[gebner]

Say you have three packages, then updating C (or adding the B dependency the first time) should take the version of A from B/lean_packages/manifest.json.

• A
• B, which depends on A
• C, which depends on B

(The current behavior is that updating C upgrades both A and B to the latest revision, typically breaking B in the process.)

This is crucial for using manifests with anything that depends transitively on mathlib. For example if A=mathlib, B=lean-liquid, and C=yourownproject. Projects like lean-liquid bump the mathlib version every couple of weeks, using any other mathlib version will break.

[tydeu]

Consider the following case:

• A
• B, which depends on master A (locked to version 2)
• C, which depends on master A (locked to version 1)
• D, which depends on B, C

Which version of A should be used? Or should Lake error?

[gebner]

Ideally version 2 with a warning that there are conflicting versions (including a list of these versions). Then you stand a chance of fixing it manually if that's possible.

[tydeu]

@gebner This feature would mean that lake update only updates the top-level package's direct dependencies, right? (As all downstream package versions would be determine by the depending package's manifest.)

[gebner]

I would have expected all dependency versions to be stored in the manifest, including the transitive dependencies. There might be conflicts, after all, and it seems like a good idea to record their resolution. Also you might need to fix the conflicts manually.

But generally, yes. lake update should only update the top-level dependencies from the specified git branch, and then resolve the transitive dependencies from the dependencies' manifests.

[tydeu]

@gebner

I have been working on this issue and two requests along with the main request of the PR have been difficult to harmonize.

There might be conflicts, after all, and it seems like a good idea to record their resolution. Also you might need to fix the conflicts manually.

This suggests that the top-level manifest should be a single source of truth for the dependencies of the package and thus no warnings should be issued if the revision their conflict with ones in the dependency's manifest. However, the PR's goal seems to be using the dependency's manifest as the source of truth. Thus, it is not clear when Lake should use what.

My current thought on how to solve this is to use an additional field in the package manifest to determine whether a entry is for the top-level or for a dependency (e.g., named inherited) and only update the dependencies not marked inherited. At the same time, when resolving dependencies for the first time, Lake prefers the entries in the top-level manifest (if they exist) over those of dependencies' manifest. This way users can manually adjust the manifest to solve conflicts.

Ideally version 2 with a warning that there are conflicting versions (including a list of these versions).

This suggests, when faced with a conflict (on initial resolution), Lake should use latest version from a set of conflicts. This poses some problems.

First there is the question of different input revision. For instance, adapting the my example from above, package B could want want feature-1 of A locked to some hash f00 and C could want feature-2 of A locked to ba1. While it is conceivable possible to pick the latest based on the dates of the commits, this seems improper as the two different inputs may not be strongly related to one another. Thus, my initial thought was make an input conflict a hard error. However, this prevents the production of a manifest file that the user could manually fix. On the other hand, it is not clear what should be rationally put in the manifest for such a dependency if Lake does not error in this case and simply issues a warning.

Second, assuming we do have matching input revisions, how and when do we get the the latest version. My thought is just to fetch for the latest version matching the descriptor always if two packages conflict on the specific revision. However, this could of course result in a version that neither supports. For example, they both, as in the original, want master one locked to f00, the other to ba1, Lake fetches and gets the latest master c4f which neither likes.

TL;DR 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. On initial resolution, we use whatever revision happens to appear first and users can manually update the manifest if conflicts occur. How does that sound?

[gebner]

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.