Changing mathlib version and a couple questions

[AG161]

Is there an easy way to change the version of mathlib4 in lean-training-data to a fork or different commit for mathlib? Right now the library automatically installs the particular commit of mathlib specified in the lake-manifest. I made a fork of lean-training-data where I adjust lake-manifest.json and lakefile.lean to try to get around this:

https://github.com/AG161/lean-training-data/blob/master/lake-manifest.json https://github.com/AG161/lean-training-data/blob/master/lakefile.lean

I matched the dependencies in lake-manifest to the those of the commit of mathlib4 that I forked, but I get the following error:

lake exe training_data Mathlib.Logic.Hydra
info: [87/167] Building Std.Tactic.Simpa
info: [113/167] Building Std.Tactic.SimpTrace
error: > LEAN_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./build/lib DYLD_LIBRARY_PATH=./lake-packages/std/build/lib /Users/agittis/.elan/toolchains/leanprover--lean4---v4.2.0-rc1/bin/lean -Dlinter.missingDocs=true -DwarningAsError=true ./lake-packages/std/././Std/Tactic/SimpTrace.lean -R ./lake-packages/std/./. -o ./lake-packages/std/build/lib/Std/Tactic/SimpTrace.olean -i ./lake-packages/std/build/lib/Std/Tactic/SimpTrace.ilean -c ./lake-packages/std/build/ir/Std/Tactic/SimpTrace.c
error: stdout:
./lake-packages/std/././Std/Tactic/SimpTrace.lean:51:6: error: function expected at
  Origin.decl declName
term has type
  Origin
./lake-packages/std/././Std/Tactic/SimpTrace.lean:72:12: error: failed to synthesize instance
  HAppend (Array (TSyntax `Lean.Parser.Tactic.simpStar)) (Array (TSyntax `Lean.Parser.Tactic.simpLemma))
    (Array (TSyntax `Lean.Parser.Tactic.simpStar))
error: external command `/Users/agittis/.elan/toolchains/leanprover--lean4---v4.2.0-rc1/bin/lean` exited with code 1
error: > LEAN_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./build/lib DYLD_LIBRARY_PATH=./lake-packages/std/build/lib /Users/agittis/.elan/toolchains/leanprover--lean4---v4.2.0-rc1/bin/lean -Dlinter.missingDocs=true -DwarningAsError=true ./lake-packages/std/././Std/Tactic/Simpa.lean -R ./lake-packages/std/./. -o ./lake-packages/std/build/lib/Std/Tactic/Simpa.olean -i ./lake-packages/std/build/lib/Std/Tactic/Simpa.ilean -c ./lake-packages/std/build/ir/Std/Tactic/Simpa.c
error: stdout:
./lake-packages/std/././Std/Tactic/Simpa.lean:74:6: error: function expected at
  Origin.decl declName
term has type
  Origin
./lake-packages/std/././Std/Tactic/Simpa.lean:103:12: error: failed to synthesize instance
  HAppend (Array (TSyntax `Lean.Parser.Tactic.simpStar)) (Array (TSyntax `Lean.Parser.Tactic.simpLemma))
    (Array (TSyntax `Lean.Parser.Tactic.simpStar))
error: external command `/Users/agittis/.elan/toolchains/leanprover--lean4---v4.2.0-rc1/bin/lean` exited with code 1
agittis@Andreass-MacBook-Pro lean-training-data % 

Is there a straightforward way to adjust the mathlib version? This is the really the main issue I'd like to figure out. I also noticed a couple other things which I have listed below, but they are not important for what I'd like to use the tool for, so feel free to ignore.

1. When I run lake exe goal_comments Mathlib.Logic.Hydra I get the following output for theorem _root_.Acc.cutExpand:

/-- A singleton `{a}` is accessible under `CutExpand r` if `a` is accessible under `r`,
  assuming `r` is irreflexive. -/
theorem _root_.Acc.cutExpand [IsIrrefl α r] {a : α} (hacc : Acc r a) : Acc (CutExpand r) {a} := by
  induction' hacc with a h ih
  -- ⊢ Acc (CutExpand r) {a}
  refine' Acc.intro _ fun s ↦ _
  -- ⊢ CutExpand r s {a} → Acc (CutExpand r) s
  classical
  simp only [cutExpand_iff, mem_singleton]
  rintro ⟨t, a, hr, rfl, rfl⟩
  refine' acc_of_singleton fun a' ↦ _
  rw [erase_singleton, zero_add]
  exact ih a' ∘ hr a'
#align acc.cut_expand Acc.cutExpand

It looks like the classical tactic caused goal comments to stop being printed, not sure if this is intended behavior for certain tactics.

2. In the documentation for declaration_types (and premises) it sounds like you can focus them to specific files: "For each declaration imported in the target file (e.g. Mathlib), print the name and type of the declaration." Here I took the "(e.g. Mathlib)" to mean I could put specific files in the arguments. However when I run lake exe declaration_types Mathlib.Logic.Hydra it seems to be printing all of mathlib, or at least more than just the Hydra file. Is there supposed to be a way to focus these commands to specific files?

3.) Finally, a very small point it looks like there is a typo in the https://github.com/semorrison/lean-training-data#training_data section where it says lake exe export_infotree Mathlib.Logic.Hydra instead of lake exe training_data Mathlib.Logic.Hydra.

Thanks for making this tool!