error: permission denied

Stream: lean4

[Martin Dvořák]

I have just created a few new project:

lake new usporadani math

Unfortunately lake build gives me:

lake build
info: mathlib: no manifest entry; deleting .\lean_packages\mathlib and cloning again
error: permission denied (error code: 13)
  file: .\lean_packages\mathlib\.git\objects\pack\pack-27b45fcfa7b0644c1a2182536e1df0193c2b3f86.idx

Lean 4 used to work on my computer before I did elan update right before creating the new project.

[Mario Carneiro]

you have an old lake, as indicated by the use of lean_packages dir

[Shreyas Srinivas]

Martin Dvořák said:

I have just created a few new project:

lake new usporadani math

Unfortunately lake build gives me:

lake build
info: mathlib: no manifest entry; deleting .\lean_packages\mathlib and cloning again
error: permission denied (error code: 13)
  file: .\lean_packages\mathlib\.git\objects\pack\pack-27b45fcfa7b0644c1a2182536e1df0193c2b3f86.idx

Lean 4 used to work on my computer before I did elan update right before creating the new project.

Did you change your default toolchain after running elan update?

[Shreyas Srinivas]

Sometimes if you have chosen a specific toolchain as your default, elan doesn't change the setting after downloading the latest nightly

[Martin Dvořák]

Shreyas Srinivas said:

Did you change your default toolchain after running elan update?

No.

Is there a command I should run after every elan update?

[Shreyas Srinivas]

what's the output of elan toolchain list?

[Martin Dvořák]

Shreyas Srinivas said:

what's the output of elan toolchain list?

stable
leanprover-community/lean:3.41.0
leanprover-community/lean:3.42.1
leanprover-community/lean:3.48.0
leanprover-community/lean:3.49.0
leanprover-community/lean:3.49.1
leanprover-community/lean:3.50.3
leanprover/lean4:nightly
leanprover/lean4:nightly-2023-02-01
leanprover/lean4:nightly-2023-02-24 (default)
leanprover/lean4:nightly-2023-03-07
leanprover/lean4:nightly-2023-03-09
leanprover/lean4:stable

[Shreyas Srinivas]

Yes so your default toolchain is pinned to the nightly from 24th Feb.

[Shreyas Srinivas]

Try elan default leanprover/lean4:nightly. Then every time you run elan update you will be using the latest nightly.

[Shreyas Srinivas]

If instead you choose a specific nightly ( for a given date leanprover/lean4:nightly-yyyy-mm-dd) then elan will merely download the latest nightly and let you continue using that specific nightly.

[Shreyas Srinivas]

The latter case is similar to opam pin for coq and ocaml

[Martin Dvořák]

I did:

elan default leanprover/lean4:nightly

As a result elan toolchain list now gives me:

stable
leanprover-community/lean:3.41.0
leanprover-community/lean:3.42.1
leanprover-community/lean:3.48.0
leanprover-community/lean:3.49.0
leanprover-community/lean:3.49.1
leanprover-community/lean:3.50.3
leanprover/lean4:nightly (default)
leanprover/lean4:nightly-2023-02-01
leanprover/lean4:nightly-2023-02-24
leanprover/lean4:nightly-2023-03-07
leanprover/lean4:nightly-2023-03-09
leanprover/lean4:stable

Nevertheless, when I create another new project, it does not build.

[Shreyas Srinivas]

The next step is to run chmod -R 755 <your project dir>

[Shreyas Srinivas]

It could very well be some weird directory permissions issue

[Martin Dvořák]

$ lake new order-theory math
$ cd order-theory/
$ ls
OrderTheory.lean  lakefile.lean
$ lake build
info: cloning https://github.com/leanprover-community/mathlib4.git to .\lean_packages\mathlib
error: .\lean_packages\mathlib\lakefile.lean:17:2: error: unknown attribute [default_target]
error: .\lean_packages\mathlib\lakefile.lean:21:2: error: unknown attribute [default_target]
error: .\lean_packages\mathlib\lakefile.lean: package configuration has errors
$ chmod -R 755 .
$ lake build
info: mathlib: no manifest entry; deleting .\lean_packages\mathlib and cloning again
info: cloning https://github.com/leanprover-community/mathlib4.git to .\lean_packages\mathlib
error: .\lean_packages\mathlib\lakefile.lean:17:2: error: unknown attribute [default_target]
error: .\lean_packages\mathlib\lakefile.lean:21:2: error: unknown attribute [default_target]
error: .\lean_packages\mathlib\lakefile.lean: package configuration has errors

[Shreyas Srinivas]

Did you run lake update after entering your project dir?

[Martin Dvořák]

No.

[Martin Dvořák]

$ lake update
error: permission denied (error code: 13)
  file: .\lean_packages\mathlib\.git\objects\pack\pack-33d2cc8135268a1430f2d9e86fcdefdcf196481c.idx
mathlib: no manifest entry; deleting .\lean_packages\mathlib and cloning again

[Shreyas Srinivas]

are you inside a folder which contains a lakefile.lean (EDIT: lean-toolchain) when you create your project?

[Martin Dvořák]

$ ls
OrderTheory.lean  lakefile.lean  lean_packages/

[Shreyas Srinivas]

Try ls ..

[Shreyas Srinivas]

one reason you might be accidentally using an old toolchain is that there is an old lean-toolchain file in the directory from which you are calling lake new...

[Shreyas Srinivas]

I have a guess you are using an even older toolchain than the feb 24th nightly because of this.

[Mario Carneiro]

you can use lake +leanprover/lean4:nightly new ... to run a particular version of lake

[Sebastian Ullrich]

What Mario said, please follow the official instructions: https://github.com/leanprover-community/mathlib4#in-a-new-project

[Martin Dvořák]

Should I use nightly-2023-02-04 specifically?

[Sebastian Ullrich]

Yes

[Shreyas Srinivas]

Wait why?

[Shreyas Srinivas]

I have been gladly using later versions as well and they have worked perfectly fine

[Mario Carneiro]

I suppose it's fine as long as we update that line of the readme whenever lake changes the lakefile format

[Mario Carneiro]

this happens rarely, anything since feb should be fine

[Sebastian Ullrich]

If it works fine that's good, it's only when things break and you want help here that you should follow the instructions as written :)

[Shreyas Srinivas]

I see that the instructions have changed. I wrote a big chunk of the previous version of the instructions. There the only requirement was a version later than Feb 04 nightly

[Sebastian Ullrich]

@Mario Carneiro Do we need to update the expected cache get output in the instructions? I haven't followed the recent cache changes closely

[Martin Dvořák]

Martin Dvořák said:

Should I use nightly-2023-02-04 specifically?

Will I have a four-month-old version of mathlib4 as a result?

[Mario Carneiro]

no

[Mario Carneiro]

this is just the version of lake used to set up the project, once you enter the directory you will be using the version of lean/lake used by mathlib master

[Patrick Massot]

It is a bit of a shame that this process always involves getting two copies of Lean 4, knowing how huge is Lean 4.

[Shreyas Srinivas]

About the cache, since it came up. Recently I have been getting a weird warning that I have ignored so far (only on mac, not linux). I have safely ignored them since they don't cause trouble anywhere else:

ld64.lld: warning: directory not found for option -L/Applications/Xcode_14.2.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX13.1.sdk/usr/lib
ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 13.4.0, which is newer than target minimum of 13.0.0
ld64.lld: warning: /usr/lib/system/libsystem_platform.dylib has version 13.4.0, which is newer than target minimum of 13.0.0
ld64.lld: warning: /usr/lib/system/libsystem_pthread.dylib has version 13.4.0, which is newer than target minimum of 13.0.0

why is cache complaining about newer versions of libraries than a target "minimum"?

[Sebastian Ullrich]

Mario Carneiro said:

this is just the version of lake used to set up the project, once you enter the directory you will be using the version of lean/lake used by mathlib master

I guess we should clarify that in the text

[Martin Dvořák]

Sebastian Ullrich said:

If it works fine that's good, it's only when things break and you want help here that you should follow the instructions as written :)

I followed the instructions. Now both lake build and lake update give me the same error:

error: .\lakefile.lean:11:2: error: unknown attribute [default_target]
error: .\lakefile.lean: package configuration has errors

[Mario Carneiro]

@Patrick Massot agreed, this lake new foo math could very well be done by elan itself

[Patrick Massot]

Yes, this is what I meant.

[Mario Carneiro]

@Sebastian Ullrich a recent run of cache looks something like this:

$ lake exe cache get
info: [1/9] Building Cache.IO
info: [3/9] Building Cache.Hashing
info: [5/9] Building Cache.Requests
Attempting to download 3053 file(s)
Downloaded: 3053 file(s) [attempted 3053/3053 = 100%] (100% success)
Decompressing 3053 file(s)

[Shreyas Srinivas]

@Martin : This is almost certainly a case of a lean-toolchain file inside the directory from which you are calling lake new

[Sebastian Ullrich]

@Martin Dvořák What is the output of elan show in that directory?

[Martin Dvořák]

In the directory of the new project:

$ elan show
installed toolchains
--------------------

stable
leanprover-community/lean:3.41.0
leanprover-community/lean:3.42.1
leanprover-community/lean:3.48.0
leanprover-community/lean:3.49.0
leanprover-community/lean:3.49.1
leanprover-community/lean:3.50.3
leanprover/lean4:nightly (default)
leanprover/lean4:nightly-2023-02-01
leanprover/lean4:nightly-2023-02-04
leanprover/lean4:nightly-2023-02-24
leanprover/lean4:nightly-2023-03-07
leanprover/lean4:nightly-2023-03-09
leanprover/lean4:stable

active toolchain
----------------

leanprover/lean4:stable (directory override for '\\?\C:\Martin\IST\_Lean\lean4try')
Lean (version 4.0.0, commit 7dbfaf9b7519, Release)

[Martin Dvořák]

Shreyas Srinivas said:

@Martin : This is almost certainly a case of a lean-toolchain file inside the directory from which you are calling lake new

This time I checked and so such file is in the directory where I was when lake new was called.

[Sebastian Ullrich]

You used elan override. Don't do that. Remove it with elan override unset <path to lean4try>.

[Martin Dvořák]

Which command did elan override? I didn't write that concrete thing.

[Sebastian Ullrich]

No command I know of uses it

[Shreyas Srinivas]

It is found here: https://leanprover.github.io/lean4/doc/setup.html

[Shreyas Srinivas]

under basic setup

[Sebastian Ullrich]

Let's remove that real quick

[Martin Dvořák]

Sebastian Ullrich said:

You used elan override. Don't do that. Remove it with elan override unset <path to lean4try>.

I am on Windows 10 in Git Bash.

dvora@DESKTOP-1V7A9NM MINGW64 /c/Martin/IST/_Lean/lean4try
$ elan override unset /c/Martin/IST/_Lean/lean4try
error: Found argument 'C:/Martin/IST/_Lean/lean4try' which wasn't expected, or isn't valid in this context

[Martin Dvořák]

Relative path attempt:

dvora@DESKTOP-1V7A9NM MINGW64 /c/Martin/IST/_Lean/lean4try
$ elan override unset .
error: Found argument '.' which wasn't expected, or isn't valid in this context

[Sebastian Ullrich]

My bad, go in that directory if you're not there already and use elan override unset without parameter

[Martin Dvořák]

Sebastian Ullrich said:

No command I know of uses it

Maybe I did that command in the past in order to have Lean 4 in this directory and Lean 3 elsewhere.

[Martin Dvořák]

Sebastian Ullrich said:

My bad, go in that directory if you're not there already and use elan override unset without parameter

$ elan override unset
info: override toolchain for 'C:\Martin\IST\_Lean\lean4try' removed

[Martin Dvořák]

Which if the previous instruction now apply?

[Sebastian Ullrich]

Possibly lake build just works now. Though you really want to run lake exe cache get first.

[Shreyas Srinivas]

It is possible that people end up following the setup instructions and get stuck. That should probably change.

[Mac Malone]

Mario Carneiro said:

Patrick Massot agreed, this lake new foo math could very well be done by elan itself

We could potentially add a leanprover/lean4:mathlib toolchain ala nightly that corresponds to whatever the current lean-toolchain in mathlib master is.

[Shreyas Srinivas]

Mario Carneiro said:

no, just using elan for lake new

Isn't it a bit confusing for users. Currently, elan manages installations and lake manages aspects of an individual project. Are you suggesting merging elan and lake?

[Mario Carneiro]

no, just using elan for lake new

[Kevin Buzzard]

I'm not sure I ever use elan (working either with Lean 3 or Lean 4) and it seems to be a constant source of gotchas.

[Mario Carneiro]

you actually use elan all the time, you just don't realize it

[Mario Carneiro]

elan is way better and more stable than every other lean project we have

[Mario Carneiro]

when you call lean, that's actually elan. lake? elan again

[Mac Malone]

To avoid porting features, the elan init ... could just add a toolchain file and then run lake init ... (and the elan new would create the directory and then do the same).

[Shreyas Srinivas]

Then it is definitely confusing. Why is the toolchain manager managing one aspect of individual projects (namely creating them)

[Mac Malone]

Because the first thing you need to do in a project is select a toolchain before using any of the tools?

[Mario Carneiro]

lake new could just be dispatched to elan to handle, users don't really have to care where the functionality is implemented

[Mac Malone]

Mario Carneiro That creates the same problem though as it is not backwards compatible (i.e., if something in the process changes old lakes will break the call).

[Shreyas Srinivas]

Mac said:

Because the first thing you need to do in a project is select a toolchain before using any of the tools?

This was in response to Mario's suggestion. package managers and toolchain managers are doing two different things. To me it looks like a simpler solution exists: adding an interactive option in lake new and lake init to confirm the toolchain to use before creating a project. Cabal does this for haskell versions (98 or 2010)

[Mac Malone]

But lake itself is on the toolchain so if the problem is a change in lake, then the old lake cannot fix it.

[Mario Carneiro]

Mac said:

Mario Carneiro That creates the same problem though as it is not backwards compatible (i.e., if something in the process changes old lakes will break the call).

not if lake new just calls elan new and hands off all the arguments - this is not likely to change any time soon

[Mario Carneiro]

of course we will still have to deal with lakes from before we started doing this but once we get past that point it should be stable

[Mac Malone]

@Mario Carneiro If we add new templates in the future, it may.

[Mario Carneiro]

why?

[Shreyas Srinivas]

This is fixed if elan manages lake installs separately.

[Mario Carneiro]

lake new $args -> elan new $args

[Mario Carneiro]

new templates, if any, will be dispatched through elan

[Mac Malone]

@Mario Carneiro I guess the question is do we want to manage project templates and other project setup options in the Lake project (e.g. in Lean) or in the elan project (e.g., in Rust).

[Shreyas Srinivas]

Mac said:

Mario Carneiro I guess the question is do we want to manage project templates in the Lake project (e.g. in Lean) or in the elan project (e.g., in Rust).

wait, doesn't cargo manage them (and not rustup) in rust.

[Mario Carneiro]

elan is written in rust

[Shreyas Srinivas]

In my mind : elan = rustup, lake = cargo.

[Shreyas Srinivas]

Mario Carneiro said:

elan is written in rust

Ah okay, I see what you mean.

[Mario Carneiro]

I don't really like the project template system, but such as it is it should be handled in elan

[Shreyas Srinivas]

Still, this seems like a feature in the wrong place. One solution is to combine elan and lake into one project like stack for haskell.

[Mario Carneiro]

because it includes logic like deciding which toolchain to use

[Mario Carneiro]

which is part of why we are talking about this in the first place

[Mario Carneiro]

Again @Shreyas Srinivas , users can still write lake new

[Mario Carneiro]

this is an implementation detail

[Mario Carneiro]

elan new doesn't even have to work literally as written

[Mario Carneiro]

it would be more like elan (masquerading as lake) new

[Mario Carneiro]

because elan is a "multi-personality binary", it uses argv[0] to decide what to do

[Mario Carneiro]

that's what I meant earlier when I said that lake is elan and lean is elan, they are all symlinks to the elan binary

[Mario Carneiro]

the lake +toolchain syntax is parsed by elan before it hands the rest of the args off to the appropriate lake binary

[Shreyas Srinivas]

Hmm.. okay, as long as the interface is the same, I guess the idea is good.

Bonus : I wonder if elan can also manage mathlib in a central place and just simlink to the right version from a project.

[Shreyas Srinivas]

Currently a fresh lake-packages directory consumes 3 GB.

[Sebastian Ullrich]

That's a task for cache get, not elan. You can find previous discussions about symlinking somewhere around here.

[Sebastian Ullrich]

Mario Carneiro said:

Patrick Massot agreed, this lake new foo math could very well be done by elan itself

I like the current separation of concerns, but one simple fix would be for elan to automatically download mathlib4's lean-toolchain and use it when called as lake new foo math.

[Shreyas Srinivas]

Sebastian Ullrich said:

That's a task for cache get, not elan. You can find previous discussions about symlinking somewhere around here.

Okay. The build files are indeed the bigger space hog, not the source files. The last discussion where I asked this question was one or two months ago, and there were other more pressing issues with cache to deal with. The primary obstacle with simlinking itself had something to do with windows not doing well with symlinks. I don't know if OS specific solutions are a good workaround, at least in the short run. I also don't know how the situation has changed on the developers side, but in the meantime mathlib4 is 1GB bigger, and there are more installs.

[Mac Malone]

Another option would be to have Lake cache certain packages in the toolchain and symlink them into the lake-packages directory if possible.