Lean error while building

Stream: new members

[Rahul Saha]

Hey guys, I am trying to build a Lean4 project. Below I try to recreate a minimal example of the project. When I run lake build for the example below, I get the following error:

info: cloning https://github.com/leanprover-community/mathlib4.git to ./lake-packages/mathlib
error: ./lake-packages/mathlib/lakefile.lean:29:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig'
error: ./lake-packages/mathlib/lakefile.lean:52:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig'
error: ./lake-packages/mathlib/lakefile.lean: package configuration has errors

I have reasons to believe this is because I set the revision of mathlib4 to the latest commit. (see the bottom of the post for context)
Before calling lake build the project directory structure is as follows:

PackageName
    |_  PackageName
             |_ All.lean
             |_ theorems.lean
    |_ Package.lean
    |_ lake-manifest.lean
    |_ lakefile.lean
    |_ lean-toolchain

All.lean is an empty file. The lakefile.lean is as follows:

import Lake
open Lake DSL

package «packageName» {
  -- add any package configuration options here
}

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

@[default_target]
lean_lib «PackageName» {
  -- add any library configuration options here
}

My lake-manifest.json looks like this:

{"version": 4,
 "packagesDir": "lake-packages",
 "packages":
 [{"git":
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "subDir?": null,
    "rev": "c532d7b8b62ae053ce3d894ac69b52564e644696",
    "name": "mathlib",
    "inputRev?": null}},
  {"git":
   {"url": "https://github.com/gebner/quote4",
    "subDir?": null,
    "rev": "c71f94e34c1cda52eef5c93dc9da409ab2727420",
    "name": "Qq",
    "inputRev?": "master"}},
  {"git":
   {"url": "https://github.com/JLimperg/aesop",
    "subDir?": null,
    "rev": "cdc00b640d0179910ebaa9c931e3b733a04b881c",
    "name": "aesop",
    "inputRev?": "master"}},
  {"git":
   {"url": "https://github.com/leanprover/std4",
    "subDir?": null,
    "rev": "6006307d2ceb8743fea7e00ba0036af8654d0347",
    "name": "std",
    "inputRev?": "main"}}]}

Note: The revision for mathlib4 is set to the latest commit (perhaps this is where the error is?).

One thing of note is that if I replace the current commit version with the following commit hash: f52ba342fc94eccad393169be575cc94f22d6ca9, the package builds and works just fine, so that is where the issue is happening. The reason I am trying to build the latest version is because the previous one is from March and misses out on a lot of development that has happened since then.

Any advice on building this would be appreciated. Thanks!

ADDENDUM: If I try lake update on the commit that works, it gives the same error.

[Kevin Buzzard]

Try removing the lake-packages directory and then run lake exe cache get. There is no problem using the latest mathlib commit. If removing the directory doesn't work then just delete the repo and make a new one with lake new name-of-project math then lake exe cache get and don't touch any config files.

[Kevin Buzzard]

The correct way to update a project which depends on mathlib is explained in the mathlib readme IIRC (it involves a curl command)

[Rahul Saha]

Ah gotcha, the following worked for the update.

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

Thanks!

[Kevin Buzzard]

(I think the curl command is just copying mathlib's version of Lean and making it your project's version of Lean BTW)