Yet another "cannot build" topic

Stream: general

[Number Eighteen]

On a linux system, I run the following commands:

rm -rf .elan
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

I select nightly for the default toolchain and accept to modify PATH. According to instructions, I then run

source $HOME/.elan/env

Then I run

lake new test
cd test
lake build

All ok. Now I modify:

import Lake
open Lake DSL

package "test" where
  -- add package configuration options here

lean_lib «Test» where
  -- add library configuration options here

@[default_target]
lean_exe "test" where
  root := `Main

to

import Lake
open Lake DSL

package "test" where
  -- add package configuration options here

lean_lib «Test» where
  -- add library configuration options here
require alloy from git
  "https://github.com/tydeu/lean4-alloy.git"

@[default_target]
lean_exe "test" where
  root := `Main

I run

lake update
lake build

Completes normally. Now I modify lakefile.lean to

import Lake
open Lake DSL

package "test" where
  -- add package configuration options here

lean_lib «Test» where
  -- add library configuration options here
require alloy from git
  "https://github.com/tydeu/lean4-alloy.git"
require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

@[default_target]
lean_exe "test" where
  root := `Main

I get the "missing manifest" message when I try to build, so I follow the instructions and type

lake update mathlib

At this point, I get the error

error: ././lakefile.lean:4:7: error: unexpected token; expected identifier
error: ././lakefile.lean:16:8: error: unexpected token; expected identifier
error: ././lakefile.lean: package configuration has errors
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git to '././.lake/packages/mathlib'
info: batteries: cloning https://github.com/leanprover-community/batteries to '././.lake/packages/batteries'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets'
warning: ././.lake/packages/proofwidgets/lakefile.lean:22:20: warning: `Lake.inputFile` has been deprecated
warning: ././.lake/packages/proofwidgets/lakefile.lean:76:36: warning: `Lake.inputFile` has been deprecated
info: Cli: cloning https://github.com/leanprover/lean4-cli to '././.lake/packages/Cli'
info: importGraph: cloning https://github.com/leanprover-community/import-graph.git to '././.lake/packages/importGraph'
info: mathlib: running post-update hooks
error: mathlib: failed to fetch cache

and any further attempts to run lake with any command are rejected with

error: ././lakefile.lean:4:7: error: unexpected token; expected identifier
error: ././lakefile.lean:14:8: error: unexpected token; expected identifier
error: ././lakefile.lean: package configuration has errors

(I did not modify lakefile.lean at all)

I give up; help.

[Eric Wieser]

What does your lean-toolchain file contain?

[Number Eighteen]

It reads: leanprover/lean4:v4.9.0-rc2

[Number Eighteen]

By the way, I did not touch the lean-toolchain file, it was created by lake and never modified.

[Ruben Van de Velde]

What instructions did you find that tell you to run lake update mathlib?

[Number Eighteen]

After adding mathlib requirement to lakefile.lean, I run lake build. Then I get the message:

error: dependency 'mathlib' not in manifest; use `lake update mathlib` to add it

[Eric Wieser]

Number Eighteen said:

By the way, I did not touch the lean-toolchain file, it was created by lake and never modified.

What it contains depends on what version of lake you have installed, which can sometimes depend on when you installed elan for the first time

[Eric Wieser]

(your content sounds fine)

[Number Eighteen]

Eric, I have not "installed" any version of lake by hand. I installed elan according to the steps above and chose nightly for the default toolchain. Lake is a complete black box to me.

[Eric Wieser]

Can you also share the contents of your lake-manifest.json (which was created automatically by lake)?

[Eric Wieser]

And perhaps the output of lake --version for good measure (run from inside your project directory)

[Number Eighteen]

Lake version: Lake version 5.0.0-7ed9b73 (Lean version 4.9.0-rc2)

Contents of manifest:

{"version": "1.0.0",
 "packagesDir": ".lake/packages",
 "packages":
 [{"url": "https://github.com/tydeu/lean4-alloy.git",
   "type": "git",
   "subDir": null,
   "rev": "d93e0591e2b2ee76f13b8394d9b4c870af7489b6",
   "name": "alloy",
   "manifestFile": "lake-manifest.json",
   "inputRev": null,
   "inherited": false,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/batteries",
   "type": "git",
   "subDir": null,
   "rev": "47e4cc5c5800c07d9bf232173c9941fa5bf68589",
   "name": "batteries",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/quote4",
   "type": "git",
   "subDir": null,
   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
   "name": "Qq",
   "manifestFile": "lake-manifest.json",
   "inputRev": "master",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/aesop",
   "type": "git",
   "subDir": null,
   "rev": "882561b77bd2aaa98bd8665a56821062bdb3034c",
   "name": "aesop",
   "manifestFile": "lake-manifest.json",
   "inputRev": "master",
   "inherited": true,
   "configFile": "lakefile.toml"},
  {"url": "https://github.com/leanprover-community/ProofWidgets4",
   "type": "git",
   "subDir": null,
   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
   "name": "proofwidgets",
   "manifestFile": "lake-manifest.json",
   "inputRev": "v0.0.36",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover/lean4-cli",
   "type": "git",
   "subDir": null,
   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
   "name": "Cli",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/import-graph.git",
   "type": "git",
   "subDir": null,
   "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96",
   "name": "importGraph",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
   "inherited": true,
   "configFile": "lakefile.toml"},
  {"url": "https://github.com/leanprover-community/mathlib4.git",
   "type": "git",
   "subDir": null,
   "rev": "e19c07e6753d1d2844a1849a0077a6c9ad2d8676",
   "name": "mathlib",
   "manifestFile": "lake-manifest.json",
   "inputRev": null,
   "inherited": false,
   "configFile": "lakefile.lean"}],
 "name": "test",
 "lakeDir": ".lake"}

[Eric Wieser]

That all looks ok to me. Does lake clean work?

[Number Eighteen]

No, again all lake commands, including lake clean, fail with the same message:

error: ././lakefile.lean:4:7: error: unexpected token; expected identifier
error: ././lakefile.lean:15:8: error: unexpected token; expected identifier
error: ././lakefile.lean: package configuration has errors

[Eric Wieser]

Try rm -rf .lake then lake build again

[Eric Wieser]

Number Eighteen said:

... and chose nightly for the default toolchain. Lake is a complete black box to me.

I would guess this is the cause of the problem; you did a partial build with nightly, but lake update mathlib ended up downgrading the contents of your lean-toolchain file (which is what you want), and left the .lake folder in a corrupt state

[Number Eighteen]

I run

rm -rf .lake
lake build

I get

error: ././lakefile.lean:4:7: error: unexpected token; expected identifier
error: ././lakefile.lean:15:8: error: unexpected token; expected identifier
error: ././lakefile.lean: package configuration has errors

[Eric Wieser]

I think the lakefile.lean format changed between versions...

[Eric Wieser]

Though I'm not really sure what happened here

[Eric Wieser]

package "test" is not legal syntax, it should be package test

[Eric Wieser]

(same for lean_exe test)

[Number Eighteen]

OK, after modifying to remove the double quotes, lake build runs. Once it's done, I'll report back. But why did lake new use the old syntax to create the lake file, even though the toolchain is nightly?

[Eric Wieser]

Can you run lake new in a new folder, and report the value of lake --version in that folder?

[Eric Wieser]

(This time, without trying to add mathlib to the lakefile, which is what caused the version to switch)

[Ruben Van de Velde]

I think the opposite happened, it used new syntax and lake update mathlib reverted to an older version

[Number Eighteen]

The toolchain in the new folder is now nightly, as instructed by elan.

[Eric Wieser]

Maybe the short answer here is "choosing nightly was a mistake, pick stable instead"

[Eric Wieser]

Using mathlib would cause the version to change anyway, but the generated lakefile.lean would hopefully end up compatible that way

[Eric Wieser]

If you want a project that depends on mathlib, you should use lake new math yourproject

[Number Eighteen]

So I cannot manually add mathlib as a dependency afterwards to a project?

[Eric Wieser]

You can, but it may not go smoothly, as happened here

[Eric Wieser]

cc @Mac Malone, the fact that nightly lake new generates lakefiles incompatible with older versions of lean seems rather unfortunate here.

[Number Eighteen]

But math does not create an exe target, only a lib target; I want to create executables and have mathlib as a dependency.

[Eric Wieser]

You can add the exe target yourself later, but I guess you had no reason to expect that to be easier than adding require "mathlib" from ... manually instead

[Number Eighteen]

Also I just tried doing the math command, and the generated lakefile has the double quotes.

[Eric Wieser]

Let's see what Mac has to say here

[Number Eighteen]

Incredible; I am getting the same error in the new math directory!!

[Number Eighteen]

I write:

rm -rf foobar
lake new foobar math
cd foobar
lake build

error: ././lakefile.lean:4:7: error: unexpected token; expected identifier
error: ././lakefile.lean: package configuration has errors

[Eric Wieser]

Yes, this is because your global lake is the nightly / unstable version

[Number Eighteen]

Ha ha hahaaa.

[Eric Wieser]

This is still arguably a bug, but you did ask for the version most likely to contain bugs

[Number Eighteen]

But when I run lake --version in the folder, I get Lake version 5.0.0-7ed9b73 (Lean version 4.9.0-rc2)

[Number Eighteen]

Whereas in a folder without math, I get the global nightly which reads Lake version 5.0.0-src (Lean version 4.10.0-nightly-2024-06-22)

[Number Eighteen]

In any case, I will wipe .elan again and try everything again with stable.

[Eric Wieser]

What's happening is:

• you have nightly installed globally
• lake new math:
  • Creates a new lakefile.lean in the nightly format, and a lean-toolchain containing nightly
  • Runs lake update mathlib, which downgrades lean-toolchain to the stable release
• lake --version reads this lean-toolchain file to determine its version
• you're now in trouble because the lakefile.lean is now in a format that can't be read by the stable release

[Sebastian Ullrich]

Which is the reason why https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency has very specific instructions

[Eric Wieser]

Should lake new math error if invoked without a + argument?

[Number Eighteen]

@Sebastian Ullrich With those instructions, I end up in exactly the same state of the folder as the one that led me to the errors; in particular, the lean-toolchain you're instructing me to curl has leanprover/lean4:v4.9.0-rc2 which was what was there anyway.

[Sebastian Ullrich]

I did mean the instructions for a new project. Starting with an existing project that was created by nightly is not a good idea because the ecosystem never uses nightly

[Mac Malone]

Eric Wieser said:

cc Mac Malone, the fact that nightly lake new generates lakefiles incompatible with older versions of lean seems rather unfortunate here.

This is an inevitable consequence of new features. The unfortunate problem here is mathlib downgrading things. Hopefully the soon-to-be-addressed toolchain-aware lake update will fic this.