Issues setting the lean-training-data repo

Stream: general

[Frederick Pu]

when i run lake exe get cache i get the following error message:

info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git 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'
error: external command 'git' exited with code 128

[Kim Morrison]

lake build -v reveal that the expected commit is missing at quote4

[Kim Morrison]

I've updated the toolchain/mathlib dependency from v4.9.0-rc1 to v4.9.0 (still ancient!) and the problem is resolved.

[Kim Morrison]

I've pushed tags v4.9.0 through v4.16.0 to the lean-training-data repo, making it usable at any of those toolchains (hopefully --- it compiles at least...)

[Frederick Pu]

so i just need to reclone the latest version and it should work fine?

[Kim Morrison]

No need to reclone, just checkout master

[Frederick Pu]

so now get cache is working but declaration_types isn't working

[Frederick Pu]

C:\Users\pufre\Downloads\CodingProjects\lean-training-data>lake exe cache get
Attempting to download 6014 file(s)
Downloaded: 6014 file(s) [attempted 6014/6014 = 100%] (100% success)
Decompressing 6014 file(s)
Unpacked in 36583 ms
Completed successfully!

C:\Users\pufre\Downloads\CodingProjects\lean-training-data>lake exe declaration_types Mathlib
uncaught exception: Could not find native implementation of external declaration 'UInt64.ofNatCore' (symbols 'l_UInt64_ofNatCore___boxed' or 'l_UInt64_ofNatCore').
For declarations from `Init`, `Std`, or `Lean`, you need to set `supportInterpreter := true` in the relevant `lean_exe` statement in your `lakefile.lean`.

[Frederick Pu]

also it seems like goal_comments is looking in the wrong directory:

C:\Users\pufre\Downloads\CodingProjects\lean-training-data>lake exe goal_comments Mathlib.Logic.Hydra
uncaught exception: no such file or directory (error code: 2)
  file: .\.\.lake/packages\mathlib\.lake\build\lib\Mathlib\Logic\Hydra.lean

C:\Users\pufre\Downloads\CodingProjects\lean-training-data>lake exe goal_comments Mathlib.Logic.Pairwise
uncaught exception: no such file or directory (error code: 2)
  file: .\.\.lake/packages\mathlib\.lake\build\lib\Mathlib\Logic\Pairwise.lean

[Kim Morrison]

@Frederick Pu, could you checkout master again and try lake exe declaration_types Mathlib again? I couldn't reproduce your error, but encountered and fixed a different one. It's working for me now.

[Kim Morrison]

I can't reproduce your problem with goal_comments, it is working fine for me.

[Frederick Pu]

PS C:\Users\pufre\Downloads\CodingProjects\lean-training-data> git checkout origin/master
Note: switching to 'origin/master'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by switching back to a branch.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -c with the switch command. Example:

  git switch -c <new-branch-name>

Or undo this operation with:

  git switch -

Turn off this advice by setting config variable advice.detachedHead to false

HEAD is now at bce849f bump to v4.16
PS C:\Users\pufre\Downloads\CodingProjects\lean-training-data> lake exe cache get
No files to download
Decompressing 6014 file(s)
Unpacked in 6964 ms
Completed successfully!
PS C:\Users\pufre\Downloads\CodingProjects\lean-training-data> lake exe declaration_types Mathlib
uncaught exception: Could not find native implementation of external declaration 'UInt64.ofNatCore' (symbols 'l_UInt64_ofNatCore___boxed' or 'l_UInt64_ofNatCore').
For declarations from `Init`, `Std`, or `Lean`, you need to set `supportInterpreter := true` in the relevant `lean_exe` statement in your `lakefile.lean`.
PS C:\Users\pufre\Downloads\CodingProjects\lean-training-data>

[Thomas Zhu]

You need to follow what the error message says, and add supportInterpreter := true to the lakefile.lean. Sorry I am on mobile now, but it would look something like this

[Kim Morrison]

Oh, is this a Windows only issue?

[Kim Morrison]

PR welcome!

[Frederick Pu]

mb this is also a windows only error, since it's a weird windows file path:

PS C:\Users\pufre\Downloads\CodingProjects\lean-training-data> lake exe goal_comments Mathlib.Logic.Hydra
uncaught exception: no such file or directory (error code: 2)
  file: .\.\.lake/packages\mathlib\.lake\build\lib\Mathlib\Logic\Hydra.lean

[Thomas Zhu]

Oh, is this a Windows only issue?

I also got the error message on my Linux server. I don't completely understand the reason but it went away after its suggested fix.

[Frederick Pu]

i switched to wsl and goal_comments runs now but it doesn't seem to be actually adding the goal comments but rather just printing the file:

(base) neuman@Neuman:/mnt/c/Users/pufre/Downloads/CodingProjects/lean-training-data$ lake exe goal_comments Mathlib.Logic.Hydra
info: Version 4.0.0 of elan is available! Use `elan self update` to update.
info: downloading component 'lean'
260.8 MiB / 260.8 MiB (100 %)  47.7 MiB/s ETA:   0 s
info: installing component 'lean'
/-
Copyright (c) 2022 Junyan Xu. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Junyan Xu
-/
import Mathlib.Data.Finsupp.Lex
import Mathlib.Data.Finsupp.Multiset
import Mathlib.Order.GameAdd

/-!
# Termination of a hydra game

This file deals with the following version of the hydra game: each head of the hydra is
labelled by an element in a type `α`, and when you cut off one head with label `a`, it
grows back an arbitrary but finite number of heads, all labelled by elements smaller than
`a` with respect to a well-founded relation `r` on `α`. We show that no matter how (in
what order) you choose cut off the heads, the game always terminates, i.e. all heads will
eventually be cut off (but of course it can last arbitrarily long, i.e. takes an
arbitrary finite number of steps).

This result is stated as the well-foundedness of the `CutExpand` relation defined in
this file: we model the heads of the hydra as a multiset of elements of `α`, and the
valid "moves" of the game are modelled by the relation `CutExpand r` on `Multiset α`:
`CutExpand r s' s` is true iff `s'` is obtained by removing one head `a ∈ s` and
adding back an arbitrary multiset `t` of heads such that all `a' ∈ t` satisfy `r a' a`.

We follow the proof by Peter LeFanu Lumsdaine at https://mathoverflow.net/a/229084/3332.

TODO: formalize the relations corresponding to more powerful (e.g. Kirby–Paris and Buchholz)
hydras, and prove their well-foundedness.
-/


namespace Relation

open Multiset Prod

variable {α : Type*}

/-- The relation that specifies valid moves in our hydra game. `CutExpand r s' s`
  means that `s'` is obtained by removing one head `a ∈ s` and adding back an arbitrary
  multiset `t` of heads such that all `a' ∈ t` satisfy `r a' a`.

  This is most directly translated into `s' = s.erase a + t`, but `Multiset.erase` requires
  `DecidableEq α`, so we use the equivalent condition `s' + {a} = s + t` instead, which
  is also easier to verify for explicit multisets `s'`, `s` and `t`.

  We also don't include the condition `a ∈ s` because `s' + {a} = s + t` already
  guarantees `a ∈ s + t`, and if `r` is irreflexive then `a ∉ t`, which is the
  case when `r` is well-founded, the case we are primarily interested in.

  The lemma `Relation.cutExpand_iff` below converts between this convenient definition
  and the direct translation when `r` is irreflexive. -/
def CutExpand (r : α → α → Prop) (s' s : Multiset α) : Prop :=
  ∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ s' + {a} = s + t

variable {r : α → α → Prop}

theorem cutExpand_le_invImage_lex [DecidableEq α] [IsIrrefl α r] :
    CutExpand r ≤ InvImage (Finsupp.Lex (rᶜ ⊓ (· ≠ ·)) (· < ·)) toFinsupp := by
  rintro s t ⟨u, a, hr, he⟩
  replace hr := fun a' ↦ mt (hr a')
  classical
  refine ⟨a, fun b h ↦ ?_, ?_⟩ <;> simp_rw [toFinsupp_apply]
  · apply_fun count b at he
    simpa only [count_add, count_singleton, if_neg h.2, add_zero, count_eq_zero.2 (hr b h.1)]
      using he
  · apply_fun count a at he
    simp only [count_add, count_singleton_self, count_eq_zero.2 (hr _ (irrefl_of r a)),
      add_zero] at he
    exact he ▸ Nat.lt_succ_self _

theorem cutExpand_singleton {s x} (h : ∀ x' ∈ s, r x' x) : CutExpand r s {x} :=
  ⟨s, x, h, add_comm s _⟩

theorem cutExpand_singleton_singleton {x' x} (h : r x' x) : CutExpand r {x'} {x} :=
  cutExpand_singleton fun a h ↦ by rwa [mem_singleton.1 h]

theorem cutExpand_add_left {t u} (s) : CutExpand r (s + t) (s + u) ↔ CutExpand r t u :=
  exists₂_congr fun _ _ ↦ and_congr Iff.rfl <| by rw [add_assoc, add_assoc, add_left_cancel_iff]

lemma cutExpand_add_right {s' s} (t) : CutExpand r (s' + t) (s + t) ↔ CutExpand r s' s := by
  convert cutExpand_add_left t using 2 <;> apply add_comm

theorem cutExpand_iff [DecidableEq α] [IsIrrefl α r] {s' s : Multiset α} :
    CutExpand r s' s ↔
      ∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t := by
  simp_rw [CutExpand, add_singleton_eq_iff]
  refine exists₂_congr fun t a ↦ ⟨?_, ?_⟩
  · rintro ⟨ht, ha, rfl⟩
    obtain h | h := mem_add.1 ha
    exacts [⟨ht, h, erase_add_left_pos t h⟩, (@irrefl α r _ a (ht a h)).elim]
  · rintro ⟨ht, h, rfl⟩
    exact ⟨ht, mem_add.2 (Or.inl h), (erase_add_left_pos t h).symm⟩

theorem not_cutExpand_zero [IsIrrefl α r] (s) : ¬CutExpand r s 0 := by
  classical
  rw [cutExpand_iff]
  rintro ⟨_, _, _, ⟨⟩, _⟩

lemma cutExpand_zero {x} : CutExpand r 0 {x} := ⟨0, x, nofun, add_comm 0 _⟩

/-- For any relation `r` on `α`, multiset addition `Multiset α × Multiset α → Multiset α` is a
  fibration between the game sum of `CutExpand r` with itself and `CutExpand r` itself. -/
theorem cutExpand_fibration (r : α → α → Prop) :
    Fibration (GameAdd (CutExpand r) (CutExpand r)) (CutExpand r) fun s ↦ s.1 + s.2 := by
  rintro ⟨s₁, s₂⟩ s ⟨t, a, hr, he⟩; dsimp at he ⊢
  classical
  obtain ⟨ha, rfl⟩ := add_singleton_eq_iff.1 he
  rw [add_assoc, mem_add] at ha
  obtain h | h := ha
  · refine ⟨(s₁.erase a + t, s₂), GameAdd.fst ⟨t, a, hr, ?_⟩, ?_⟩
    · rw [add_comm, ← add_assoc, singleton_add, cons_erase h]
    · rw [add_assoc s₁, erase_add_left_pos _ h, add_right_comm, add_assoc]
  · refine ⟨(s₁, (s₂ + t).erase a), GameAdd.snd ⟨t, a, hr, ?_⟩, ?_⟩
    · rw [add_comm, singleton_add, cons_erase h]
    · rw [add_assoc, erase_add_right_pos _ h]
....

[Kim Morrison]

I'm sorry, I don't have availability at the moment to debug this, you may have to work it out yourself.