lake exe cache get failed to get github releases

Stream: lean4

[Jafar Tanoukhi]

I'm using Gitpod, but I'm receiving this error after simply creating a Gitpod workspace on my mathlib4 fork and running lake exe cache get.

image.png

I've tried running lake clean and lake update before lake exe cache get and still same issue.

[Jafar Tanoukhi]

Also, is there a way to build mathlib locally without using cache at all?

[Aaron Liu]

Jafar Tanoukhi said:

Also, is there a way to build mathlib locally without using cache at all?

That would be lake build, but it takes five hours on my machine and I don't know how many it will take on yours.

[Aaron Liu]

You would still need to checkout the dependencies though

[Jafar Tanoukhi]

Aaron Liu said:

That would be lake build, but it takes five hours on my machine and I don't know how many it will take on yours.

image.png

This is the error I received on GitPod when running lake build. Same error.

[Jafar Tanoukhi]

image.png
Locally, it just starts as if I did lake exe cache get.
Locally, it does lake exe cache get for any command, even lake clean

[Jafar Tanoukhi]

For context, I am using Gitpod and not doing it locally because lake exe cache get continuously fails on my internet connection. A 5-hour build is nothing for me if that's all it takes, but I can't get it to actually build for some reason, and it appears as if it will still ask for lake exe cache get at some point.

[Niels Voss]

Can you send the output of something like lake build -v? And to confirm, from your gitpod instance, you can access the internet (so commands like curl https://google.com work) right?

[Aaron Liu]

Jafar Tanoukhi said:

Aaron Liu said:

That would be lake build, but it takes five hours on my machine and I don't know how many it will take on yours.

image.png

This is the error I received on GitPod when running lake build. Same error.

This is what I meant by "you will still need to checkout the dependencies", you don't have up to date proofwidgets so you can't build until you update it

[Wang Jingting]

I also met the same problem while running CI for mathlib, in https://github.com/leanprover-community/mathlib4/actions/runs/17906080667/job/50907383060#step:34:18 CI failed in get cache 1/3 with the same error as above. Does anyone know why this is happening?

[Jafar Tanoukhi]

Aaron Liu said:

This is what I meant by "you will still need to checkout the dependencies", you don't have up to date proofwidgets so you can't build until you update it

Is there a way to retrieve proof widgets without running lake exe cache get so I can run lake build? My thought was that the cache was created purely so that nobody has to wait the 5+ hours to build, but if you are willing to wait, then lake build should work fully offline. (I'm not sure if this is a stupid question:sweat_smile:)

[Jafar Tanoukhi]

Niels Voss said:

Can you send the output of something like lake build -v?

This outputted a huge mess, so i will just paste below as much as I can. Also, yes, I can access the internet from the gitPod instance.

ℹ [7229/7231] Replayed Batteries.Lean.Meta.Simp
trace: .> LEAN_PATH=/home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.24.0-rc1/bin/lean /home/runner/work/reservoir/reservoir/testbed/repo/Batteries/Lean/Meta/Simp.lean -o /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Lean/Meta/Simp.olean -i /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Lean/Meta/Simp.ilean -c /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Lean/Meta/Simp.c --setup /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Lean/Meta/Simp.setup.json --json
ℹ [7230/7231] Replayed Batteries.Lean.SatisfiesM
trace: .> LEAN_PATH=/home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.24.0-rc1/bin/lean /home/runner/work/reservoir/reservoir/testbed/repo/Batteries/Lean/SatisfiesM.lean -o /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Lean/SatisfiesM.olean -i /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Lean/SatisfiesM.ilean -c /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Lean/SatisfiesM.c --setup /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Lean/SatisfiesM.setup.json --json
ℹ [7232/7244] Replayed Batteries.Lean.Util.EnvSearch
trace: .> LEAN_PATH=/home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.24.0-rc1/bin/lean /home/runner/work/reservoir/reservoir/testbed/repo/Batteries/Lean/Util/EnvSearch.lean -o /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Lean/Util/EnvSearch.olean -i /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Lean/Util/EnvSearch.ilean -c /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Lean/Util/EnvSearch.c --setup /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Lean/Util/EnvSearch.setup.json --json
ℹ [7233/7244] Replayed Batteries.Tactic.Instances
trace: .> LEAN_PATH=/home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.24.0-rc1/bin/lean /home/runner/work/reservoir/reservoir/testbed/repo/Batteries/Tactic/Instances.lean -o /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Tactic/Instances.olean -i /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Tactic/Instances.ilean -c /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Tactic/Instances.c --setup /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Tactic/Instances.setup.json --json
ℹ [7234/7244] Replayed Batteries.Tactic.Lemma
trace: .> LEAN_PATH=/home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.24.0-rc1/bin/lean /home/runner/work/reservoir/reservoir/testbed/repo/Batteries/Tactic/Lemma.lean -o /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Tactic/Lemma.olean -i /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Tactic/Lemma.ilean -c /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Tactic/Lemma.c --setup /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Tactic/Lemma.setup.json --json
ℹ [7235/7244] Replayed Batteries.Tactic.NoMatch
trace: .> LEAN_PATH=/home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.24.0-rc1/bin/lean /home/runner/work/reservoir/reservoir/testbed/repo/Batteries/Tactic/NoMatch.lean -o /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Tactic/NoMatch.olean -i /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Tactic/NoMatch.ilean -c /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Tactic/NoMatch.c --setup /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Tactic/NoMatch.setup.json --json
ℹ [7236/7244] Replayed Batteries.Tactic.PrintDependents
trace: .> LEAN_PATH=/home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.24.0-rc1/bin/lean /home/runner/work/reservoir/reservoir/testbed/repo/Batteries/Tactic/PrintDependents.lean -o /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Tactic/PrintDependents.olean -i /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Tactic/PrintDependents.ilean -c /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Tactic/PrintDependents.c --setup /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Tactic/PrintDependents.setup.json --json
ℹ [7237/7244] Replayed Batteries.Tactic.PrintOpaques
trace: .> LEAN_PATH=/home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.24.0-rc1/bin/lean /home/runner/work/reservoir/reservoir/testbed/repo/Batteries/Tactic/PrintOpaques.lean -o /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Tactic/PrintOpaques.olean -i /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Tactic/PrintOpaques.ilean -c /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Tactic/PrintOpaques.c --setup /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Tactic/PrintOpaques.setup.json --json
ℹ [7238/7244] Replayed Batteries.Tactic.PrintPrefix
trace: .> LEAN_PATH=/home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.24.0-rc1/bin/lean /home/runner/work/reservoir/reservoir/testbed/repo/Batteries/Tactic/PrintPrefix.lean -o /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Tactic/PrintPrefix.olean -i /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Tactic/PrintPrefix.ilean -c /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Tactic/PrintPrefix.c --setup /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Tactic/PrintPrefix.setup.json --json
ℹ [7239/7244] Replayed Batteries.Tactic.ShowUnused
trace: .> LEAN_PATH=/home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.24.0-rc1/bin/lean /home/runner/work/reservoir/reservoir/testbed/repo/Batteries/Tactic/ShowUnused.lean -o /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Tactic/ShowUnused.olean -i /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Tactic/ShowUnused.ilean -c /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Tactic/ShowUnused.c --setup /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Tactic/ShowUnused.setup.json --json
ℹ [7240/7244] Replayed Batteries.Tactic.SqueezeScope
trace: .> LEAN_PATH=/home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.24.0-rc1/bin/lean /home/runner/work/reservoir/reservoir/testbed/repo/Batteries/Tactic/SqueezeScope.lean -o /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Tactic/SqueezeScope.olean -i /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Tactic/SqueezeScope.ilean -c /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Tactic/SqueezeScope.c --setup /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Tactic/SqueezeScope.setup.json --json
ℹ [7241/7244] Replayed Batteries.Util.Pickle
trace: .> LEAN_PATH=/home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.24.0-rc1/bin/lean /home/runner/work/reservoir/reservoir/testbed/repo/Batteries/Util/Pickle.lean -o /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Util/Pickle.olean -i /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries/Util/Pickle.ilean -c /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Util/Pickle.c --setup /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries/Util/Pickle.setup.json --json
ℹ [7242/7244] Replayed Batteries
trace: .> LEAN_PATH=/home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.24.0-rc1/bin/lean /home/runner/work/reservoir/reservoir/testbed/repo/Batteries.lean -o /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries.olean -i /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/lib/lean/Batteries.ilean -c /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries.c --setup /home/runner/work/reservoir/reservoir/testbed/repo/.lake/build/ir/Batteries.setup.json --json
Some required targets logged failures:
- proofwidgets/widgetJsAll
error: build failed

[Rémy Degenne]

I got the same error. I can't run lake exe cache get successfully on my machine because it fails to get proofwidgets.

[Burkhardt Renz]

I have the same problem. Yesterday I initialized a new project and all got well, but today?? Does anybody know what to do?

[Riccardo Brasca]

There is a (private) discussion about this in the reviewers stream, so people are aware of the issue and it will hopeful solved soon.

[Jafar Tanoukhi]

Any news on this issue? Is this happening to everyone or only some people?

My understanding is that automated PR checks are also failing due to this issue.

[Jafar Tanoukhi]

Not sure if this was just a coincidence, and this was already fixed, but deleting the .lake folder and trying again worked for me.

[Mario Carneiro]

This seems to still be broken. From v4.25.1 branch of mathlib I can't lake exe cache get:

$ lake exe cache get
lake stdout:
error: build failed
lake stderr:
error: build failed
uncaught exception: Failed to validate ProofWidgets cloud release: lake failed with error code 1

[Ruben Van de Velde]

I understood 4.25.2 was released to fix this