Installation error: "Tried to read from handle containing...

Stream: lean4

[Sebastian Ziesche]

Hi, I just wanted to get started with Lean4. I followed the installation instructions on the website (in various different ways and on different windows machines) but always got the following error:

PS C:\Users\User\Documents\eigene_Programme> git clone https://github.com/leanprover-community/mathematics_in_lean.git
Cloning into 'mathematics_in_lean'...
remote: Enumerating objects: 2396, done.
remote: Counting objects: 100% (200/200), done.
remote: Compressing objects: 100% (113/113), done.
remote: Total 2396 (delta 112), reused 147 (delta 84), pack-reused 2196 (from 1)
Receiving objects: 100% (2396/2396), 41.18 MiB | 6.11 MiB/s, done.
Resolving deltas: 100% (1608/1608), done.
PS C:\Users\User\Documents\eigene_Programme> cd mathematics_in_lean
PS C:\Users\User\Documents\eigene_Programme\mathematics_in_lean> lake exe cache get
info: downloading component 'lean'
230.5 MiB / 230.5 MiB (100 %)   6.6 MiB/s ETA:   0 s
info: installing component 'lean'
info: mathlib: cloning https://github.com/leanprover-community/mathlib4 to '.\.\.lake/packages\mathlib'
info: batteries: cloning https://github.com/leanprover-community/batteries to '.\.\.lake/packages\batteries'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '.\.\.lake/packages\Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '.\.\.lake/packages\aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '.\.\.lake/packages\proofwidgets'
info: importGraph: cloning https://github.com/leanprover-community/import-graph to '.\.\.lake/packages\importGraph'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient to '.\.\.lake/packages\LeanSearchClient'
info: plausible: cloning https://github.com/leanprover-community/plausible to '.\.\.lake/packages\plausible'
info: Cli: cloning https://github.com/leanprover/lean4-cli to '.\.\.lake/packages\Cli'
installing leantar 0.1.14
uncaught exception: Tried to read from handle containing non UTF-8 data.

I already searched the web and discussed for some time with ChatGPT but to no avail. In particular it is strange, that it happens on my 12 year old win10 desktop machine as well as on my 5 year old win11 Laptop.

Has anybody an idea what is going wrong?

[Kevin Buzzard]

Try disabling antivirus?

[Sebastian Ziesche]

that made the error go away, lets see if that was the last problem =)

[Sebastian Ziesche]

alright, thx alot. The "Mathematics in Lean" stuff seems to work after a "Restart File".