Lake version issue of imported package

Stream: lean4

[Floris van Doorn]

In the repository
https://github.com/fpvandoorn/LeanInRome
I'm requiring mathlib at a specific commit:

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

The hash in lake-manifest.json is exactly the same.

However, when running any lake command, I get the warning

warning: manifest out of date: git revision of dependency 'mathlib' changed; use `lake update mathlib` to update it

Furthermore, when updating, I just get an error:

Floris@Dell-E MINGW64 ~/projects/LeanInRome (master)
$ lake update
error: no error (error code: 0)

Floris@Dell-E MINGW64 ~/projects/LeanInRome (master)
$ lake update mathlib
error: no error (error code: 0)

What is wrong in my configuration? (@Mac Malone)

[Mac Malone]

@Floris van Doorn It sounds to me like Lake's checkout of mathlib was corrupted. For debugging purposes, you could try backing up the .lake fold (e.g., by renaming it) and then starting from fresh and seeing if you still have the same issue.

[Floris van Doorn]

I have the same issue with a fresh clone of the repo.

[Mac Malone]

Oh.

[Floris van Doorn]

oh, deleting lake-manifest.json fixed the issue.

[Floris van Doorn]

The new lake-manifest.json that was generated had the following diff:

-   "inputRev": "master",
+   "inputRev": "e659b1b3c9ad1535ef5f4ec13280a382fe457aee",

I indeed changed the commit from master to the specific sha in lakefile.lean. It would be nice if lake update can deal with this change.

[Mac Malone]

@Floris van Doorn lake update should deal with this (which is why Lake was asking you to run it). Why is was breaking is confusing me.

[Mac Malone]

Perhaps lake update -v would have provided more information. Tracing IO errors is hard, which is something I am now attempting to improve with more logging were I notice it, but sadly some of this stuff is deeply nested.

[Floris van Doorn]

Ok, I'll try lake update -v next time I see this (I tried to reproduce it again, but failed).

[Floris van Doorn]

I am experiencing this again. However, lake update -v doesn't print any more information:

Floris@Dell-E MINGW64 ~/projects/LeanCourse (master)
$ lake update -v
error: no error (error code: 0)

Both times I got this, the steps I took are roughly:

• Take a repository that worked fine, with mathlib a few months old
• Change the commit in lakefile.lean (but don't change anything else)
• Run lake update but get the following error:

$ lake update
error: .\lake-packages\mathlib\lakefile.lean:6:2: error: 'leanOptions' is not a field of structure 'Lake.PackageConfig'
error: .\lake-packages\mathlib\lakefile.lean: package configuration has errors
mathlib: updating repository '.\lake-packages\mathlib' to revision '5964134838f12fb0ea6fde72764f6d985c312842'

• Update lakefile.lean to the new option configuration
• copy lean-toolchain from the mathlib dependency (is this still a required step?)
• Run lake update again and get the no error error.

Presumably the first lake update is causing an issue here.