could not rename packages directory

Stream: lean4

[Bernardo Borges]

I am having the exact same problem, however on this environment:
toolchain
leanprover/lean4:v4.7.0
lakefile

import Lake
open Lake DSL

package «lean-cutting-planes» where

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

lean_lib «LeanCuttingPlanes» where

@[default_target]
lean_exe «lean-cutting-planes» where
  root := `Main

And also, lake update returns:

PS D:\ic\lean-cutting-planes> lake update
error: «lean-cutting-planes»: could not rename packages directory (.\.lake/packages -> .\.lake\packages): no error (error code: 0)

And lake exe cache get:

PS D:\ic\lean-cutting-planes> lake exe cache get
info: [1/9] Building Cache.IO
info: [2/9] Building Cache.Hashing
info: [2/9] Compiling Cache.IO
info: [4/9] Compiling Cache.Hashing
info: [4/9] Building Cache.Requests
info: [6/9] Building Cache.Main
info: [6/9] Compiling Cache.Requests
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache.exe
No files to download
Decompressing 4381 file(s)
[...]
C:\Users\foo\.cache\mathlib\0f6c25b493881f3b.ltar: The process cannot access the file because it is being used by another process. (os error 32)
uncaught exception: leantar failed with error code 1

And with lake build

PS D:\ic\lean-cutting-planes> lake build
[1395/1395] Linking lean-cutting-planes.exe
error: failed to execute `c:\Users\foo\.elan\toolchains\leanprover--lean4---v4.7.0\bin\leanc.exe`: unspecified system_category error (error code: 87)

Now, with a fresh project that depends on mathlib4 it's the same

[Floris van Doorn]

I get this error as well on Windows when trying to run lake update in a project using leanprover/lean4:v4.7.0-rc2

[Sebastian Ullrich]

The original issue was fixed in 4.8.0, for other errors let's start separate threads/issue reports

[Notification Bot]

3 messages were moved here from #mathlib4 > error building windows exe proj by Floris van Doorn.

[Sebastian Ullrich]

Ah, if the rename is the error you received, then that as well should be fixed :) https://github.com/leanprover/lean4/commit/e54a0d7b89b7b8e4393b91e81f471d81f67ca713

[Floris van Doorn]

Ok, I moved this to a separate thread.
When running lake update in Windows in this repository
https://github.com/fpvandoorn/carleson/tree/9e06a00378a321140e8fd366a8f5fa96844f1fc5
at Lean version leanprover/lean4:v4.7.0-rc2
I get the error

Floris@Dell-E MINGW64 ~/projects/carleson (master)
$ lake update
error: carleson: could not rename packages directory (.\.lake/packages -> .\.lake\packages): no error (error code: 0)

[Floris van Doorn]

Sebastian Ullrich said:

Ah, if the rename is the error you received, then that as well should be fixed :) https://github.com/leanprover/lean4/commit/e54a0d7b89b7b8e4393b91e81f471d81f67ca713

What is currently the most convenient way to update lean-toolchain when lake update errors?

[Mario Carneiro]

there isn't one, it's copy paste

[Mario Carneiro]

the convenient way is the mathlib post-update hook but this only works if lake hasn't had a forward-incompatible change recently

[Floris van Doorn]

I can confirm that this is fixed after manually replacing the contents of lean-toolchain with leanprover/lean4:v4.8.0-rc1. Thanks!

[Bernardo Borges]

Right now the error changed to aesop config:

PS D:\ic\lean-cutting-planes> lake update
error: .\.lake\packages\aesop\lakefile.toml:1:0: error: unexpected identifier; expected command
error: .\.lake\packages\aesop\lakefile.toml: package configuration has errors

[Sebastian Ullrich]

Your lean-toolchain is likely older than aesop's, try copying it over

[Bernardo Borges]

Changed to leanprover/lean4:v4.8.0-rc1. Now lake update works

[Bolton Bailey]

@Kim Morrison made lean#4103 last night about how there should be more of a warning for toolchain mismatch on lake update, so if anyone is looking for an issue to upvote, perhaps this is it.

[Bernardo Borges]

However on lake build i get a huge error ending with:

error: failed to execute 'c:\Users\bernb\.elan\toolchains\leanprover--lean4---v4.8.0-rc1\bin\leanc.exe': unspecified system_category error (error code: 87)
Some build steps logged failures:
- Linking lean-cutting-planes.exe
error: build failed

[Bolton Bailey]

Last night I had to rm -rf .lake to remove the .lake folder to get it to work after I updated the toolchain

[Bernardo Borges]

Bolton Bailey said:

Last night I had to remove the .lake folder to get it to work after I updated the toolchain

What is your toolchain now?

[Bolton Bailey]

leanprover/lean4:v4.8.0-rc1

[Bolton Bailey]

Hmm, maybe this is a different issue, sorry, lake update was the thing that was broken for me after updating the toolchain.

[Bernardo Borges]

Tried deleting .lake but the outcome is the same, sadly.

[Kim Morrison]

@Bernardo Borges, could you post the URL of a repo that shows this problem?

[Bernardo Borges]

Kim Morrison said:

Bernardo Borges, could you post the URL of a repo that shows this problem?

Surely, its https://github.com/bernborgess/lean-cutting-planes

[Kim Morrison]

@Bernardo Borges, for me:

• git clone https://github.com/bernborgess/lean-cutting-planes
• cd lean-cutting-planes
• git checkout 3eae7fc729e0c895d28992a36b271b8f485c28bf (current master)
• change lean-toolchain to leanprover/lean4:v4.8.0-rc1
• lake update
• lake exe cache get
• lake build

succeeds.

[Bernardo Borges]

Ok! I'll try it again this way

[Bernardo Borges]

So, I cloned the project again and followed each step. All is fine, until the lake build, that fails with an error (password is "rename")

error: failed to execute 'c:\Users\bernb\.elan\toolchains\leanprover--lean4---v4.8.0-rc1\bin\leanc.exe': unspecified system_category error (error code: 87)
Some build steps logged failures:
- Linking lean-cutting-planes.exe
error: build failed

[Kim Morrison]

Sorry, this has exceeded my lake expertise, I've never built an .exe on windows. :-(

[Richard Copley]

87 is ERROR_INVALID_PARAMETER ("The parameter was incorrect"). Looks like lake called CreateProcess with a 56856-character string as the lpCommandLine argument, and that's invalid because the maximum length for that parameter is 32767 characters. I was able to get an exe by writing the arguments to a file args.txt then invoking leanc as leanc.exe @args.txt. Maybe lake should be doing that for you.

[Kim Morrison]

@Mac Malone, do you know what's going on here?

We may need a bug report with a repro.

[Mac Malone]

@Kim Morrison Yeah, this should get a bug report. Command line limits were a anticipated problem but were put off until they actually become one. It seems we have reached that point.

[Kim Morrison]

@Richard Copley, would you be able to write an issue at the lean repository showing how to reproduce your observations above?

[Richard Copley]

Not until this evening (after 2024-05-10T17:00:00+01:00) or tomorrow, I'm afraid, so if someone beats me to it that would be good. I did the commands in your message and got the same error as Bernardo, so anyone on Windows should be able to do it.

[Richard Copley]

Actually @Kim Morrison, @Mac Malone, I'll be a little more assertive, and say that I'm not the right person to create the bug report, because I don't know enough about Lean as a general-purpose language to do it properly. Sorry!

[Bernardo Borges]

How can I help?

[Kim Morrison]

@Bernardo Borges, pretty much just combining my command line list above, with whatever output you get from running that on WIndows. Richard's post above seems to do a good job of highlighting the relevant information. We just need it in an issue on the lean4 repository, so that when and if Mac has time to deal with it, there's a simple to reproduce bug to observe.

[Bernardo Borges]

Created the issue https://github.com/leanprover/lean4/issues/4159

[Eric Taucher]

Any updates or workarounds on this?

I am on Windows 11 trying to use
https://github.com/teorth/equational_theories/tree/main

with the command

C:\Users\XYZ\Projects\learn_4_equational> lake exe extract_implications --json > C:\Users\XYZ\Desktop\equational_theories\implications.json

which is a Windows command similar to

https://github.com/teorth/equational_theories/blob/main/.github/workflows/blueprint.yml#L173-L177

and getting

error: failed to execute 'c:\Users\XYZ\.elan\toolchains\leanprover--lean4---v4.13.0-rc3\bin\leanc.exe': unspecified system_category error (error code: 87)
Some build steps logged failures:
- extract_implications
error: build failed

---

I did see this related work around so will give it a try

Richard Copley said:

I was able to get an exe by writing the arguments to a file args.txt then invoking leanc as leanc.exe @args.txt.

but really do not understand what was done.

[Richard Copley]

For the case above, I wrote lake build --verbose instead of lake build. This outputs the commands that lake is running. One of those commands was the offending leanc.exe invocation. I copied the terminal output into a text editor so I could snip out that invocation, then saved only the arguments (the part of the command line after "leanc.exe") into a text file "args.txt". Then I ran leanc.exe @args.txt.

I don't know how to adapt that to the case of lean exe extract_implications --json. Does lean build extract_implications --verbose do anything? I'll try it, but first I need to do

git clone https://github.com/teorth/equational_theories
cd equational_theories
lake exe cache get
lake build

which will take some time.

[Eric Taucher]

Richard Copley said:

I don't know how to adapt that to the case of lean exe extract_implications --json.

No worries. Seems that OpenAI canvas might be of value here. Still working with it but it did give a suggestion.

[Richard Copley]

lake build extract_implications --verbose seems to be working.

[Richard Copley]

It seems to work. Of note:

• I had to replace backslashes \ with forward slashes / in args.txt
• I had to delete the argument -leanshared from args.txt to avoid an error "unable to find library -leanshared"; I'm not sure if this will cause trouble later on.

[Eric Taucher]

It was going good then failed

Starting from a new directory to get a clean install of the repository.

git clone https://github.com/teorth/equational_theories
cd equational_theories
lake exe cache get

then this caused it to fail with the same error.

lake  build extract_implications --verbose

[Richard Copley]

Yes, that's expected. But it still outputs the commands, and you know what to do next.

[Richard Copley]

The output from

lake build extract_implications --verbose

ends with

[916/916] Building extract_implications
trace: .> c:\Users\buster\.elan\toolchains\leanprover--lean4---v4.13.0-rc3\bin\leanc.exe {{{a gigantic heap of stuff}}} -leanshared
error: failed to execute 'c:\Users\buster\.elan\toolchains\leanprover--lean4---v4.13.0-rc3\bin\leanc.exe': unspecified system_category error (error code: 87)

• Copy {{{a gigantic heap of stuff}}} (all the text between leanc.exe and -leanshared, excluding leanc.exe and -leanshared) from the output and paste it into a text editor.
• Replace the backslashes with forward slashes.
• Save it as args.txt (in the top-level directory of your equational_theories tree).
• Run the following commands (also in the top-level directory):

leanc.exe @args.txt
leanc.exe @args.txt -leanshared
lake exe extract_implications --json

It is weird that I needed to run leanc.exe twice, but that is what works.

[Richard Copley]

@Eric Taucher, is anything unclear? Does it work for you?

[Eric Taucher]

Richard Copley said:

@Eric Taucher, is anything unclear? Does it work for you?

Bouncing between many tasks but what you note makes sense. Slowing making progress between all the tasks I am juggling, e.g. helping others on the OpenAI forum, trying to see the comet (ref)

[Eric Taucher]

Still working on this

Currently failing at the last step, still with error code: 87

lake exe extract_implications --json

I will take a shot at this using WSL on another machine and see if that works, however I have not installed Lean on WSL and the machine only has 8GB of memory so not optimistic.

The current goal is to just get the data needed to create graphs used by the Equational project, e.g.

https://teorth.github.io/equational_theories/graphiti/?render=true&implies=14&highlight_red=14

https://teorth.github.io/equational_theories/graphiti/?render=true&limit_equations=1%2C+2%2C+3%2C+4%2C+5%2C+6%2C+7%2C+8%2C+23%2C+38%2C+39%2C+40%2C+41%2C+42%2C+43%2C+45%2C+46%2C+168%2C+387%2C+4512%2C+4513%2C+4522%2C+4564%2C+4579%2C+4582

[Richard Copley]

The intention is that extract_implications.exe already exists and is newer than all its dependencies, so that lake decides that it does not need to be built.

• Does lake build extract_implications --verbose give the same error as before, with the failing command being similar to leanc.exe -o extract_implications.exe [...]?
• Does extract_implications.exe already exist?
• Have you changed any source files since you created it?

[Eric Taucher]

@Richard Copley

Thanks!

It worked just had to run the steps in order without any mistakes. In essence started all over and learned from previous mistakes.

Change to a directory with user write permissions, used C:\User\Groot\Projects

git clone https://github.com/teorth/equational_theories
cd equational_theories
lake exe cache get
lake build
lake build extract_implications --verbose > extract_implications_verbose.txt

The output from

lake build extract_implications --verbose

ends with

[916/916] Building extract_implications
trace: .> c:\Users\buster\.elan\toolchains\leanprover--lean4---v4.13.0-rc3\bin\leanc.exe {{{a gigantic heap of stuff}}} -leanshared
error: failed to execute 'c:\Users\buster\.elan\toolchains\leanprover--lean4---v4.13.0-rc3\bin\leanc.exe': unspecified system_category error (error code: 87)

• Copy {{{a gigantic heap of stuff}}} (all the text between leanc.exe and -leanshared, excluding leanc.exe and -leanshared) from the output and paste it into a text editor.
• Replace .\.\.lake with .lake
• Replace the backslashes with forward slashes.
• Save it as args.txt (in the top-level directory of your equational_theories tree).

dir args.txt

10/19/2024  09:25 AM            32,923 args.txt

Sample of args.txt

-o .lake/build/bin/extract_implications.exe
.lake/build/ir/scripts/extract_implications.c.o.export
.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Init/Lemmas.c.o.export
...
.lake/build/ir/equational_theories/EquationalResult.c.o.export
.lake/build/ir/equational_theories/Closure.c.o.export
.lake/packages/MD4Lean/.lake/build/md4c/libleanmd4c.a

• Run the following commands (also in the top-level directory):

leanc.exe @args.txt
leanc.exe @args.txt -leanshared
lake exe extract_implications --json > extract_imiplications.json

dir extract_imiplications.json

10/19/2024  09:28 AM        26,382,724 extract_imiplications.json

Sample of extract_implications.json

{"nonimplications":[{"rhs":"Equation2", "lhs":"Equation1"},{"rhs":"Equation3", "lhs":"Equation1"},
...
{"rhs":"Equation1", "lhs":"Equation4658"},{"rhs":"Equation1", "lhs":"Equation4666"}]}