❌ Build Failed: MCMC

Project build failed

📋 View command log (YAML)

Full Build Log

✔ [3340/3362] Built MCMC.PF.Combinatorics.Quiver.Cyclic (2.6s)
✔ [3341/3362] Built MCMC.PF.Topology.Compactness.ExtremeValueUSC (3.1s)
✔ [3342/3362] Built MCMC.PF.Data.List (3.4s)
✖ [3343/3362] Building MCMC.PF.LinearAlgebra.Matrix.Spectrum (4.4s)
trace: .> LEAN_PATH=/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/packages/Cli/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/packages/batteries/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/packages/Qq/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/packages/aesop/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/packages/importGraph/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/packages/plausible/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/packages/mathlib/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/build/lib/lean /home/nfr/.elan/toolchains/leanprover--lean4---v4.29.0/bin/lean /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/MCMC/PF/LinearAlgebra/Matrix/Spectrum.lean -o /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/build/lib/lean/MCMC/PF/LinearAlgebra/Matrix/Spectrum.olean -i /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/build/lib/lean/MCMC/PF/LinearAlgebra/Matrix/Spectrum.ilean -c /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/build/ir/MCMC/PF/LinearAlgebra/Matrix/Spectrum.c --setup /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/build/ir/MCMC/PF/LinearAlgebra/Matrix/Spectrum.setup.json --json
error: MCMC/PF/LinearAlgebra/Matrix/Spectrum.lean:143:2: Type mismatch
  _root_.isCompact_stdSimplex n
has type
  ∀ (ι : Type ?u.257.2) [inst : Fintype ι] [inst_1 : TopologicalSpace n] [inst_2 : Semiring n] [inst_3 : PartialOrder n]
    [OrderClosedTopology n] [ContinuousAdd n] [CompactIccSpace n] [IsOrderedAddMonoid n], IsCompact (stdSimplex n ι)
but is expected to have type
  IsCompact (stdSimplex ℝ n)
warning: MCMC/PF/LinearAlgebra/Matrix/Spectrum.lean:443:4: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
warning: MCMC/PF/LinearAlgebra/Matrix/Spectrum.lean:635:4: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
warning: MCMC/PF/LinearAlgebra/Matrix/Spectrum.lean:657:2: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
error: Lean exited with code 1
✖ [3346/3362] Building MCMC.PF.Combinatorics.Quiver.Path (4.0s)
trace: .> LEAN_PATH=/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/packages/Cli/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/packages/batteries/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/packages/Qq/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/packages/aesop/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/packages/importGraph/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/packages/plausible/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/packages/mathlib/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/build/lib/lean /home/nfr/.elan/toolchains/leanprover--lean4---v4.29.0/bin/lean /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/MCMC/PF/Combinatorics/Quiver/Path.lean -o /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/build/lib/lean/MCMC/PF/Combinatorics/Quiver/Path.olean -i /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/build/lib/lean/MCMC/PF/Combinatorics/Quiver/Path.ilean -c /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/build/ir/MCMC/PF/Combinatorics/Quiver/Path.c --setup /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MCMC/.lake/build/ir/MCMC/PF/Combinatorics/Quiver/Path.setup.json --json
warning: MCMC/PF/Combinatorics/Quiver/Path.lean:305:0: Definition `Quiver.inducedQuiver` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
warning: MCMC/PF/Combinatorics/Quiver/Path.lean:315:17: instance `Quiver.inducedQuiver` must be marked with `@[reducible]` or `@[implicit_reducible]`
warning: MCMC/PF/Combinatorics/Quiver/Path.lean:536:2: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
error: MCMC/PF/Combinatorics/Quiver/Path.lean:628:39: unsolved goals
V : Type u_1
inst✝¹ : Quiver V
inst✝ : DecidableEq V
a b x b✝ : V
pPrev : Path a b✝
ih : x ∈ pPrev.vertices → ∃ p₁ p₂, pPrev = p₁.comp p₂ ∧ x ∉ p₂.vertices.tail
e : b✝ ⟶ x
hx : x ∈ (pPrev.cons e).vertices
hx' : x ∈ pPrev.vertices ∨ x = (pPrev.cons e).end
⊢ pPrev.comp e.toPath = (pPrev.comp e.toPath).comp nil
error: MCMC/PF/Combinatorics/Quiver/Path.lean:629:13: `simp` made no progress
error: MCMC/PF/Combinatorics/Quiver/Path.lean:647:12: Type mismatch: After simplification, term
  hmem
 has type
  x ∈ q₂'.vertices.tail
but is expected to have type
  x ∈ (q₂.vertices.dropLast ++ [b✝, c✝]).tail
warning: MCMC/PF/Combinatorics/Quiver/Path.lean:628:74: This simp argument is unused:
  comp_nil

Hint: Omit it from the simp argument list.
  simp only [cons_eq_comp_toPath,̵ ̵c̵o̵m̵p̵_̵n̵i̵l̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: MCMC/PF/Combinatorics/Quiver/Path.lean:935:4: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
error: Lean exited with code 1
Some required targets logged failures:
- MCMC.PF.LinearAlgebra.Matrix.Spectrum
- MCMC.PF.Combinatorics.Quiver.Path
error: build failed

← Back to Summary