Lake error codes

Stream: general

[Frederick Pu]

Where can I find the definitions for all of lake's error codes.

[Patrick Massot]

(deleted)

[Kim Morrison]

@Frederick Pu, can you give a example of what you mean? It's not clear to me what you're looking for.

[Frederick Pu]

The following occured when I was trying to setup the Lean 4 Game dev container.

Screenshot-2024-02-16-094459.png

[Kevin Buzzard]

Then I think a better question is to ask someone like @Jon Eugster what to do next, because what's actually going on is that lake is being actively maintained and changed right now, and there are lot of moving parts with the gameserver, so the issue is getting them all to be in the right place at the right time, and right now this can only be done with professional help :-)

[Shreyas Srinivas]

You are getting a manifest error. This can be remedied by deleting the lake-manifest.json file and also the ./.lake folder.

[Shreyas Srinivas]

Then run lake build

[Shreyas Srinivas]

you might want to run lake update before you run lake build. But this could create problems of incompatible versions.

[Frederick Pu]

Kevin Buzzard said:

Then I think a better question is to ask someone like Jon Eugster what to do next, because what's actually going on is that lake is being actively maintained and changed right now, and there are lot of moving parts with the gameserver, so the issue is getting them all to be in the right place at the right time, and right now this can only be done with professional help :-)

Yeah, I just talked to him and resolved the error.

[Jon Eugster]

Indeed, what @Shreyas Srinivas says. If in doubt,

rm -rf .lake
rm lake-manifest.json
lake update -R

is a good approach to deal with a bad state of lake. Opposed to projects like mathlib, I generally try to have any lakefile.lean always in a state such that lake update -R is a safe operation (i.e. have the versions of packages fixed in there). I'm not sure if lake clean would be a suitable command instead of lake update -R.

[Kim Morrison]

Improvements are in the pipeline here. We're aware there are three things going on, all of which are being addressed:

• The change to field name (leanOptions) wasn't sufficiently backwards compatible (i.e. the final error message should have given you something actionable)
• lake -R is currently required to override "sticky" state that probably shouldn't exist
• for simple projects, Turing complete configuration files are overkill

[Patrick Massot]

They are not only overkill, they also make it much harder to automatically fix issues like your first point.

[Patrick Massot]

And they also make it much harder to write lakefiles from other other tools such as my leanblueprint tool which helps setting up a blueprint. Here I simply want a python script to add a requirement to the lakefile. This would be trivial to do reliably to a toml or yaml or ini file.

[Patrick Massot]

And it was pretty ironic to work on packaging this python tool in this context. I don’t do python packaging often enough to remember it. So every time I need to read again all those webpage explaining why Python moved away from setup.py which is the equivalent of lakefile.lean and towards pyproject.toml which is a toml file.

[Shreyas Srinivas]

I don't see how removing Turing completeness solves your issue. This is a case of not having a suitably high level python API for dealing with a suitable subset of the lake DSL that suffices for simple projects

[Shreyas Srinivas]

It is easy to change toml files through python because you have this high level API.