error adding leancopilot

Stream: lean4

[Jared green]

i tried adding leancopilot, i got this:

ASUS@GHD05 MINGW64 ~/OneDrive/Documents/lean projects/polySat (master)
$ lake exe LeanCopilot/download
PANIC at getOS! lakefile:16:4: Windows is not supported
PANIC at getOS! lakefile:16:4: Windows is not supported
info: [0/4] Downloading LeanCopilot cloud release
info: [0/4] Unpacking LeanCopilot cloud release
error: > tar -xz -f .\.lake/packages\LeanCopilot\.lake\x86_64-linux.tar.gz -C .\.lake/packages\LeanCopilot\.lake\build
error: stderr:
./OpenBLAS/libopenblas.a: Can't create '\\\\?\\C:\\Users\\ASUS\\OneDrive\\Documents\\lean projects\\polySat\\.lake\\packages\\LeanCopilot\\.lake\\build\\OpenBLAS\\libopenblas.a'
./OpenBLAS/libopenblas.so: Can't create '\\\\?\\C:\\Users\\ASUS\\OneDrive\\Documents\\lean projects\\polySat\\.lake\\packages\\LeanCopilot\\.lake\\build\\OpenBLAS\\libopenblas.so'
./OpenBLAS/libopenblas.so.0: Can't create '\\\\?\\C:\\Users\\ASUS\\OneDrive\\Documents\\lean projects\\polySat\\.lake\\packages\\LeanCopilot\\.lake\\build\\OpenBLAS\\libopenblas.so.0'
tar: Error exit delayed from previous errors.
error: external command `tar` exited with code 1
info: [1/4] Cloning OpenBLAS from https://github.com/OpenMathLib/OpenBLAS
error: > git clone --recursive https://github.com/OpenMathLib/OpenBLAS    # in directory .\.lake/packages\LeanCopilot\.lake\build
error: stderr:
fatal: destination path 'OpenBLAS' already exists and is not an empty directory.
error: external command `git` exited with code 128
error: no such file or directory (error code: 2)
  file: .\.lake/packages\LeanCopilot\.lake\build\lib\openblas.dll

is this a problem?

[Kevin Buzzard]

If you're trying to run it on Windows then I would imagine that the fact that Windows is not listed as a supported OS in the readme of leancopilot is a problem. Or are you using WSL?

[Jared green]

whats wsl?

[Kevin Buzzard]

I don't know, I don't use Windows, I'm just reading the readme for leancopilot.

[Kevin Buzzard]

And the third line of the error you posted

[Jared green]

its the 'windows subsystem for linux'. it seems that is part of windows.

[Kevin Buzzard]

I wasnt sure whether it was a way to make non-Windows machines run Windows or a way to make Windows behave like a non-Windows machine (sounds like the latter), but it looks like whatever it is that's what you're going to have to get your head around if you want to use leancopilot on your machine

[Jared green]

os support doesnt appear to be the problem. i deleted the target folder and tried again, got a different error:

ASUS@GHD05 MINGW64 ~/OneDrive/Documents/lean projects/polySat (master)
$ lake exe LeanCopilot/download
PANIC at getOS! lakefile:16:4: Windows is not supported
PANIC at getOS! lakefile:16:4: Windows is not supported
info: [1/4] Cloning OpenBLAS from https://github.com/OpenMathLib/OpenBLAS
info: [1/4] Building OpenBLAS with `make NO_LAPACK=1 NO_FORTRAN=1 -j8`
error: failed to execute `make`: no such file or directory (error code: 2)
error: no such file or directory (error code: 2)
  file: .\.lake/packages\LeanCopilot\.lake\build\lib\openblas.dll

[Yaël Dillies]

Note that one of the slashes is / while the other ones are \ That sounds like an OS support issue to me.

[Jared green]

no, there is literally a file missing.

[Kevin Buzzard]

Are you now using WSL?

[Yaël Dillies]

Jared green said:

no, there is literally a file missing.

Yeah maybe because it is looking for the file openblas.dll in folder lib in folder .lake in folder LeanCopilot in folder .lake/packages, but in fact the file is openblas.dll in folder lib in folder .lake in folder LeanCopilot in folder .lake in folder packages.

[Jared green]

the suggested path also doesnt exist.

[Sebastian Ullrich]

Jared green said:

os support doesnt appear to be the problem

It quite explicitly says "Windows is not supported" in the log, I would heed that

[Jared green]

i just installed wsl, now what?

[Kevin Buzzard]

I guess you start by firing up WSL and then install lean following the instructions on the community website or the lean manual

[Kevin Buzzard]

Maybe you have to install some Linux OS first?

[Kevin Buzzard]

But basically you're now using a new OS so you have to install everything on it

[Jared green]

it automatically installed ubuntu.

[Jared green]

jared@GHD05:~$ sudo apt install git curl
-bash: /usr/bin/sudo: Input/output error
jared@GHD05:~$ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
mktemp: too few X's in template ‘elan’
elan: command failed: mktemp -d -t elan
info: downloading installer
mkdir: cannot create directory ‘’: No such file or directory
elan: command failed: mkdir -p

[Richard Copley]

There's an unfortunate bug in the elan-init.sh script (mktemp -d -t elan should probably read mktemp -d -t elan.XXXX), but is is a red herring. The bug ordinarily does not affect anybody, because the previous command mktemp -d 2>/dev/null does not ordinarily fail. The reason it failed for you is hard to debug on a purely psychic level. It might be the same reason that sudo failed. I suggest you make sure there is sufficient space on your C: drive, then run wsl --shutdown, then start wsl.exe again, and retry the instructions.

[Kevin Buzzard]

My experience with Input/output error on Ubuntu is that it means your disc drive is borked or full. Have you committed enough disc space to Ubuntu?

[Richard Copley]

https://learn.microsoft.com/en-us/windows/wsl/disk-space

[Jared green]

how much space is required?

[Jared green]

the c drive has 1.54 gb

[Jared green]

*left

[Kevin Buzzard]

If you're planning on using mathlib then that's 4gb straight away

[Jared green]

i had intended to also use leancopilot.

[Kevin Buzzard]

IIRC there's some download for leancopilot but I don't know whether that's all happening in the .lake directory of your repo or whether it's external. I have a project depending on mathlib and in .lake/packages/LeanCopilot it's another 400 megs, but I don't remember whether that is all of leancopilot unfortunately.

[Jared green]

does the default model run locally?

[Patrick Massot]

Yes

[Jared green]

and how large is that?