mathlib must come after proofwidgets?

Stream: lean4

[Adam Topaz]

I came across some strange behavior. To reproduce, make a fresh Lean4 project with the following lakefile:

import Lake
open Lake DSL

package «foo» where
  -- Settings applied to both builds and interactive editing
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
    ⟨`pp.proofs.withType, false⟩
  ]
  -- add any additional package configuration options here

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

require "leanprover-community" / "proofwidgets" @ git "v0.0.48"

@[default_target]
lean_lib «Foo» where
  -- add any library configuration options here

and leanprover/lean4:v4.15.0-rc1 as the toolchain. Running lake exe cache get clones the deps as expected, but then fails (very slowly!) to download the cache. If I put proofwidgets ahead of mathlib in the dependencies, then it works as expected. Is this a known issue?

[Johan Commelin]

cc @Mac Malone

[Mac Malone]

The failure is curious (and needs ome debugging on my end), but I do question why you are requiring ProofWidgets at all when Mathlib already depends on it?

[Adam Topaz]

@Mac Malone what I actually have is a project A that depends on proofwidgets and a project B that depends on A and on mathlib. If proofwidgets is replaced by such an A then you should get a similar failure

[Patrick Massot]

I think that non-linear package dependencies graphs are simply not supported by lake.

[Ruben Van de Velde]

I would hope that's not the case! But you may need to spend a bit of effort to make the versions match up

[Adam Topaz]

Yes I did make sure to use the same version of proofwidgets in A as the one used in mathlib (same goes for the toolchain)

[Ruben Van de Velde]

Then I'm out of my depth :)

[Patrick Massot]

By not supported I mean not supported unless a miracle makes every version match exactly.

[Adam Topaz]

Well, in this case the versions all matched, but this strange issue still occurred.

[Adam Topaz]

By the way, it seems that proofwidgets has something to do with it. If I try to do the same thing with batteries then there are no issues at all.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Possible relevant factors are that there is special handling for proofwidgets in the Cache binary, but not for Batteries (as far as I can see). proofwidgets also uses the Lake cloud release feature whereas Batteries does not.

[Mac Malone]

@Adam Topaz I have found the problem! ProofWidgets and mathlib require different versions of batteries. The order of the dependences in the lake file determines whether Lake ends up using mathlib's or ProofWidget's. In the example case, Lake prefers ProofWidget's over Mathlib's (and the opposite is true in the reverse order).

[Adam Topaz]

Thanks!

[Kevin Buzzard]

Nice sleuthing!

[Mario Carneiro]

so it seems Patrick was right...

[Kim Morrison]

This seems very hard to avoid, because Mathlib wants to update to essentially every commit on Batteries master, whereas ProofWidgets wants to update as necessary (or I guess at least monthly when it moves to a new toolchain).

[Kim Morrison]

Looking forward to being able to specify this (i.e. that ProofWidgets doesn't care much, but Mathlib does) in the lakefiles. :-)