leantar too old (lean exe cache get not working)

Stream: mathlib4

[MohanadAhmed]

On a fresh clone of mathlib I get the following message.

PS C:\Users\Mohanad\LeanStuff> git clone git@github.com:leanprover-community/mathlib4.git
Cloning into 'mathlib4'...
remote: Enumerating objects: 93846, done.
remote: Counting objects: 100% (11031/11031), done.
remote: Compressing objects: 100% (1663/1663), done.
remote: Total 93846 (delta 10317), reused 9419 (delta 9366), pack-reused 82815
Receiving objects: 100% (93846/93846), 40.57 MiB | 2.53 MiB/s, done.
Resolving deltas: 100% (70747/70747), done.
Updating files: 100% (3634/3634), done.
PS C:\Users\Mohanad\LeanStuff> cd .\mathlib4\
PS C:\Users\Mohanad\LeanStuff\mathlib4> lake exe cache get
info: cloning https://github.com/leanprover/std4 to .\lake-packages\std
info: cloning https://github.com/gebner/quote4 to .\lake-packages\Qq
info: cloning https://github.com/JLimperg/aesop to .\lake-packages\aesop
info: cloning https://github.com/mhuisi/lean4-cli.git to .\lake-packages\Cli
info: cloning https://github.com/EdAyers/ProofWidgets4 to .\lake-packages\proofwidgets
info: Downloading proofwidgets/v0.0.11/windows-64.tar.gz
info: Unpacking proofwidgets/v0.0.11/windows-64.tar.gz
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: [6/9] Compiling Cache.Requests
info: [6/9] Building Cache.Main
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache.exe
leantar is too old; downloading more recent version
uncaught exception: no such file or directory (error code: 2)

There is no cache applied and starting vscode triggers a full rebuild.

[MohanadAhmed]

This is on Windows 10 using Powershell terminal

[Mario Carneiro]

this was #5985, it should be fixed on master

[Sebastian Ullrich]

@Mario Carneiro By the way, the "leantar is too old" message doesn't really seem to have any purpose; unlike curl, we don't expect most people to already have leantar in their PATH

[Mario Carneiro]

the message will make more sense once they already have a leantar version

[Mario Carneiro]

I think it is useful to notify that we're downloading another leantar

[Mario Carneiro]

there is already another leantar bump on the queue, so anyone who has the new cache will be seeing the message again for leantar 0.1.4 and it won't be a lie this time

[Sebastian Ullrich]

Then perhaps a simple "downloading new version of leantar"? The current message sounds like a warning, as exhibited by this thread's title

[Mario Carneiro]

how about note: leantar out of date, downloading leantar 0.1.4

[Sebastian Ullrich]

I don't see the need for the first part. It will still be inaccurate for first-time users who are most prone to confusion

[MohanadAhmed]

Mario Carneiro said:

this was #5985, it should be fixed on master

Just tried it about 2 mins ago
Still the same

[MohanadAhmed]

What directory is it looking for?

[MohanadAhmed]

leantar is too old; downloading more recent version
uncaught exception: no such file or directory (error code: 2)

[MohanadAhmed]

option --verbose on lake displays no extra information

[MohanadAhmed]

PS C:\Users\Mohanad\LeanStuff\mgrave> git clone https://github.com/leanprover-community/mathlib4
Cloning into 'mathlib4'...
remote: Enumerating objects: 93851, done.
remote: Counting objects: 100% (11261/11261), done.
remote: Compressing objects: 100% (1711/1711), done.
remote: Total 93851 (delta 10524), reused 9601 (delta 9548), pack-reused 82590
Receiving objects: 100% (93851/93851), 40.75 MiB | 3.46 MiB/s, done.
Resolving deltas: 100% (70720/70720), done.
Updating files: 100% (3634/3634), done.
PS C:\Users\Mohanad\LeanStuff\mgrave> cd .\mathlib4\
PS C:\Users\Mohanad\LeanStuff\mgrave\mathlib4> lake exe cache get!
info: cloning https://github.com/leanprover/std4 to .\lake-packages\std
info: cloning https://github.com/gebner/quote4 to .\lake-packages\Qq
info: cloning https://github.com/JLimperg/aesop to .\lake-packages\aesop
info: cloning https://github.com/mhuisi/lean4-cli.git to .\lake-packages\Cli
info: cloning https://github.com/EdAyers/ProofWidgets4 to .\lake-packages\proofwidgets
info: Downloading proofwidgets/v0.0.11/windows-64.tar.gz
info: Unpacking proofwidgets/v0.0.11/windows-64.tar.gz
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: [6/9] Compiling Cache.Requests
info: [6/9] Building Cache.Main
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache.exe
leantar is too old; downloading more recent version
uncaught exception: no such file or directory (error code: 2)
PS C:\Users\Mohanad\LeanStuff\mgrave\mathlib4> lake --verbose exe cache get!
leantar is too old; downloading more recent version
uncaught exception: no such file or directory (error code: 2)

[Mario Carneiro]

do you have the same symptoms as reported on #5984? What leantar* files are in the $HOME/.cache/mathlib directory?

[Mario Carneiro]

it's most likely looking for leantar.exe, or some messed up spelling of that

[MohanadAhmed]

The version in .cache is 0.1.4

PS C:\Users\Mohanad\LeanStuff\mgrave\mathlib4> cd .\.cache\
PS C:\Users\Mohanad\LeanStuff\mgrave\mathlib4\.cache> dir

    Directory: C:\Users\Mohanad\LeanStuff\mgrave\mathlib4\.cache


Mode                 LastWriteTime         Length Name
----                 -------------         ------ ----
-a----         7/19/2023  11:37 AM         643578 leantar-0.1.4.exe.zip
-a----         7/19/2023   5:14 AM        1540096 leantar.exe

[MohanadAhmed]

After runnig expand archive it seems to work

[MohanadAhmed]

Not ignore that still fails

[MohanadAhmed]

PS C:\Users\Mohanad\LeanStuff\mgrave\mathlib4\.cache> Expand-Archive .\leantar-0.1.4.exe.zip
PS C:\Users\Mohanad\LeanStuff\mgrave\mathlib4\.cache> dir


    Directory: C:\Users\Mohanad\LeanStuff\mgrave\mathlib4\.cache


Mode                 LastWriteTime         Length Name
----                 -------------         ------ ----
d-----         7/19/2023  11:48 AM                leantar-0.1.4.exe
-a----         7/19/2023  11:37 AM         643578 leantar-0.1.4.exe.zip
-a----         7/19/2023   5:14 AM        1540096 leantar.exe


PS C:\Users\Mohanad\LeanStuff\mgrave\mathlib4\.cache> cd ..
PS C:\Users\Mohanad\LeanStuff\mgrave\mathlib4> lake exe cache get!
Attempting to download 3589 file(s)
Downloaded: 3589 file(s) [attempted 3589/3589 = 100%] (100% success)
Decompressing 3589 file(s)
uncaught exception: input/output error (error code: 5)
PS C:\Users\Mohanad\LeanStuff\mgrave\mathlib4>

[MohanadAhmed]

So it seems to have downloaded the files but not able to decompress them (or whatever it is supposed to do after that)

[Mario Carneiro]

it is supposed to have created a file called leantar-0.1.4.exe

[MohanadAhmed]

It looks like it has copied it to leantar.exe without the version number

[MohanadAhmed]

Doing the manual remaing suggested by Eagle941 seems to fix it

[Mario Carneiro]

is the directory named leantar-0.1.4.exe in your second code block just due to manual unpacking?

[MohanadAhmed]

not that was created by lake exe cache get
I think that is probably the mistake right?

[Mario Carneiro]

also, it looks like you just showed the contents of .cache, whereas lake exe cache should be unpacking things into .cache/mathlib, or am I misreading?

[Mario Carneiro]

i.e. the file is supposed to be located at .cache/mathlib/leantar-0.1.4.exe

[MohanadAhmed]

There is no mathlib folder inside the .cache folder

[Sebastian Ullrich]

Why is there a .cache folder in mathlib4/ to begin with?

[Mario Carneiro]

oh good point

[Mario Carneiro]

lake exe cache uses $XDG_CACHE_HOME$/.cache/mathlib, else $HOME$/.cache/mathlib, else ./.cache for the cache directory depending on the presence of those env vars

[Mario Carneiro]

so it sounds like $HOME$ is not defined

[Mario Carneiro]

@MohanadAhmed is there anything at C:\Users\Mohanad\.cache\mathlib?

[MohanadAhmed]

No there is no folder like that

[MohanadAhmed]

Here is the home variable

[MohanadAhmed]

PS C:\Users\Mohanad> echo $HOME
C:\Users\Mohanad

[Mario Carneiro]

can you open Cache/IO.lean and make some edits?

[Mario Carneiro]

at the end of validateLeanTar add this before the final line:

  println! "HOME: {← IO.getEnv "HOME"}"
  println! "running: mv {(IO.CACHEDIR / s!"leantar{EXE}").toString} {LEANTARBIN.toString}"
  let _ ← runCmd "mv" #[(IO.CACHEDIR / s!"leantar{EXE}").toString, LEANTARBIN.toString]

[Mario Carneiro]

then delete the .cache directory and run lake exe cache get

[MohanadAhmed]

I tried the solution suggestd by Eagle941. It seems to work but only if BOTH leantar.exe and leantar-0.1.4.exe are both presentiin the cache folder

PS C:\Users\Mohanad\LeanStuff\mgrave2> git clone https://github.com/leanprover-community/mathlib4
Cloning into 'mathlib4'...
remote: Enumerating objects: 94405, done.                                                                                                                                                                        remote: Counting objects: 100% (14474/14474), done.                                                                                                                                                              remote: Compressing objects: 100% (2242/2242), done.                                                                                                                                                             Updating files: 100% (3634/3634), done.
PS C:\Users\Mohanad\LeanStuff\mgrave2> cd .\mathlib4\
PS C:\Users\Mohanad\LeanStuff\mgrave2\mathlib4> lake exe cache get
info: cloning https://github.com/leanprover/std4 to .\lake-packages\std
info: cloning https://github.com/gebner/quote4 to .\lake-packages\Qq
info: cloning https://github.com/JLimperg/aesop to .\lake-packages\aesop
info: cloning https://github.com/mhuisi/lean4-cli.git to .\lake-packages\Cli
info: cloning https://github.com/EdAyers/ProofWidgets4 to .\lake-packages\proofwidgets
info: Downloading proofwidgets/v0.0.11/windows-64.tar.gz
info: Unpacking proofwidgets/v0.0.11/windows-64.tar.gz
info: [1/9] Building Cache.IO
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [6/9] Compiling Cache.Requests
info: [6/9] Building Cache.Main
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache.exe
leantar is too old; downloading more recent version
uncaught exception: no such file or directory (error code: 2)
PS C:\Users\Mohanad\LeanStuff\mgrave2\mathlib4> cd .\.cache\
PS C:\Users\Mohanad\LeanStuff\mgrave2\mathlib4\.cache> dir leantar*



Mode                 LastWriteTime         Length Name
----                 -------------         ------ ----
-a----         7/19/2023  12:08 PM         643578 leantar-0.1.4.exe.zip
-a----         7/19/2023   5:14 AM        1540096 leantar.exe


PS C:\Users\Mohanad\LeanStuff\mgrave2\mathlib4\.cache> Expand-Archive .\leantar-0.1.4.exe.zip
PS C:\Users\Mohanad\LeanStuff\mgrave2\mathlib4\.cache> dir leantar*


    Directory: C:\Users\Mohanad\LeanStuff\mgrave2\mathlib4\.cache


Mode                 LastWriteTime         Length Name
----                 -------------         ------ ----
d-----         7/19/2023  12:09 PM                leantar-0.1.4.exe
-a----         7/19/2023  12:08 PM         643578 leantar-0.1.4.exe.zip
-a----         7/19/2023   5:14 AM        1540096 leantar.exe


PS C:\Users\Mohanad\LeanStuff\mgrave2\mathlib4\.cache> cp .\leantar-0.1.4.exe\leantar-v0.1.4-x86_64-pc-windows-msvc\leantar.exe .\leantar.exe
PS C:\Users\Mohanad\LeanStuff\mgrave2\mathlib4\.cache> rm -Recurse -Force .\leantar-0.1.4.exe\
PS C:\Users\Mohanad\LeanStuff\mgrave2\mathlib4\.cache> dir leantar*


    Directory: C:\Users\Mohanad\LeanStuff\mgrave2\mathlib4\.cache


Mode                 LastWriteTime         Length Name
----                 -------------         ------ ----
-a----         7/19/2023  12:08 PM         643578 leantar-0.1.4.exe.zip
-a----         7/19/2023   5:14 AM        1540096 leantar.exe


PS C:\Users\Mohanad\LeanStuff\mgrave2\mathlib4\.cache> cp .\leantar.exe .\leantar-0.1.4.exe
PS C:\Users\Mohanad\LeanStuff\mgrave2\mathlib4\.cache> dir leantar*


    Directory: C:\Users\Mohanad\LeanStuff\mgrave2\mathlib4\.cache


Mode                 LastWriteTime         Length Name
----                 -------------         ------ ----
-a----         7/19/2023   5:14 AM        1540096 leantar-0.1.4.exe
-a----         7/19/2023  12:08 PM         643578 leantar-0.1.4.exe.zip
-a----         7/19/2023   5:14 AM        1540096 leantar.exe


PS C:\Users\Mohanad\LeanStuff\mgrave2\mathlib4\.cache> cd ..
PS C:\Users\Mohanad\LeanStuff\mgrave2\mathlib4> lake exe cache get
Attempting to download 3589 file(s)
Downloaded: 3589 file(s) [attempted 3589/3589 = 100%] (100% success)
Decompressing 3589 file(s)
unpacked in 5801 ms
PS C:\Users\Mohanad\LeanStuff\mgrave2\mathlib4>

[Mario Carneiro]

I think mv leantar.exe leantar-0.1.4.exe alone would be sufficient. But I'm more interested in making sure that the script that does the mv works so that you don't have to manually edit the file

[MohanadAhmed]

This is just a guess but before mv leantar.exe leantar-0.1.4.exe is the folder with the same name leantar-0.1.4.exe supposed to there,
The rename will fail silently in powershell.

[MohanadAhmed]

Because the folder and executable file cannot share the same name

[Mario Carneiro]

that makes sense, but the folder shouldn't be there in the first place

[Mario Carneiro]

I think it is being created by extract-archive

[Mario Carneiro]

in the original state before your manual edits:

PS C:\Users\Mohanad\LeanStuff\mgrave2\mathlib4\.cache> dir leantar*



Mode                 LastWriteTime         Length Name
----                 -------------         ------ ----
-a----         7/19/2023  12:08 PM         643578 leantar-0.1.4.exe.zip
-a----         7/19/2023   5:14 AM        1540096 leantar.exe

you can see that there is no directory leantar-0.1.4.exe and also the correct executable has been unpacked as leantar.exe (at least, based on the length), so the only thing that is missing is to rename leantar.exe to leantar-0.1.4.exe

[MohanadAhmed]

Ah OK that was might mistake

[Mario Carneiro]

Mario Carneiro said:

can you open Cache/IO.lean and make some edits?

at the end of validateLeanTar add this before the final line (line 198):

  println! "HOME: {← IO.getEnv "HOME"}"
  println! "running: mv {(IO.CACHEDIR / s!"leantar{EXE}").toString} {LEANTARBIN.toString}"
  let _ ← runCmd "mv" #[(IO.CACHEDIR / s!"leantar{EXE}").toString, LEANTARBIN.toString]

then delete the .cache directory and run lake exe cache get

[MohanadAhmed]

Should it look like this?

def validateLeanTar : IO Unit := do
  if (← LEANTARBIN.pathExists) then return
  if let some version ← some <$> runCmd "leantar" #["--version"] <|> pure none then
    let "leantar" :: v :: _ := version.splitOn " "
      | throw $ IO.userError "Invalidly formatted response from `leantar --version`"
    let some v := parseVersion v | throw $ IO.userError "Invalidly formatted version of `leantar`"
    -- currently we need exactly one version of leantar, change this to reflect compatibility
    if v = (parseVersion LEANTARVERSION).get! then return
  let win := System.Platform.getIsWindows ()
  let target ← if win then
    pure "x86_64-pc-windows-msvc"
  else
    let mut arch ← (·.trim) <$> runCmd "uname" #["-m"] false
    if arch = "arm64" then arch := "aarch64"
    unless arch ∈ ["x86_64", "aarch64"] do
      throw $ IO.userError s!"unsupported architecture {arch}"
    pure <|
      if System.Platform.getIsOSX () then s!"{arch}-apple-darwin"
      else s!"{arch}-unknown-linux-musl"
  IO.println s!"leantar is too old; downloading more recent version"
  IO.FS.createDirAll IO.CACHEDIR
  let ext := if win then "zip" else "tar.gz"
  let _ ← runCmd "curl" #[
    s!"https://github.com/digama0/leangz/releases/download/v{LEANTARVERSION}/leantar-v{LEANTARVERSION}-{target}.{ext}",
    "-L", "-o", s!"{LEANTARBIN}.{ext}"]
  let _ ← runCmd "tar" #["-xf", s!"{LEANTARBIN}.{ext}",
    "-C", IO.CACHEDIR.toString, "--strip-components=1"]
  println! "HOME: {← IO.getEnv "HOME"}"
  println! "running: mv {(IO.CACHEDIR / s!"leantar{EXE}").toString} {LEANTARBIN.toString}"
  let _ ← runCmd "mv" #[(IO.CACHEDIR / s!"leantar{EXE}").toString, LEANTARBIN.toString]

[Mario Carneiro]

yes

[MohanadAhmed]

PS C:\Users\Mohanad\LeanStuff\mgrv\mathlib4> rm -Recurse -Force .\.cache\
PS C:\Users\Mohanad\LeanStuff\mgrv\mathlib4> lake exe cache get
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [4/9] Building Cache.Requests
info: [7/9] Building Cache.Main
info: [9/9] Linking cache.exe
leantar is too old; downloading more recent version
HOME: none
running: mv .cache\leantar.exe .cache\leantar-0.1.4.exe
uncaught exception: no such file or directory (error code: 2)

[Mario Carneiro]

hm, that is basically what I expected... does running mv .cache\leantar.exe .cache\leantar-0.1.4.exe manually work?

[MohanadAhmed]

Note that $HOME is defined by I don't know why it is not picked up

PS C:\Users\Mohanad\LeanStuff\mgrv\mathlib4> rm -Recurse -Force .\.cache\
PS C:\Users\Mohanad\LeanStuff\mgrv\mathlib4> lake exe cache get
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [4/9] Building Cache.Requests
info: [7/9] Building Cache.Main
info: [9/9] Linking cache.exe
leantar is too old; downloading more recent version
HOME: none
running: mv .cache\leantar.exe .cache\leantar-0.1.4.exe
uncaught exception: no such file or directory (error code: 2)
PS C:\Users\Mohanad\LeanStuff\mgrv\mathlib4> echo $HOME
C:\Users\Mohanad

[MohanadAhmed]

Mario Carneiro said:

hm, that is basically what I expected... does running mv .cache\leantar.exe .cache\leantar-0.1.4.exe manually work?

Yes it works

[MohanadAhmed]

PS C:\Users\Mohanad\LeanStuff\mgrv\mathlib4> mv .\.cache\leantar.exe .\.cache\leantar-0.1.4.exe
PS C:\Users\Mohanad\LeanStuff\mgrv\mathlib4> lake exe cache get
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [4/9] Building Cache.Requests
info: [7/9] Building Cache.Main
info: [9/9] Linking cache.exe
Attempting to download 3589 file(s)
Downloaded: 3589 file(s) [attempted 3589/3589 = 100%] (100% success)
Decompressing 3589 file(s)
unpacked in 5256 ms
PS C:\Users\Mohanad\LeanStuff\mgrv\mathlib4>

[David Renshaw]

I'm getting an SSL error:

dwrensha@hafnium:~/src/math-puzzles-in-lean4$ lake exe cache get
info: Downloading proofwidgets/v0.0.11/linux-64.tar.gz
error: > curl -s -f -o ./lake-packages/proofwidgets/build/linux-64.tar.gz -L https://github.com/EdAyers/ProofWidgets4/releases/download/v0.0.11/linux-64.tar.gz
error: external command `curl` exited with code 60
leantar is too old; downloading more recent version
uncaught exception:   % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
curl: (60) SSL: no alternative certificate subject name matches target host name 'objects.githubusercontent.com'
More details here: https://curl.se/docs/sslcerts.html

curl failed to verify the legitimacy of the server and therefore could not
establish a secure connection to it. To learn more about this situation and
how to fix it, please visit the web page mentioned above.

[David Renshaw]

My curl version:

$ curl --version
curl 7.81.0 (x86_64-pc-linux-gnu) libcurl/7.81.0 OpenSSL/3.0.2 zlib/1.2.11 brotli/1.0.9 zstd/1.4.8 libidn2/2.3.2 libpsl/0.21.0 (+libidn2/2.3.2) libssh/0.9.6/openssl/zlib nghttp2/1.43.0 librtmp/2.3 OpenLDAP/2.5.14
Release-Date: 2022-01-05
Protocols: dict file ftp ftps gopher gophers http https imap imaps ldap ldaps mqtt pop3 pop3s rtmp rtsp scp sftp smb smbs smtp smtps telnet tftp
Features: alt-svc AsynchDNS brotli GSS-API HSTS HTTP2 HTTPS-proxy IDN IPv6 Kerberos Largefile libz NTLM NTLM_WB PSL SPNEGO SSL TLS-SRP UnixSockets zstd

[David Renshaw]

It works on my other computer, with curl version

curl 7.86.0 (aarch64-apple-darwin21.3.0) libcurl/7.86.0 OpenSSL/3.0.7 zlib/1.2.13 brotli/1.0.9 zstd/1.5.2 libidn2/2.3.4 libpsl/0.21.1 (+libidn2/2.3.3) nghttp2/1.51.0
Release-Date: 2022-10-26
Protocols: dict file ftp ftps gopher gophers http https imap imaps mqtt pop3 pop3s rtsp smb smbs smtp smtps telnet tftp
Features: alt-svc AsynchDNS brotli HSTS HTTP2 HTTPS-proxy IDN IPv6 Largefile libz NTLM NTLM_WB PSL SSL threadsafe TLS-SRP UnixSockets zstd

[Arthur Paulino]

Your curl dependencies are more up to date on your other computer. In particular, it uses a newer version of OpenSSL

[David Renshaw]

OpenSSL/3.0.2 is from May 2022, and is the current version on ubuntu 22.04.

[David Renshaw]

Ugh. I got it to work by downgrading my system curl from version 7.81.0-1ubuntu1.11 to 7.81.0-1ubuntu1.10:

sudo apt-get install curl=7.81.0-1ubuntu1.10 libcurl4=7.81.0-1ubuntu1.10

So looks like my problem was independent of mathlib/lake/lean.

[Arthur Paulino]

Yeah that's a bit alarming. A bug on some curl release is totally out of our hands

[David Renshaw]

I'm guessing that the problem is that curl 7.81.0-1ubuntu1.11 has a bad fix for CVE-2023-28321.

[Arthur Paulino]

What are your curl dependencies now?

[David Renshaw]

not sure what you're asking, but I can copy/paste a command and post the output, if you want

[David Renshaw]

7.81.0-1ubuntu1.11 came out on Monday, so I expect that others will soon hit this problem and a new version should fix it

[Arthur Paulino]

David Renshaw said:

not sure what you're asking, but I can copy/paste a command and post the output, if you want

Just curl --version.
Your previous call had these:

libcurl/7.81.0 OpenSSL/3.0.2 zlib/1.2.11 brotli/1.0.9 zstd/1.4.8 libidn2/2.3.2 libpsl/0.21.0 (+libidn2/2.3.2) libssh/0.9.6/openssl/zlib nghttp2/1.43.0 librtmp/2.3 OpenLDAP/2.5.14

[David Renshaw]

$ curl --version
curl 7.81.0 (x86_64-pc-linux-gnu) libcurl/7.81.0 OpenSSL/3.0.2 zlib/1.2.11 brotli/1.0.9 zstd/1.4.8 libidn2/2.3.2 libpsl/0.21.0 (+libidn2/2.3.2) libssh/0.9.6/openssl/zlib nghttp2/1.43.0 librtmp/2.3 OpenLDAP/2.5.14
Release-Date: 2022-01-05
Protocols: dict file ftp ftps gopher gophers http https imap imaps ldap ldaps mqtt pop3 pop3s rtmp rtsp scp sftp smb smbs smtp smtps telnet tftp
Features: alt-svc AsynchDNS brotli GSS-API HSTS HTTP2 HTTPS-proxy IDN IPv6 Kerberos Largefile libz NTLM NTLM_WB PSL SPNEGO SSL TLS-SRP UnixSockets zstd

[David Renshaw]

aha, the bug has already been reported: https://bugs.launchpad.net/ubuntu/+source/curl/+bug/2028170

[Mario Carneiro]

Can someone on MacOS Arm64 ("apple silicon") test #6430? A compilation flag that was supposed to be set on windows was instead set on macos aarch64 so those two OSs are the only ones potentially affected. @MohanadAhmed helped me debug the windows issue already

[Eric Rodriguez]

how can I check this?

[Eric Rodriguez]

I have such a mac:)

[Mario Carneiro]

just check out the branch and make sure lake exe cache get still works

[Eric Rodriguez]

Stuff seems to work, the output is slighly different to what I'm used to but doesn't seem worrying

Output

info: updating ./lake-packages/std to revision 7601c54efadd70b688a163f5dcc11ae0ccdf7621
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: [6/9] Compiling Cache.Requests
info: [6/9] Building Cache.Main
info: [9/9] Linking cache
info: stderr:
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
leantar is too old; downloading more recent version
Attempting to download 3133 file(s)
Downloaded: 3133 file(s) [attempted 3133/3133 = 100%] (100% success)
Decompressing 3633 file(s)
unpacked in 3844 ms

[Mario Carneiro]

also, what does ldd ~/.cache/mathlib/leantar-0.1.5 show?

[Eric Rodriguez]

(I'm told otool -L is the equivalent in OSX)

[Mario Carneiro]

I have no idea what that linker warning is about, I've seen it before and it seems to be harmless

[Eric Rodriguez]

/Users/ericr/.cache/mathlib/leantar-0.1.5:
    /usr/lib/libiconv.2.dylib (compatibility version 7.0.0, current version 7.0.0)
    /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1319.0.0)

[Mario Carneiro]

hm, the road to static linking is long

[Matthew Ballard]

I did not actually checkout the branch. One sec...

[Mario Carneiro]

then again, elan also shows those same libraries for its OSX builds, so I'm going to say it's fine

[Matthew Ballard]

Still clean

info: cloning https://github.com/leanprover/std4 to ./lake-packages/std
info: cloning https://github.com/gebner/quote4 to ./lake-packages/Qq
info: cloning https://github.com/JLimperg/aesop to ./lake-packages/aesop
info: cloning https://github.com/mhuisi/lean4-cli.git to ./lake-packages/Cli
info: cloning https://github.com/EdAyers/ProofWidgets4 to ./lake-packages/proofwidgets
info: Downloading proofwidgets/v0.0.13/macOS-64.tar.gz
info: Unpacking proofwidgets/v0.0.13/macOS-64.tar.gz
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: [6/9] Compiling Cache.Requests
info: [6/9] Building Cache.Main
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache
Attempting to download 3633 file(s)
Downloaded: 3633 file(s) [attempted 3633/3633 = 100%] (100% success)
Decompressing 3633 file(s)
unpacked in 2405 ms

[Mario Carneiro]

@Matthew Ballard did you get a leantar is too old; downloading more recent version message?

[Matthew Ballard]

No

[Mario Carneiro]

does ~/.cache/mathlib/leantar-0.1.5 exist?

[Matthew Ballard]

Steps

• remove mathlib
• clone a new copy
• checkout branch
• lake exe cache get!

[Mario Carneiro]

you must have gotten the message on a previous run then

[Matthew Ballard]

I cloned a completely new copy

[Mario Carneiro]

the cache won't be cleared by those steps

[Matthew Ballard]

Ah ok. I see

[Matthew Ballard]

I did get that error on a previous run

[Matthew Ballard]

Do you want me to clear and rerun?

[Matthew Ballard]

I did and nothing changed except the leantar too old

info: cloning https://github.com/leanprover/std4 to ./lake-packages/std
info: cloning https://github.com/gebner/quote4 to ./lake-packages/Qq
info: cloning https://github.com/JLimperg/aesop to ./lake-packages/aesop
info: cloning https://github.com/mhuisi/lean4-cli.git to ./lake-packages/Cli
info: cloning https://github.com/EdAyers/ProofWidgets4 to ./lake-packages/proofwidgets
info: Downloading proofwidgets/v0.0.13/macOS-64.tar.gz
info: Unpacking proofwidgets/v0.0.13/macOS-64.tar.gz
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
leantar is too old; downloading more recent version
Attempting to download 3633 file(s)
Downloaded: 3633 file(s) [attempted 3633/3633 = 100%] (100% success)
Decompressing 3633 file(s)
unpacked in 3897 ms

[Sebastian Ullrich]

Mario Carneiro said:

then again, elan also shows those same libraries for its OSX builds, so I'm going to say it's fine

Yes, one does not simply static-link on macOS