Lean 4 project creation error

Stream: general

[Mario Weitzer]

If I follow these instructions to create a new Lean 4 project with mathlib4:

https://leanprover-community.github.io/install/project.html

I get errors when executing "lake update". What's strange is that tar seems to mix slashes and backslashes for directory separation in the extract command but I'm not sure if this is the root of the problem and if it is how to fix it. If I check, the "build" directory tar claims does not exist, does indeed exist but tar doesn't seem to see it. Here is the log:

$ lake update
warning: Qq: ignoring missing dependency manifest '.\.lake\packages\Qq\lake-manifest.json'
warning: Cli: ignoring missing dependency manifest '.\.lake\packages\Cli\lake-manifest.json'
my_project: no previous manifest, creating one from scratch
mathlib: cloning https://github.com/leanprover-community/mathlib4.git to '.\.lake\packages\mathlib'
std: cloning https://github.com/leanprover/std4 to '.\.lake\packages\std'
Qq: cloning https://github.com/leanprover-community/quote4 to '.\.lake\packages\Qq'
aesop: cloning https://github.com/leanprover-community/aesop to '.\.lake\packages\aesop'
proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '.\.lake\packages\proofwidgets'
Cli: cloning https://github.com/leanprover/lean4-cli to '.\.lake\packages\Cli'
importGraph: cloning https://github.com/leanprover-community/import-graph.git to '.\.lake\packages\importGraph'
mathlib: running post-update hooks
info: [0/9] Downloading proofwidgets cloud release
info: [0/9] Unpacking proofwidgets cloud release
error: > tar -xz -f .\.lake/packages\proofwidgets\.lake\ProofWidgets4.tar.gz -C .\.lake/packages\proofwidgets\.lake\build
error: stderr:
tar: .lake/packages\\proofwidgets\\.lake\build: Cannot open: No such file or directory
tar: Error is not recoverable: exiting now
error: external command tar exited with code 2
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.exe
% Total % Received % Xferd Average Speed Time Time Time Current
Dload Upload Total Spent Left Speed
0 0 0 0 0 0 0 0 --:--:-- --:--:-- --:--:-- 0
100 669k 100 669k 0 0 521k 0 0:00:01 0:00:01 --:--:-- 7295k

installing leantar 0.1.11
uncaught exception: failure in tar #[-xf, C:\Users\Mario\.cache\mathlib\leantar-0.1.11.exe.zip, -C, C:\Users\Mario\.cache\mathlib, --strip-components=1]:
tar: Cannot connect to C: resolve failed

error: mathlib: failed to fetch cache

[Mario Weitzer]

Update:
When I try to execute the command "tar -xz -f .\.lake/packages\proofwidgets\.lake\ProofWidgets4.tar.gz -C .\.lake/packages\proofwidgets\.lake\build" from the log I get this error:

$ tar -xz -f .\.lake/packages\proofwidgets\.lake\ProofWidgets4.tar.gz -C .\.lake/packages\proofwidgets\.lake\build
tar (child): ..lake/packagesproofwidgets.lakeProofWidgets4.tar.gz: Cannot open: No such file or directory
tar (child): Error is not recoverable: exiting now
tar: Child returned status 2
tar: Error is not recoverable: exiting now

but when I change it to "tar -xz -f ./.lake/packages/proofwidgets/.lake/ProofWidgets4.tar.gz -C ./.lake/packages/proofwidgets/.lake/build" (i.e. change all backslashes to slashes) it works fine, so the problem indeed does seem to be with the mix of slashes and backslashes. But how can I make "lake update" use the correct command?

[Mario Carneiro]

are you on WSL?

[Mario Weitzer]

No, I don't use WSL. I exactly followed the instruction on this page

https://leanprover-community.github.io/install/windows.html

and executed the commands from this page

https://leanprover-community.github.io/install/project.html

in git bash. I worked on Lean 3 for some time and wanted to transition to Lean 4. About half a year ago I was able to create a new Lean 4 project following the instructions of the above page but now it doesn't work anymore.

Edit: Also, my old Lean 4 project (which I never did anything with) still works, just the creation of a new one using lake fails now.

[Mario Carneiro]

See whether it works in powershell and/or cmd.exe? I'm not on windows so I'm not sure what the usual thing is here. Perhaps someone else on windows can chime in

[Mario Carneiro]

The error messages are consistent with the commands being run on some linux emulation layer, which is confusing the tools which are expecting windows behavior because the host OS is windows

[Mario Carneiro]

cc: @Mac Malone

[Mario Weitzer]

I hacked the thing by renaming "tar.exe" to "tar1.exe" and writing a program called "tar.exe" which changes '\' to '/' in the arguments it's called with and then passes on the command to tar1.exe. It works now, but the error at the end still remains:

installing leantar 0.1.11
uncaught exception: failure in tar #[-xf, C:\Users\Mario\.cache\mathlib\leantar-0.1.11.exe.zip, -C, C:\Users\Mario\.cache\mathlib, --strip-components=1]:
tar1: Cannot connect to C: resolve failed

[Richard Copley]

What does echo $HOME say?

[Mario Weitzer]

/c/Users/Mario

[Richard Copley]

That's not the problem then. You don't need to write your own version of tar. Everything should just work. The functionality for path conversion is hacked into all the MSYS applications indvidually.

which tar in MSYS or Git Bash should say /usr/bin/tar; does it?

[Mario Weitzer]

Yes, it does. But if that's true, why does it work with my own version of tar but not with the original one?

[Richard Copley]

That's the question indeed :smile: It works just fine for me.

[Richard Copley]

The instructions there are a bit baroque. Can you try this (in Git Bash)?

lake new testproject math
cd testproject
lake update

[Mario Weitzer]

Same problems.
I tried to modify my version of tar to also change "C:" to "/C" to solve the second problem but so far without success.

[Richard Copley]

env | grep MSYS ?

[Mario Weitzer]

$ env | grep MSYS
MSYSTEM=MINGW64
MSYSTEM_CARCH=x86_64
MSYSTEM_CHOST=x86_64-w64-mingw32
PS1=\[\033]0;$TITLEPREFIX:$PWD\007\]\n\[\033[32m\]\u@\h \[\033[35m\]$MSYSTEM \[\033[33m\]\w\[\033[36m\]__git_ps1\[\033[0m\]\n$
MSYSTEM_PREFIX=/mingw64
MSYS=disable_pcon

[Richard Copley]

All good

[Richard Copley]

(disable_pcon: that's "pseudoconsole", not "path conversion")

[Richard Copley]

Want to try one more time?

• Restore c:\Program Files\Git\usr\bin\tar.exe to the original
• Delete the testproject folder created earlier if necessary

export PATH=/mingw64/bin:/usr/local/bin:/usr/bin:/bin:/mingw64/bin:${HOME}/.elan/bin
lake new testproject math
cd testproject
curl -L -O https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain
lake update

[Mario Weitzer]

Same problems:

info: [0/9] Unpacking proofwidgets cloud release
error: > tar -xz -f .\.lake/packages\proofwidgets\.lake\ProofWidgets4.tar.gz -C .\.lake/packages\proofwidgets\.lake\build
error: stderr:
tar: .lake/packages\\proofwidgets\\.lake\build: Cannot open: No such file or directory
tar: Error is not recoverable: exiting now
error: external command tar exited with code 2

and

installing leantar 0.1.11
uncaught exception: failure in tar #[-xf, C:\Users\Mario\.cache\mathlib\leantar-0.1.11.exe.zip, -C, C:\Users\Mario\.cache\mathlib, --strip-components=1]:
tar: Cannot connect to C: resolve failed

error: mathlib: failed to fetch cache

[Mario Weitzer]

Interestingly, when I have my version of tar change "C:" to "/C" I get a different error message:

tar1: This does not look like a tar archive
tar1: Skipping to next header
tar1: Exiting with failure status due to previous errors

And it's correct, "leantar-0.1.11.exe" is a ".zip" file, not a ".tar" file.

[Richard Copley]

Have a look at the source code for validateLeanTar in mathlib\Cache\IO.lean (around where it prints the "installing leantar" message") and see if anything jumps out at you

[Richard Copley]

(note System.Platform.getIsWindows just returns the constant 1, in a version of Lean that was compiled for Windows)

[Richard Copley]

$ md5sum ${HOME}/.cache/mathlib/leantar-0.1.11.exe{,.zip}
b7208cc6bde3e89da98808b3547da64d */c/Users/buster/.cache/mathlib/leantar-0.1.11.exe
da116448572ba930ee176e7dfbfef14e */c/Users/buster/.cache/mathlib/leantar-0.1.11.exe.zip

?

[Mario Weitzer]

$ md5sum ${HOME}/.cache/mathlib/leantar-0.1.11.exe{,.zip}
md5sum: /c/Users/Mario/.cache/mathlib/leantar-0.1.11.exe: No such file or directory
da116448572ba930ee176e7dfbfef14e */c/Users/Mario/.cache/mathlib/leantar-0.1.11.exe.zip

And if I manually extract leantar.exe

$ md5sum ${HOME}/.cache/mathlib/leantar.exe
b7208cc6bde3e89da98808b3547da64d */c/Users/Mario/.cache/mathlib/leantar.exe

I don't get how the tar command is supposed to work anyway. I can't make it extract the .exe file from the .zip archive. I had to use 7-zip.

[Richard Copley]

No, I don't get that either.
Unpack it to the expected filename leantar-0.1.11.exe and try again?

[Mario Weitzer]

$ md5sum ${HOME}/.cache/mathlib/leantar-0.1.11.exe{,.zip}
b7208cc6bde3e89da98808b3547da64d */c/Users/Mario/.cache/mathlib/leantar-0.1.11.exe
da116448572ba930ee176e7dfbfef14e */c/Users/Mario/.cache/mathlib/leantar-0.1.11.exe.zip

[Richard Copley]

sorry, try creating a project again (validateLeanTar starts by checking if leantar already exists at the expected location, and if so, does not try to untar it)

[Mario Weitzer]

Ah, I see. Yes, that worked, at least with my version of tar. Thank you very much! :)
But I guess that's not how this is supposed to work...

[Richard Copley]

I'm happy it's working, but I'm sad we didn't work out why it was going wrong.

[Mauricio Collares]

Which versions of tar extract zip files? Is it the case that Windows comes with its own version of tar which can extract zip files, while the default tar in either Git Bash or MSYS doesn't?

[Richard Copley]

• Apparently bsdtar and not GNU tar
• Apparently yes

$ rm -rf leantar-v0.1.11-x86_64-pc-windows-msvc/
$ /c/Windows/System32/tar.exe -xf leantar-0.1.11.exe.zip
$ ls -d leantar-v0.1.11-x86_64-pc-windows-msvc
leantar-v0.1.11-x86_64-pc-windows-msvc/

$ /c/Windows/System32/tar.exe --version
bsdtar 3.5.2 - libarchive 3.5.2 zlib/1.2.5.f-ipp

$ rm -rf leantar-v0.1.11-x86_64-pc-windows-msvc/
$ tar -xf leantar-0.1.11.exe.zip
tar: This does not look like a tar archive
tar: Skipping to next header
tar: Exiting with failure status due to previous errors

$ tar --version
tar (GNU tar) 1.35
Copyright (C) 2023 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <https://gnu.org/licenses/gpl.html>.
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.

Written by John Gilmore and Jay Fenlason.

[Sebastian Ullrich]

It seems the easiest solution would be to reorder PATH, or not to use an MSYS-based shell for interacting with Lake (the Lean extension can already be used for that to some degree)

[Richard Copley]

validateLeanTar calls runCmd which calls IO.Process.output which uses IO.Process.spawn which is implemented by lean_io_process_spawn which calls spawn (in /src/runtime/process.cpp) which is a wrapper around CreateProcess which has its own ideas about how to find executables and "C:\Windows\System32\tar.exe" takes precedence over what is on the PATH environment variable.

@Mario Weitzer, what's your Windows version? What do you get for /c/Windows/System32/tar.exe --version?

[Mario Weitzer]

Windows 7 Ultimate, but there is no tar.exe in system32. The only tar.exe I have on my laptop comes with git, is in "C:\Git\usr\bin", and is up-to-date:

$ tar --version
tar (GNU tar) 1.35
Copyright (C) 2023 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <https://gnu.org/licenses/gpl.html>.
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.

Written by John Gilmore and Jay Fenlason.

[Mauricio Collares]

Nice, so Richard fully diagnosed the problem! Post April 2018, Windows 10 includes a tar binary by default which can handle zip files, and by Richard's observation it is used regardless of what you have in PATH. But on Windows 7 there is no such built-in binary, so it falls back to Git Bash tar, which is not bsdtar, and fails.

[Mauricio Collares]

I thought Lean 4 didn't support Windows 7, though

[Sebastian Ullrich]

Indeed it does not officially https://lean-lang.org/lean4/doc/setup.html - after all, Windows 7 was already end-of-life before Lean 4 was even released

[Richard Copley]

I shouldn't think it makes any effort to. @Mario Weitzer, you have chosen to walk a difficult path :smile:

[Mario Weitzer]

@Richard Copley I guess so :smile:
This probably also explains the other problem as the version that comes with Windows 10 probably can handle slashes and backslashes simultaneously while the git version can't.

[Mauricio Collares]

I do wonder why leantar for Windows is a zip instead of a .tar.gz if it's going to be unpacked with tar anyway

[Mauricio Collares]

MSYS has bsdtar as an optional package, but I don't know if it handles slashes and backslashes

[Mario Carneiro]

Mauricio Collares said:

I do wonder why leantar for Windows is a zip instead of a .tar.gz if it's going to be unpacked with tar anyway

It's generally easier for windows users to work with .zip files than .tar.gz files

[Mario Carneiro]

but maybe we need to tweak the command line to call unzip or whatever it is called on windows

[Mario Weitzer]

One final update: I replaced the tar.exe in git/usr/bin with bsdtar and now everything works without any additional effort (both, the slash/backslash problem and also the unpacking of leantar-0.1.11.exe). Since even for Windows 10/11 users it is conceivable that a wrong version of tar.exe is called it would probably be a good idea to address this issue somehow. In any case, thanks again for your combined help!