an error

Stream: new members

[tsuki hao]

import Mathlib.Data.Set.Lattice
import Mathlib.Data.Nat.Prime
import Mathlib.Data.Nat.Parity
import Mathlib.Tactic

section
variable {α : Type _}
variable (s t u : Set α)
open Set

example : s ∩ t = t ∩ s := by
  ext x
  simp only [mem_inter_iff]
  constructor
  · rintro ⟨xs, xt⟩
    exact ⟨xt, xs⟩
  . rintro ⟨xt, xs⟩
    exact⟨xs,xt⟩

There is an error reporting expected checkColGt, does anyone know why?

[Ruben Van de Velde]

No error here

[Anne Baanen]

These kinds of checkColGt errors indicate that Lean has trouble parsing indentation, but I can't see any error here.

[Peter Gumm]

I think I got Lean4 installed. Trying "Mathematics in Lean" , the first line "import Mathlib.Data.Nat.Basic" results in an error:
c:\Users\gumm\.elan\toolchains\leanprover--lean4---nightly-2023-06-20\bin\lake.exe print-paths Init Mathlib.Data.Nat.Basic Mathlib.Data.Nat.Parity Mathlib.Tactic` failed:

stderr:
info: [52/379] Building Std.CodeAction.Attr
....
error: external command c:\Users\gumm\.elan\toolchains\leanprover--lean4---nightly-2023-06-20\bin\lean.exe exited with code 3221225477

What to do?

[Ruben Van de Velde]

Did you run a lake exe cache get command?

[Eric Wieser]

Note that you have to stop vscode from running lean before running that command, either by closing vscode, or running pkill lean first.

[Peter Gumm]

I did all commands described in the Manual
OK I ran the command ...
OK I killed lean and ran the command again
Now I get a Windows message
image.png

[Mauricio Collares]

Try killing lean and running lake exe cache get! instead (the exclamation point forces redownloading existing files). Corrupted caches are weirdly common.

[Peter Gumm]

OK, I did it. But that command has been stuck for some minutes now after "99%" :
Here is my command and lake's response:

C:\Users\gumm\mathematics_in_lean>lake exe cache get!

Attempting to download 3538 file(s)
Downloaded: 3527 file(s) [attempted 3527/3538 = 99%]

Hm !!??

[Mauricio Collares]

Yes, that (stalled downloads and cache corruption on less-than-perfect network connections) matches my pre-leantar experience too, unfortunately. Hopefully there will be a mathlib bump soon so leantar can be used in mathematics_in_lean.

[Mauricio Collares]

If you run gzip -t *.gz inside the cache folder (should be called .mathlib in your home folder or something) then it will tell you which files are corrupted. You can then delete them and run lake exe cache get (without the exclamation point) to re-download the files you deleted.

[Mauricio Collares]

Assuming you have a working gzip program on windows, at least

[Mauricio Collares]

Test mathlib bump at https://github.com/leanprover-community/mathematics_in_lean/pull/9 if you want to see if it helps with your cache corruption problems

[Mauricio Collares]

(A "proper" mathlib bump is at https://github.com/avigad/mathematics_in_lean_source/pull/100)

[Peter Gumm]

sorry, I dont have gzip installed, neither do I know what a "bump" is
I'll try to see whether some other lean tutorial works on my machine ...

[Mauricio Collares]

I think I didn't explain myself too well, sorry! What I mean is that I updated mathlib on my fork of the tutorial (https://github.com/collares/mathematics_in_lean), and you can clone that if you'd like to test whether lake exe cache get works any better. In the future this update will be in the main tutorial too.

[Peter Gumm]

YES ! This worked. Thanks a lot !!