lean4 web editor version information

Stream: general

[Eric Wieser]

When I click the "version" button at https://lean.math.hhu.de/, I get "Last update: Invalid date" and no information; am I right in saying that it hasn't been updated in a while?

[Eric Wieser]

ping @Jon Eugster in case you're not already aware

[Jon Eugster]

Looks like it runs at mathlib commit 5f5c4e1 which is just 4 hours old, so I think it's only the version display that is broken rn.

[Jon Eugster]

Fixed. I believe lake update caused the script to fail on some core/std bumps but it always recovered automatically on the following build a few hours later. Thanks for spotting this

[Eric Wieser]

I think it was much older than that, because {α : Type*} syntax only just started working

[Jon Eugster]

Eric Wieser said:

I think it was much older than that, because {α : Type*} syntax only just started working

Hmm, interesting. In that case I need to dig through the logs.

[Jon Eugster]

lean4web: error: ./lake-packages/proofwidgets/lakefile.lean:28:27: error: function expected at
lean4web:   NPackage
lean4web: term has type
lean4web:   ?m.6347
lean4web: error: ./lake-packages/proofwidgets/lakefile.lean:64:29: error: function expected at
lean4web:   NPackage
lean4web: term has type
lean4web:   ?m.9379
lean4web: error: ./lake-packages/proofwidgets/lakefile.lean:77:26: error: unknown identifier 'NPackage'
lean4web: error: ./lake-packages/proofwidgets/lakefile.lean:80:29: error: unknown identifier 'NPackage'
lean4web: error: ./lake-packages/proofwidgets/lakefile.lean:84:18: error: unknown identifier 'NPackage'
lean4web: error: ./lake-packages/proofwidgets/lakefile.lean:88:10: error: invalid field notation, type is not of the form (C ...) where C is a constant
lean4web:   job₁
lean4web: has type
lean4web:   ?m.14602
lean4web: error: ./lake-packages/proofwidgets/lakefile.lean:89:13: error: invalid field notation, type is not of the form (C ...) where C is a constant
lean4web:   lib
lean4web: has type
lean4web:   ?m.14586 pkg x✝¹
lean4web: error: ./lake-packages/proofwidgets/lakefile.lean:90:10: error: invalid field notation, type is not of the form (C ...) where C is a constant
lean4web:   job₂
lean4web: has type
lean4web:   ?m.14687
lean4web: error: ./lake-packages/proofwidgets/lakefile.lean: package configuration has errors

Any idea what this means? Could this be related to a wrong toolchain? Until now I had

lake update
cp ./lake_packages/mathlib/lean-toolchain .

instead of

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake update

so this might potentially have been the source of the error.

[Sebastian Ullrich]

cp vs curl shouldn't really matter but the order of the two commands is important, yes

[Jon Eugster]

Yes, but you can't cp until you used lake update to download the new mathlib, can you?

[Sebastian Ullrich]

Hah right, so curl it is

[Sebastian Ullrich]

Originally the only reason I used curl there is because unlike cp it works on Windows as well

[Jon Eugster]

So does that mean the error message above has nothing to do with proofwidgets, but that's just the first package lake update sees?

[Sebastian Ullrich]

The first one it doesn't understand using the old toolchain at least, yes

[Scott Morrison]

(Not sure this affected you here, but note the change from lake_packages to lake-packages recently. Both appear above!)