(base) stepannesterov@DN0a221534 Lean % git clone https://github.com/stepan2698-cpu/Stepan-s-mathlib4-fork.git
Cloning into 'Stepan-s-mathlib4-fork'...
remote: Enumerating objects: 451532, done.
remote: Counting objects: 100% (320/320), done.
remote: Compressing objects: 100% (264/264), done.
remote: Total 451532 (delta 173), reused 56 (delta 56), pack-reused 451212 (from 3)
Receiving objects: 100% (451532/451532), 296.32 MiB | 1.70 MiB/s, done.
Resolving deltas: 100% (370505/370505), done.
(base) stepannesterov@DN0a221534 Lean % lake exe cache get
info: downloading https://releases.lean-lang.org/lean4/v4.27.0/lean-4.27.0-darwin.tar.zst
Total: 476.2 MiB Speed:  23.3 MiB/s
info: installing /Users/stepannesterov/.elan/toolchains/leanprover--lean4---v4.27.0
error: [root]: no configuration file with a supported extension:
/Users/stepannesterov/Lean/lakefile.lean
/Users/stepannesterov/Lean/lakefile.toml
(base) stepannesterov@DN0a221534 Lean % cd Stepan-s-mathlib4-fork
(base) stepannesterov@DN0a221534 Stepan-s-mathlib4-fork % lake exe cache get
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '7311586e1a56af887b1081d05e80c11b6c41d212'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '5ce7f0a355f522a952a3d678d696bd563bb4fd28'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '14107dc03e4540e534621b3af3804c06dfd480f1'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision 'f08e838d4f9aea519f3cde06260cfb686fd4bab0'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '23324752757bf28124a518ec284044c8db79fee5'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision 'f0440aecee888582922e892d573b8726c09a1f6f'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '28e0856d4424863a85b18f38868c5420c55f9bae'
✖ [10/22] Building Batteries.Data.Array.Match
trace: .> LEAN_PATH=/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/Cli/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/Qq/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/aesop/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/importGraph/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/plausible/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/build/lib/lean /Users/stepannesterov/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/bin/lean /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/Batteries/Data/Array/Match.lean -o /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Match.olean -i /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Match.ilean -c /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.c --setup /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.setup.json --json
error: Batteries/Data/Array/Match.lean:138:2: `Rel` is not a field of structure `FinitenessRelation`
error: Batteries/Data/Array/Match.lean:137:44: Fields missing: `rel`

Field `rel` must be explicitly provided; its synthesized value is
  InvImage IterM.IsPlausibleSuccessorOf ?m.18
error: Batteries/Data/Array/Match.lean:146:6: failed to synthesize
  Iterator ?m.19 ?m.20 ?m.21

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
error: Batteries/Data/Array/Match.lean:154:10: failed to synthesize
  Iterator ?m.19 ?m.20 ?m.21

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
error: Batteries/Data/Array/Match.lean:162:10: failed to synthesize
  Iterator ?m.19 ?m.20 ?m.21

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
error: Lean exited with code 1
Some required targets logged failures:
- Batteries.Data.Array.Match
error: build failed