leantar error while installing

Stream: mathlib4

[Kenji Fujita]

The following error messages are displayed on Windows 11 when "lake exe cache get" in mathematics_in_lean folder according to the instruction in "https://leanprover-community.github.io/install/project.html".

---

installing leantar 0.1.14
uncaught exception: Tried to read from handle containing non UTF-8 data.

---

Is there any idea to solve above?

[Sebastian Ullrich]

Are there any special characters in the target directory path or your home directory?

[Kenji Fujita]

Hi Sebastian. Thank you for your advice. Therefore, no special characters are in target directory path or my home directory(as below). I tried "lake exe cache get" both in "Git Bash" and "Git CMD" but the results were same. I'm using Japanese version of Windows 11 which can be the reason?

---

$ pwd
/c/Users/kenji/lean4/mathematics_in_lean

kenji@Fujita MINGW64 ~/lean4/mathematics_in_lean (master)
$ cd

kenji@Fujita MINGW64 ~
$ pwd
/c/Users/kenji

[Kenji Fujita]

I tried "lake --verbose exe cache get" as below and curious characters "邃ｹ" which cannot be read by Japanese people are displayed. This can be the reason.
Is there any solution?

---

$ lake --verbose exe cache get
邃ｹ [2/10] Replayed Cache.IO
trace: .> LEAN_PATH=.\.\.lake/packages\batteries\.lake\build\lib;.\.\.lake/packages\Qq\.lake\build\lib;.\.\.lake/packages\aesop\.lake\build\lib;.\.\.lake/packages\proofwidgets\.lake\build\lib;.\.\.lake/packages\Cli\.lake\build\lib;.\.\.lake/packages\importGraph\.lake\build\lib;.\.\.lake/packages\LeanSearchClient\.lake\build\lib;.\.\.lake/packages\plausible\.lake\build\lib;.\.\.lake/packages\mathlib\.lake\build\lib;.\.\.lake\build\lib PATH c:\Users\kenji\.elan\toolchains\leanprover--lean4---v4.13.0\bin\lean.exe -Dpp.unicode.fun=true -DautoImplicit=false -Dweak.linter.docPrime=true -Dweak.linter.hashCommand=true -Dweak.linter.oldObtain=true -Dweak.linter.refine=true -Dweak.linter.style.cdot=true -Dweak.linter.style.dollarSyntax=true -Dweak.linter.style.header=true -Dweak.linter.style.lambdaSyntax=true -Dweak.linter.style.longLine=true -Dweak.linter.style.longFile=1500 -Dweak.linter.style.missingEnd=true -Dweak.linter.style.multiGoal=true -Dweak.linter.style.setOption=true .\.\.lake/packages\mathlib\.\.\Cache\IO.lean -R .\.\.lake/packages\mathlib\.\. -o .\.\.lake/packages\mathlib\.lake\build\lib\Cache\IO.olean -i .\.\.lake/packages\mathlib\.lake\build\lib\Cache\IO.ilean -c .\.\.lake/packages\mathlib\.lake\build\ir\Cache\IO.c --json
---- (omittied)-----
邃ｹ [10/10] Replayed cache
trace: .> c:\Users\kenji\.elan\toolchains\leanprover--lean4---v4.13.0\bin\leanc.exe -o .\.\.lake/packages\mathlib\.lake\build\bin\cache.exe .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Main.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Cache\IO.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Hashing.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Requests.c.o.noexport
installing leantar 0.1.14
uncaught exception: Tried to read from handle containing non UTF-8 data.

[Sebastian Ullrich]

I don't think so, that is your terminal misinterpreting Lake's output while the exception is internal to some Lean program

[Mauricio Collares]

Can you tell us what's the output of echo $HOMEPATH, echo $HOMEDRIVE and echo $USERPROFILE?

[Mauricio Collares]

Also, do you have any files whose name start with leantar in $HOMEDRIVE\$HOMEPATH\.cache\mathlib?

[Mauricio Collares]

If the answer to the last question is "yes", the problem is likely from curl's json output. To simulate what Cache is doing, please run curl --request GET --fail --silent --write-out "%{json}\n" https://lakecache.blob.core.windows.net/mathlib4/f/b9a8c5908014b028.ltar -o b9a8c5908014b028.ltar and paste the output here. It should be a single very long line, with about 19k characters. You can also paste the output on pastebin.com if you prefer.

[Mauricio Collares]

See also #lean4 > lake cache on Windows with Chinese locale, where it is claimed that changing the system locale to UTF-8 is a workaround (but please run the above commands before trying this, since the data will be valuable!)

[Kenji Fujita]

The followings are the result. curl's output were only "test.json" and I tried curl with "-v" option again.

---

$ echo $HOMEPATH
\Users\kenji

kenji@Fujita202212 MINGW64 ~/.cache/mathlib
$ echo $HOMEDRIVE
C:

kenji@Fujita202212 MINGW64 ~/.cache/mathlib
$ echo $USERPROFILE
C:\Users\kenji

kenji@Fujita202212 MINGW64 ~/.cache/mathlib
$ ls -la
total 0
drwxr-xr-x 1 kenji 197121 0 Dec 3 21:43 ./
drwxr-xr-x 1 kenji 197121 0 Dec 3 21:43 ../

kenji@Fujita202212 MINGW64 ~/.cache/mathlib
$ curl --request GET --fail --silent --write-out test.json https://lakecache.blob.core.windows.net/mathlib4/f/b9a8c5908014b028.ltar -o b9a8c5908014b028.ltar
test.json
kenji@Fujita202212 MINGW64 ~/.cache/mathlib
$ curl -v --request GET --fail --silent --write-out test.json https://lakecache.blob.core.windows.net/mathlib4/f/b9a8c5908014b028.ltar -o b9a8c5908014b028.ltar

• Host lakecache.blob.core.windows.net:443 was resolved.
• IPv6: (none)
• IPv4: 20.209.19.193
• Trying 20.209.19.193:443...
• schannel: disabled automatic use of client certificate
• schannel: next InitializeSecurityContext failed: CRYPT_E_NO_REVOCATION_CHECK (0x80092012) - 失効の関数は証明書の失効を確認できませんでした。
• closing connection #0
  test.json
  kenji@Fujita202212 MINGW64 ~/.cache/mathlib

[Mauricio Collares]

Sorry, I messed up the command! It should have been curl --request GET --fail --silent --write-out "%{json}\n" https://lakecache.blob.core.windows.net/mathlib4/f/b9a8c5908014b028.ltar -o b9a8c5908014b028.ltar. But I think the output with -v already gives us enough information to figure out what went wrong.

[Mauricio Collares]

Basically, curl failed to verify the SSL certificate, and part of the error message is in (non-UTF8) Japanese. In other words, the encoding error is just masking a SSL certificate error. The most common reason for SSL certificate issues is antivirus software intercepting the connection with self-signed certificates; you can read #mathlib4 > lake exe cache get errors @ 💬 to see workarounds for most popular antivirus software. If you do use another antivirus software, let me know how it names the equivalent of "encrypted connection scanning" (or let me know what's the antivirus so we can figure it out together).

[Kenji Fujita]

Thanks for good advice. Finally, I succeeded "lake exe cache get" after disabling AVAST anti virus temporally.