Zulip Chat Archive

"and then what" can either be interpreted as frustration or a request for further technical instructions, among other things. I guess Johan interpreted it as the former (which makes sense), but please clarify if you meant something else.

Jared green (Jan 10 2025 at 15:46):

i change the toolchain to 4.15.0, and then what is the next step?

Jared green (Jan 10 2025 at 15:57):

like, how do i install that version now? and roll back the mathlib if thats required

Mauricio Collares (Jan 10 2025 at 15:57):

Then lake exe cache get should work. If it doesn't, please tell us what the error is

Mauricio Collares (Jan 10 2025 at 15:58):

Do you have a lakefile.lean or a lakefile.toml in your project?

Jared green (Jan 10 2025 at 15:58):

i have both files

Mauricio Collares (Jan 10 2025 at 15:59):

Unexpected, but in this case lakefile.lean should take precedence

Mauricio Collares (Jan 10 2025 at 15:59):

You should have a line like this in there:

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

Mauricio Collares (Jan 10 2025 at 16:00):

Update it to look like this:

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

Jared green (Jan 10 2025 at 16:00):

actually i have lakefile.lean

Mauricio Collares (Jan 10 2025 at 16:00):

Then run lake update

Jared green (Jan 10 2025 at 16:12):

attempting to download 5826 files, 5664 downloads failed

Mauricio Collares (Jan 10 2025 at 16:13):

Can you paste the full output of lake exe cache get?

Kevin Buzzard (Jan 10 2025 at 16:13):

Maybe this is nothing to do with the 4.16-rc1 cache issue. Did you try deleting .lake and running lake update again?

Jared green (Jan 10 2025 at 16:18):

lake exe cache get
info: downloading component 'lean'
Total: 245.7 MiB Speed: 19.6 MiB/s
info: installing component 'lean'
error: ././.lake/packages/proofwidgets/lakefile.lean:40:14: error: unknown constant 'Lake.Job.collectArray'

error: ././.lake/packages/proofwidgets/lakefile.lean:46:29: error: invalid field notation, type is not of the form (C ...) where C is a constant
deps
has type
?m.4714 fs deps✝¹ __do_lift✝

error: ././.lake/packages/proofwidgets/lakefile.lean:78:2: error: type mismatch
widgetJsAllTarget pkg.toPackage false
has type
FetchM (Job (Array FilePath)) : Type
but is expected to have type
FetchM (BuildJob (Array FilePath)) : Type

error: ././.lake/packages/proofwidgets/lakefile.lean:81:2: error: type mismatch
widgetJsAllTarget pkg.toPackage true
has type
FetchM (Job (Array FilePath)) : Type
but is expected to have type
FetchM (BuildJob (Array FilePath)) : Type

error: ././.lake/packages/proofwidgets/lakefile.lean: package configuration has errors

Jared green (Jan 10 2025 at 16:22):

then i try it again after changing the lakefile:
lake exe cache get
warning: manifest out of date: git revision of dependency 'mathlib' changed; use lake update mathlib to update it
error: ././.lake/packages/proofwidgets/lakefile.lean:40:14: error: unknown constant 'Lake.Job.collectArray'

error: ././.lake/packages/proofwidgets/lakefile.lean:46:29: error: invalid field notation, type is not of the form (C ...) where C is a constant
deps
has type
?m.4714 fs deps✝¹ __do_lift✝

error: ././.lake/packages/proofwidgets/lakefile.lean: package configuration has errors

Mauricio Collares (Jan 10 2025 at 16:22):

Yeah, that's definitely not expected after lake update (this means you're on a version of proofwidgets suitable for v4.16.0-rc1). I'd recommend following Kevin's suggestion of just deleting .lake and running lake update again.

Jared green (Jan 10 2025 at 16:48):

i did that. i still get:
5664 downloads failed
error: mathlib: failed to fetch cache

Kevin Buzzard (Jan 10 2025 at 16:49):

What is the first error that you get?

Kevin Buzzard (Jan 10 2025 at 16:50):

Do you have some kind of lean-toolchain v lakefile.lean mismatch? Can you post the contents of both files?

Jared green (Jan 10 2025 at 16:52):

the whole project is at https://github.com/jaredgreen2/polySat

Jared green (Jan 10 2025 at 16:54):

that by the way is the first error i get

Kevin Buzzard (Jan 10 2025 at 16:58):

I can reproduce at this end.

buzzard@buster:~/lean-projects$ git clone git@github.com:jaredgreen2/polySat.git
Cloning into 'polySat'...
remote: Enumerating objects: 242, done.
remote: Counting objects: 100% (242/242), done.
remote: Compressing objects: 100% (156/156), done.
remote: Total 242 (delta 151), reused 168 (delta 77), pack-reused 0 (from 0)
Receiving objects: 100% (242/242), 80.91 KiB | 541.00 KiB/s, done.
Resolving deltas: 100% (151/151), done.
buzzard@buster:~/lean-projects$ cd polySat/
buzzard@buster:~/lean-projects/polySat$ ls
lakefile.lean       lean-toolchain  PolySat.lean
lake-manifest.json  PolySat         README
buzzard@buster:~/lean-projects/polySat$ lake exe cache get
info: Duper: cloning https://github.com/leanprover-community/duper.git
info: Duper: checking out revision '07456e26254a478db9a48b0a37d9f5b8c8022dbc'
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '9837ca9d65d9de6fad1ef4381750ca688774e608'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '8d6c853f11a5172efa0e96b9f2be1a83d861cdd9'
info: auto: cloning https://github.com/leanprover-community/lean-auto.git
info: auto: checking out revision '4d73b99262f1ce80a33ac832bef26549cf3c2034'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '2c57364ef83406ea86d0f78ce3e342079a2fece5'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '003ff459cdd85de551f4dcf95cdfeefe10f20531'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '9a0b533c2fbd6195df067630be18e11e4349051c'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '2b000e02d50394af68cfb4770a291113d94801b5'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '2689851f387bb2cef351e6825fe94a56a304ca13'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'f0c584bcb14c5adfb53079781eeea75b26ebbd32'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '0c8ea32a15a4f74143e4e1e107ba2c412adb90fd'
Attempting to download 5664 file(s)
Downloaded: 0 file(s) [attempted 5664/5664 = 100%] (0% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
Decompressing 162 file(s)
Unpacked in 208 ms
Completed successfully!
buzzard@buster:~/lean-projects/polySat$

In your lakefile.lean you are requiring mathlib v4.15.0 (which uses Lean v4.15), duper v0.0.21 (which uses Lean v4.14.0) and LeanCopilot v1.5.1 (which uses Lean v4.11.0-rc1) so my guess is that things are not going to go too well in general, but I don't know if that is the cause of the Downloaded: 0 file(s) issue.

Jared green (Jan 10 2025 at 17:04):

require leancopilot... is commented out. as for duper, i could remove that too unless @Josh Clune updates duper first.

Kevin Buzzard (Jan 10 2025 at 17:05):

You're absolutely right and I don't understand what's going on.

Josh Clune (Jan 10 2025 at 17:12):

Jared green said:

require leancopilot... is commented out. as for duper, i could remove that too unless Josh Clune updates duper first.

I intend to push a version of Duper compatible with v4.15.0 within the next couple of days. Apologies for any inconvenience caused by the delay

Jared green (Jan 10 2025 at 17:13):

but i am not so sure thats the problem necessarily

Kevin Buzzard (Jan 10 2025 at 17:13):

FWIW I commented out the Duper dependency and still get 0 files downloaded; furthermore nothing builds because batteries won't build.

Jared green (Jan 10 2025 at 17:16):

you have to eliminate it from the lake-manifest too

Mauricio Collares (Jan 10 2025 at 18:06):

I assume the problem has been solved already, but just to confirm: commenting out duper from the lakefile and rerunning lake update restores the cache functionality. The reason, as alluded above, is that duper and mathlib require conflicting batteries versions.

Jared green (Jan 10 2025 at 19:40):

i get errors in the infoview:/Users/programr/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/bin/lake setup-file /Users/programr/polySat/PolySat/basic2.lean Init Init.Data.List Init.PropLemmas Mathlib.Data.List.Dedup Mathlib.Data.List.Pairwise Mathlib.Data.List.Basic Mathlib.Data.List.Defs Mathlib.Data.List.Infix Mathlib.Data.List.Lattice Mathlib.Data.List.Lemmas Mathlib.Data.Bool.AllAny Mathlib.Data.Bool.Basic Mathlib.Logic.Basic Batteries.Data.List.Lemmas Batteries.Data.List.Basic PolySat.IList Aesop` failed:

stderr:
warning: ././.lake/packages/proofwidgets/lakefile.lean:28:63: warning: Lake.BuildJob has been deprecated: use Lake.Job instead

warning: ././.lake/packages/proofwidgets/lakefile.lean:40:13: warning: Lake.BuildJob.collectArray has been deprecated: use Lake.Job.collectArray instead

(there is more where that came from, but i am dealing with them one at a time)

Jared green (Jan 10 2025 at 19:56):

it might help if i had all the dependencies on a version compatible with 4.15. for proofwidgets, thats 0.0.49

Mauricio Collares (Jan 10 2025 at 20:53):

The infoview errors stem from the fact that it still does seem to be using v4.16.0-rc1 for some reason. Perhaps you need to restart the server, or perhaps lean-toolchain got overwritten somehow

Jared green (Jan 10 2025 at 21:18):

i changed it to 4.15 because 4.16-rc1 has issues

Mauricio Collares (Jan 11 2025 at 14:07):

Sure, I remember that. What I meant was the opposite: The infoview logs you pasted start with /Users/programr/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/bin/lake, implying an old v4.16.0-rc1 server is still running somewhere. So restarting VS Code should fix it.

Jared green (Jan 11 2025 at 14:22):

done

Josh Clune (Jan 12 2025 at 01:22):

Jared green said:

require leancopilot... is commented out. as for duper, i could remove that too unless Josh Clune updates duper first.

Duper version v0.0.22 has been pushed and is now compatible with Lean version v4.15.0.

Wrenna Robson (Mar 06 2025 at 11:31):

I am having this issue on a project I haven't worked on for a while, I was trying to update it.

Wrenna Robson (Mar 06 2025 at 11:32):

It is a public repo: https://github.com/linesthatinterlace/xmss

Wrenna Robson (Mar 06 2025 at 11:33):

Possibly I need to update the lean toolchain but I thought lake update would do that for me?

Wrenna Robson (Mar 06 2025 at 11:34):

Hmm, no, looks like
curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
fixed it...

Jon Eugster (Mar 06 2025 at 11:46):

I seem to remember that lake update tries to update the toolchain, but in order to succeed it needs to be able to parse the new lakefile with the old toolchain. This is because the copying is defined as post-update hook in the lakefile. So if the lakefile syntax changed it might fail. (this might be an outdated memory from about a year or two ago when I had these issues frequently, not sure if anything happened on this front recently).

So yes, updating lean-toolchain first manually (e.g. with your curl) is the more robust way.

Yaël Dillies (Mar 06 2025 at 11:48):

This happened to me just yesterday when moving from v4.14.0-rc1

Last updated: May 02 2025 at 03:31 UTC