pinned dependencies

Stream: mathlib4

[Arthur Paulino]

Why aren't mathlib4 dependencies pinned by git hashes? I think it can cause weird behaviors for packages that depend on mathlib.

For example, @Siddhartha Gadgil 's LeanAide uses the same pinning method from mathlib (using master revision on the lakefile), but it downloaded a different version of Aesop from the one that's explicited on mathlib's manifest.

In https://github.com/yatima-inc we manage a web of ~8 different Lean packages with dependencies pinned by git hashes and we don't run into this problem

[Mauricio Collares]

(deleted useless question)

[Siddhartha Gadgil]

Indeed I was going to ask what happens if a dependency is transitive through too different routes, perhaps with one direct. For instance a few days ago "lake update" repeatedly gave me the wrong version of "docgen" and only manually updating made things work.

[Henrik Böving]

Arthur Paulino said:

Why aren't mathlib4 dependencies pinned by git hashes? I think it can cause weird behaviors for packages that depend on mathlib.

For example, Siddhartha Gadgil 's LeanAide uses the same pinning method from mathlib (using master revision on the lakefile), but it downloaded a different version of Aesop from the one that's explicited on mathlib's manifest.

In https://github.com/yatima-inc we manage a web of ~8 different Lean packages with dependencies pinned by git hashes and we don't run into this problem

If a dependency provides a lake manifest file lake will of course do the sane thing and use the trans dependencies as locked by the dependencies, in fact it even tells you this in the stdout.

Siddhartha Gadgil said:

Indeed I was going to ask what happens if a dependency is transitive through too different routes, perhaps with one direct. For instance a few days ago "lake update" repeatedly gave me the wrong version of "docgen" and only manually updating made things work.

did you lake update or lake -Kdoc=on update in the first case lake will of course pretend that the doc-gen4 dependency doesn't exist since it is only optionally enabled if the Kdoc=on is enabled. If you enable that during update everything works and has always worked since the doc-gen4 CI started running.

[Arthur Paulino]

@Henrik Böving try the repo I pointed out and you will see. It silently downloads a different Aesop version

[Siddhartha Gadgil]

Henrik Böving said:

Arthur Paulino said:

Why aren't mathlib4 dependencies pinned by git hashes? I think it can cause weird behaviors for packages that depend on mathlib.

For example, Siddhartha Gadgil 's LeanAide uses the same pinning method from mathlib (using master revision on the lakefile), but it downloaded a different version of Aesop from the one that's explicited on mathlib's manifest.

In https://github.com/yatima-inc we manage a web of ~8 different Lean packages with dependencies pinned by git hashes and we don't run into this problem

If a dependency provides a lake manifest file lake will of course do the sane thing and use the trans dependencies as locked by the dependencies, in fact it even tells you this in the stdout.

Siddhartha Gadgil said:

Indeed I was going to ask what happens if a dependency is transitive through too different routes, perhaps with one direct. For instance a few days ago "lake update" repeatedly gave me the wrong version of "docgen" and only manually updating made things work.

did you lake update or lake -Kdoc=on update in the first case lake will of course pretend that the doc-gen4 dependency doesn't exist since it is only optionally enabled if the Kdoc=on is enabled. If you enable that during update everything works and has always worked since the doc-gen4 CI started running.

I did lake update -Kdoc=onso docgen4 did update. What it changed to though was not the latest commit at that time. I could not figure out where the specific commit came from (did not try much as I just wanted stuff working for the start of my course).

[Henrik Böving]

So regarding your repo @Siddhartha Gadgil why do you have boht a lean-packages and a lean_packages? Those are mutually exclusive, lake switched the naming and the manifest in modern :tm: lake projects is in the top level directory and the directory is called lake-packages etc. Which is because your Lean compiler version is oudated quite a while.

If you were to update to a modern version of mathlib4 everything should just blow up at the compilation phase for you already.

[Arthur Paulino]

I think his lean-packages directory is simply ignored by Lake. I suspect it's not relevant

[Siddhartha Gadgil]

I have forgotten to delete the old manifest, though I have been maintaining lake-manifest. I assumed that the old one will be ignored.

[Siddhartha Gadgil]

In any case, I will delete it.

[Siddhartha Gadgil]

I am using the latest version of mathlib4 and making sure my lean-toolchain is in sync.

[Siddhartha Gadgil]

The file was just a vestigial organ.

[Henrik Böving]

Ah you are on the mathlib4 instead of the master branch I see

[Henrik Böving]

lets check again then

[Siddhartha Gadgil]

This time it has updated to the latest version and has worked fine.

[Henrik Böving]

Okay so on a clean checkout of your mathlib4 branch I get

λ lake -Kdoc=on update
updating ./lake-packages/mathlib to revision cac724d14d1f733658a9d0e0ad5c81db20a9f802
cloning https://github.com/xubaiw/CMark.lean to ././lake-packages/CMark
cloning https://github.com/leanprover/lake to ././lake-packages/lake
cloning https://github.com/leanprover/doc-gen4 to ././lake-packages/doc-gen4
cloning https://github.com/mhuisi/lean4-cli to ././lake-packages/Cli
cloning https://github.com/hargonix/LeanInk to ././lake-packages/leanInk
cloning https://github.com/xubaiw/Unicode.lean to ././lake-packages/Unicode

Mathlib references c4477a2a7931e2490339d8087f599a45e89f25e7 as aesop commit and the aesop in lake-packages is checked out at c4477a2a7931e2490339d8087f599a45e89f25e7 what is the issue?

[Henrik Böving]

Ah it updated fine this time

[Henrik Böving]

Well in that case tell me when you see the behaviour next time and I'll have a look

[Siddhartha Gadgil]

Sure. Thanks.