help with lake new

Stream: lean4

[Sophie Morel]

I tried it myself (after updating elan to version 3.0.0), I got the following error message after entering lake +stable new SuperShinyProject:

error: toolchain 'stable' does not have the binary `/home/sophie/.elan/toolchains/stable/bin/lake`

[Sebastian Ullrich]

Use +leanprover/lean4:stable. The shortcut only works after updating elan.

[Sophie Morel]

Thanks, it works ! What confuses me is that I did update elan before trying ? (Maybe I didn't update it enough ? I have version 3.0.0 now.)

[Sophie Morel]

Sorry, it's me again, probably being very stupid again.
But, well, I created a new project using lake +leanprover/lean4:stablenew SuperShinyProject math, I and unlike what happens when I create a project using some version of nightly, it didn't create a lean-toolchain file in the project. In fact, the only things there are lakefile.lean and SuperShinyProject.lean.
Also, neither lake update nor lake exe cache get will run, they both give the same error message:

error: ./lakefile.lean:11:2: error: unknown attribute [defaultTarget]
error: ./lakefile.lean: package configuration has errors

Just a sanity check, did I need to reinstall Lean4 before I started using the new release ? Because I thought that updating elan would be enough, but apparently not.

[Sophie Morel]

Wait, I just created a lean-toolchain by hand, containing only leanprover/lean4:4.0.0, and now the next command lean --version is running. Fingers crossed.

[Sophie Morel]

(I got confused, because cat lean-toolchain just complained that lean-toolchain didn't exist, so I thought that the previous command should have created it. But maybe it shouldn't and I was supposed to create it myself all along.)

[Sophie Morel]

Hmrf. It did download lean, I got the message Lean (version 4.0.0, commit ec941735c80d, Release) and was happy. Then I tried playing with a Lean file and I get the error message

/home/sophie/.elan/toolchains/leanprover--lean4---4.0.0/bin/lake print-paths Init` failed:

stderr:
error: ./lakefile.lean:11:2: error: unknown attribute [defaultTarget]
error: ./lakefile.lean: package configuration has errors
Invalid Lake configuration.  Please restart the server after fixing the Lake configuration file.

again. I just edited lakefile.lean to comment the offending line 11 and I'm trying again, fingers crossed.

[Yaël Dillies]

(could we move discussion outside of #announce?)

[Scott Morrison]

@Sophie Morel, in what you've written above there is no space between +leanprover/lean4:stable and new, but there needs to be!

[Scott Morrison]

(I will move in a moment.)

[Scott Morrison]

Unfortunately I can't reproduce your problem at the moment. For me,

lake +leanprover/lean4:stable new SuperShinyProject math

creates a new directory SuperShinyProject containing a lean-toolchain (with contents leanprover/lean4:v4.0.0).

[Scott Morrison]

So I think we should go back a step and work out why that is not working for you (before editing too many files at random! :-)

[Notification Bot]

13 messages were moved here from #announce > First official release by Scott Morrison.

[Sophie Morel]

Scott Morrison said:

Sophie Morel, in what you've written above there is no space between +leanprover/lean4:stable and new, but there needs to be!

Sorry, that was a copying mistake, I definitely had the space in my terminal.

[Sophie Morel]

Scott Morrison said:

So I think we should go back a step and work out why that is not working for you (before editing too many files at random! :-)

Sure. First thing, elan: elan -V replies elan 3.0.0 (cdb40bff5 2023-09-08). Is this good or should I update something ?

[Sophie Morel]

(I also vote to rename the thread "Sophie is an idiot who can't create a Lean project to save her life"...)

[Sebastien Gouezel]

Just to comfort Sophie. I updated elan to the last version (the same as your elan 3.0.0, then did

lake +leanprover/lean4:stable new SuperShinyProject math

This created a superShinyProject subdirectory. It has a lean-toolchain file in it. However, when I open the folder superShinyProject in vscode, and then the file superShinyProject.lean in it, I get the following error message:

`c:\Users\Sebastien\.elan\toolchains\leanprover--lean4---v4.0.0\bin\lake.exe print-paths Init` failed:

stderr:
error: .\lakefile.lean:1:0: error: object file 'c:\Users\Sebastien\.elan\toolchains\leanprover--lean4---v4.0.0\lib\lean\Lake.olean' of module Lake does not exist
error: .\lakefile.lean:2:5: error: unknown namespace 'Lake'
error: .\lakefile.lean:4:0: error: expected command
error: .\lakefile.lean:12:0: error: expected 'abbrev', 'axiom', 'builtin_initialize', 'class', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'structure', 'syntax' or 'theorem'
error: .\lakefile.lean: package configuration has errors
Invalid Lake configuration.  Please restart the server after fixing the Lake configuration file.

[Sophie Morel]

(Also also, my method of editing files at random seems to have worked, I now have a Lean project where lake build runs. And more importantly to me, I can work on Lean files in it.)

[Sebastien Gouezel]

And if I do lake build in the directory project, I get

error: .\lakefile.lean:1:0: error: object file 'c:\Users\Sebastien\.elan\toolchains\leanprover--lean4---v4.0.0\lib\lean\Lake.olean' of module Lake does not exist
error: .\lakefile.lean:2:5: error: unknown namespace 'Lake'
error: .\lakefile.lean:4:0: error: expected command
error: .\lakefile.lean:12:0: error: expected 'abbrev', 'axiom', 'builtin_initialize', 'class', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'structure', 'syntax' or 'theorem'
error: .\lakefile.lean: package configuration has errors

(I'm glad I'm always working directly on mathlib)

[Sebastien Gouezel]

The content of lakefile.lean is

import Lake
open Lake DSL

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

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

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

[Sophie Morel]

Well if I run lake +leanprover/lean4:stable new SuperShinyProject math (with a project name that is not already used), I still don't get a lean-toolchain. My lakefile.lean says:

import Lake
open Lake DSL

package superShinyProject {
  -- add any package configuration options here
}

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

@[defaultTarget]
lean_lib SuperShinyProject {
  -- add any library configuration options here
}

[Sophie Morel]

What, why do I have @[defaultTarget] and not @[default_target] like Sébastien ? I edited lakefile.lean to change that, and now lake update will run. (I also had to create lean-toolchain by hand first. This is black magic.)

[Sebastien Gouezel]

Sebastien Gouezel said:

And if I do lake build in the directory project, I get

error: .\lakefile.lean:1:0: error: object file 'c:\Users\Sebastien\.elan\toolchains\leanprover--lean4---v4.0.0\lib\lean\Lake.olean' of module Lake does not exist

(I'm glad I'm always working directly on mathlib)

And indeed, this file does not exist. In the directory C:\Users\Sebastien\.elan\toolchains\leanprover--lean4---v4.0.0\lib\lean, there are files Init.ilean, Init.olean and subdirectories Init and Lake, both of them populated with many ilean and olean files.

[Sebastian Ullrich]

@Sophie Morel Oh, this is an elan gotcha I forgot about but that I want to address soon: if you've already installed a previous stable version of Lean, you first have to run elan update stable. Or use +leanprover/lean4:4.0.0 directly.

[Sebastian Ullrich]

@Sebastien Gouezel The file does exist in https://github.com/leanprover/lean4/releases/download/v4.0.0/lean-4.0.0-windows.tar.zst. Could you run elan toolchain uninstall leanprover/lean4:v4.0.0 and try again?

[Sebastien Gouezel]

I have uninstalled all my previous toolchains, started again, and it works fine. Probably something had already been downloaded by an old version of elan and was conflicting with something else, but since I have wiped everything away I won't be able to help you diagnose it. In any case, this shouldn't affect newcomers.

[Sebastian Ullrich]

That's good to hear. As it was in the right directory, my best guess would be a corrupted elan download. (Un)fortunately that seems like a extremely rare occurrence so I wouldn't even know where to start looking.

[Sophie Morel]

I am waiting for elan update stable to finish running and then I'll try again.

[Sophie Morel]

I got the message stable updated - Lean (version 4.0.0, commit ec941735c80d, Release) from elan (and no error message).

Then I ran lake +leanprover/lean4:stable new ShinyProject math. Still no lean-toolchain, and I get the same error messages as before when I try to run lake update or lake exe cache get:

error: ./lakefile.lean:11:2: error: unknown attribute [defaultTarget]
error: ./lakefile.lean: package configuration has errors

I think that I should burn my computer, exorcise the ashes and start with a new machine.

[Sebastian Ullrich]

Ah, this only works if you literally use +stable as in the beginning. I'm removing the code responsible for this confusion as we speak.

[Sophie Morel]

Ah yes, I tried with lake +stable and I got a toolchain.

[Sophie Morel]

I am on my way to the nearest church to light a votive candle. Thanks for the help !

[Sebastian Ullrich]

I really should fix this then so we can spend less on candles!

[Filippo A. E. Nuccio]

I am creating a new project and after some trial-and-error I detect the following behaviour:

• If I duly follow the instructions here line-by-line everything goes smoothly.
• If I bravely modify the sugested names my_project and MyProject to Expose and Expose, everything is OK again.
• But if I too bravely modify my_project and MyProject to foo and bar, my imports are not recognized (the mathlib ones are OK).

Is this expected?

[Scott Morrison]

No, this is not expected. Could you check if it's still the case if you use lake +x where x is the latest nightly?

[Scott Morrison]

@Filippo A. E. Nuccio, oh, maybe my mistake --- when you say that you put your files in bar/, are you changing the lean_lib line in your lakefile from lean_lib «Foo» { to lean_lib «bar» {? If you don't do that then just putting Lean files in bar/ will not allow you to import other files from bar/.

[Scott Morrison]

There does seem to be a lake issue hiding here, however.

[Scott Morrison]

With lean_lib «bar» (note lower-case), and files in bar/A.lean and bar/B.lean, then lake build bar.B fails with `error: unknown target bar.B`` but lake build Bar.B` succeeds.

Importing either bar.B or Bar.B works. (This is all on macos, which has the nasty feature of case-sensitive filenames that you can refer to with the wrong cases...)

[Scott Morrison]

@Mac Malone, what can we do about this? What should the behaviour be?

[Mario Carneiro]

does it work with +?

[Mario Carneiro]

lake build +bar.B

[Scott Morrison]

A different error:

% lake build +bar.A
error: unknown module `bar.A`

[Mario Carneiro]

what's the project setup?

[Scott Morrison]

lakefile.lean:

import Lake
open Lake DSL

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

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

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

[Scott Morrison]

and a file bar/A.lean.

[Mario Carneiro]

I assume the mathlib dependency is unnecessary

[Mario Carneiro]

Is there a bar.lean?

[Scott Morrison]

Behaviour is the same before and after renaming /Foo.lean to /bar.lean.

[Mario Carneiro]

the default configuration includes only bar.lean and its transitive dependencies in the lib

[Mario Carneiro]

what is the contents of bar.lean?

[Scott Morrison]

But I should still be able to build the non-transitively imported files, without munging the case!

[Scott Morrison]

def hello := "world"

[Mario Carneiro]

it has no deps?

[Scott Morrison]

Nothing

[Mario Carneiro]

in that case bar.A is not a target in the project

[Scott Morrison]

I'm not expecting lake build to build bar/A.lean. But shouldn't I be able to build it still?

[Mario Carneiro]

no

[Mario Carneiro]

this is an open feature request

[Mario Carneiro]

lake#147

[Mario Carneiro]

right now the only way to build orphan files is lake env lean bar/A.lean

[Mario Carneiro]

which is how we normally build test files

[Scott Morrison]

Oops, okay, sorry for the noise.

[Scott Morrison]

Ah, there is still a problem.

[Scott Morrison]

Starting fresh, I now have:
lakefile.lean

import Lake
open Lake DSL

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

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

[Scott Morrison]

and files bar/A.lean (empty) and bar/B.lean (just contains import bar.A).

[Scott Morrison]

and bar.lean containing

import bar.A
import bar.B

def hello := "world"

[Scott Morrison]

That seems valid, no? Or at least something a user might reasonably do. :-)

[Mario Carneiro]

yes that looks valid

[Scott Morrison]

% lake build
[0/1] Building Bar
error: > LEAN_PATH=./build/lib DYLD_LIBRARY_PATH=./build/lib /Users/kim/.elan/toolchains/leanprover--lean4---v4.1.0-rc1/bin/lean ./././Bar.lean -R ././. -o ./build/lib/Bar.olean -i ./build/lib/Bar.ilean -c ./build/ir/Bar.c
error: stdout:
./././Bar.lean:1:0: error: unknown package 'bar'
You might need to open '/Users/kim/scratch/foo' as a workspace in your editor
./././Bar.lean:4:13: error: unknown constant 'String'
error: external command `/Users/kim/.elan/toolchains/leanprover--lean4---v4.1.0-rc1/bin/lean` exited with code 1

[Scott Morrison]

Similarly opening either bar.lean or bar/B.lean gives the error:

unknown package 'bar'
You might need to open '/Users/kim/scratch/foo' as a workspace in your editor

[Mario Carneiro]

what is the toolchain version?

[Scott Morrison]

v4.1.0-rc1, just checking now with latest nightly

[Scott Morrison]

Same behaviour on nightly-2023-09-19.

[Mario Carneiro]

Ah, the default roots for a lean_lib is #[toUpperCamelCase name]

[Mario Carneiro]

meaning that even if you call it bar lake will be looking for Bar.lean and Bar/A.lean

[Scott Morrison]

Okay, I think I this point we can ping @Mac Malone and leave it with them.

[Scott Morrison]

Options:

1. We insist that the names of lean_libs start with a capital --- and error if not.
2. We make things work with lower-case lean_libs.

I don't particularly mind which (as long as option 1. actually errors).

[Mario Carneiro]

oh, apparently there is also libName which is also defaulted to toUpperCamelCase name, so I guess a library can have three "names" for resolution purposes

[Mario Carneiro]

my 2c: remove the toUpperCamelCase from these defaults. We can have a default convention of using upper camel case for lib names, but we shouldn't do any extra re-casing if the user puts a lowercase lib name anyway

[Kevin Buzzard]

Wait did someone say earlier that if lake build doesn't build it, it can't be built? Then I don't know how to make a lean project. After following the instructions aren't you left with a file called name_of_project.lean containing some random hello world thing? I usually just ignore this file (because it's code so I don't understand it) and the Lakefile (because I don't understand it either) and just start developing in the directory which has got the same level as the project name. IIRC everything works. Am I misrembering?

[Mario Carneiro]

It works, but only as much as any single file project works

[Mario Carneiro]

those files are not officially a part of any library and will not be built by lake build

[Mario Carneiro]

The recommendation is to replace the hello world file with your own code, not ignore it

[Kevin Buzzard]

And this has to be one of those stupid files which imports all the files in your project and which never used to exist? This is a compulsory file in any lean 4 project despite the fact that it could be made programatically? Is this mentioned in any documentation?

[Mario Carneiro]

You can make a project without the stupid import everything file, but you have to modify your lakefile to do it

[Kevin Buzzard]

But it's ok to delete the hello world bit?

[Mario Carneiro]

yes of course

[Kevin Buzzard]

I have no understanding of these files, I don't know what's ok any more

[Kevin Buzzard]

I thought what I was doing (ignoring everything) was ok

[Mario Carneiro]

well it's fine as long as everything works for you

[Kevin Buzzard]

There's some main mentioned, I have no idea what that is but it sounds like the kind of thing you shouldn't be deleting

[Mario Carneiro]

that's because the default project is a binary, while math projects probably want a lib

[Kevin Buzzard]

I just prove theorems, I've never had to deal with main, I don't know what the difference is between a module, a library and any of these other CS code words

[Mario Carneiro]

a library (lean_lib) is something that compiles to make oleans

[Mario Carneiro]

an executable (lean_exe) is something that goes through compilation into a program you can run

[Mario Carneiro]

math projects basically never need the latter

[Mario Carneiro]

when you use lake new foo math it will automatically set up a library for you

[Kevin Buzzard]

But it still makes a hello world file IIRC

[Mario Carneiro]

not one with a def main though

[Mario Carneiro]

just def hello := "world"

[Mario Carneiro]

testing it now, it actually doesn't create the folder, just a single file containing the hello world

[Kevin Buzzard]

Can it instead make a file saying

-- change this file to a file which imports all your theorems
-- eg
-- import Foo.basic
-- import Foo.main_theorem
-- and put your theorems in the `Foo` directory

if you called your project Foo?

[Mario Carneiro]

well the point of a template is to show you that

[Kevin Buzzard]

I see.

[Mario Carneiro]

so it should just do that with some foobar theorems

[Mario Carneiro]

Here's a sample "look ma, no import all file" project:

lakefile.lean:

import Lake
open Lake DSL

package «my-project»

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

@[default_target]
lean_lib MyProject where
  globs := #[.submodules `MyProject]

MyProject/A.lean:

def foo := 1

MyProject/B.lean:

import MyProject.A
def bar := 1

lake build will build everything in MyProject, and files can import each other as demonstrated. There is no MyProject.lean file in the project.

[Scott Morrison]

As of v4.1.0-rc1, this template is automatically created:

lake +v4.1.0-rc1 new my_project math

creates a my_project/MyProject.lean and a my_project/MyProject/Basic.lean.

Further, my_project/MyProject.lean contains:

-- This module serves as the root of the `MyProject` library.
-- Import modules here that should be built as part of the library.
import «MyProject».Basic

[Scott Morrison]

I think this is pretty much the behaviour we want, no?

[Scott Morrison]

(Maybe a minor improvement would be to have some logic that omits the « and » when they are unneeded.)

[Filippo A. E. Nuccio]

Oh, great to wake up and realise it was not just stupid me. Thanks!

Perhaps we can update the page mentioning lake +v4.1.0-rcl (and possibly some hints for newcomers about the evolution of the cabbalistic 4.1.0-rcl) instead of lean4:nightly-2023-02-04?

[Sebastian Ullrich]

https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#in-a-new-project has the correct instructions. This duplication is unfortunate.

[Scott Morrison]

@Filippo A. E. Nuccio, note that is it rc1 (i.e. release candidate one) rather than rcl.

[Scott Morrison]

In the link Sebastian has just provided there is the much better suggestion to use

lake +leanprover-community/mathlib4:lean-toolchain

rather than lake +x for any "fixed" x. This incantation says: please use whatever toolchain Mathlib is currently using!

[Scott Morrison]

I hope that in the near future there will just be no need to specify any +x incantations.

[Scott Morrison]

In fact I made a PR earlier today suggesting removing this from the leanprover-community instructions:

https://github.com/leanprover-community/leanprover-community.github.io/pull/365

[Scott Morrison]

I think the two reasonable alternatives here are:

• have the instructions everywhere advise using lake +leanprover-community/mathlib4:lean-toolchain, and then transition (hopefully as soon as the release of v4.1.0) to just advising using lake.
• have the instructions already just advise using lake

[Sebastian Ullrich]

Isn't that still problematic when mathlib is currently on an RC? Well, it will probably work, just download first a stable and then an RC Lean

[Sebastian Ullrich]

And it will reliably do that only when people have upgraded to the unmerged elan PR as well as set their default toolchain correctly

[Filippo A. E. Nuccio]

Sebastian Ullrich said:

https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#in-a-new-project has the correct instructions. This duplication is unfortunate.

Well, I would say that is more than unfortunate. Especially because it is the first where one lands from the entry page, clicking on "Working on Lean Projects".

[Kevin Buzzard]

Mario Carneiro said:

no

I am confused about this claim that lake build will only work for files which are "targets in the project". This works fine:

buzzard@buster:~/lean-projects$ lake new Foo math
info: Downloading lean-toolchain
buzzard@buster:~/lean-projects$ cd Foo
buzzard@buster:~/lean-projects/Foo$ ls
Foo.lean  lakefile.lean  lean-toolchain
buzzard@buster:~/lean-projects/Foo$ mkdir Foo
buzzard@buster:~/lean-projects/Foo$ cd Foo
buzzard@buster:~/lean-projects/Foo/Foo$ cat > Defs.lean
import Mathlib
def a : Nat := 37
buzzard@buster:~/lean-projects/Foo/Foo$ cat > Theorems.lean
import Foo.Defs

example : a = 37 := rfl
buzzard@buster:~/lean-projects/Foo/Foo$ cd ..
buzzard@buster:~/lean-projects/Foo$ lake build Foo.Theorems
error: missing manifest; use `lake update` to generate one
buzzard@buster:~/lean-projects/Foo$ lake update
cloning https://github.com/leanprover-community/mathlib4.git to ./lake-packages/mathlib
cloning https://github.com/mhuisi/lean4-cli.git to ./lake-packages/Cli
cloning https://github.com/gebner/quote4 to ./lake-packages/Qq
cloning https://github.com/JLimperg/aesop to ./lake-packages/aesop
cloning https://github.com/leanprover/std4 to ./lake-packages/std
cloning https://github.com/EdAyers/ProofWidgets4 to ./lake-packages/proofwidgets
buzzard@buster:~/lean-projects/Foo$ lake exe cache get
info: [0/9] Fetching proofwidgets cloud release
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [5/9] Compiling Cache.Requests
info: [5/9] Building Cache.Main
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache
Attempting to download 3777 file(s)
Downloaded: 3777 file(s) [attempted 3777/3777 = 100%] (100% success)
Decompressing 3777 file(s)
unpacked in 5923 ms
buzzard@buster:~/lean-projects/Foo$ lake build
[1/2] Building Foo
buzzard@buster:~/lean-projects/Foo$ lake build Foo.Theorems
[3775/3777] Building Foo.Defs
[3776/3777] Building Foo.Theorems
buzzard@buster:~/lean-projects/Foo$

[Mac Malone]

@Kevin Buzzard For a default math project named Foo, anything under the Foo directory is part of the library Foo. The problem is that, without @Mario Carneiro globs code, lake build will not build those files (lake build Foo.<module-name> will though.

[Scott Morrison]

I've just made an issue to track the camel-casing issue discussed above, to make sure we don't forget it. https://github.com/leanprover/lean4/issues/2567