Last active
May 6, 2025 18:58
-
-
Save pogin503/fb5e5305bc29a9475a9da78787a6b765 to your computer and use it in GitHub Desktop.
GroundZero log
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| PS D:\repo\github.com\forked-from-1kasper\ground_zero_2> make | |
| lake script run updateIndex | |
| info: GroundZero: no previous manifest, creating one from scratch | |
| info: toolchain not updated; already up-to-date | |
| lake build | |
| ⚠ [50/96] Built GroundZero.Exercises.Chap2 | |
| warning: .\.\.\.\GroundZero\Exercises\Chap2.lean:204:15: declaration uses 'sorry' | |
| ✖ [51/96] Building GroundZero.Theorems.Nat | |
| trace: .> LEAN_PATH=.\.\.lake\build\lib\lean d:\.local\share\elan\toolchains\leanprover--lean4---v4.18.0\bin\lean.exe -Dlinter.deprecated=false -Dlinter.unusedVariables=false -DrelaxedAutoImplicit=false -DautoImplicit=false .\.\.\.\GroundZero\Theorems\Nat.lean -R .\.\.\. -o .\.\.lake\build\lib\lean\GroundZero\Theorems\Nat.olean -i .\.\.lake\build\lib\lean\GroundZero\Theorems\Nat.ilean -c .\.\.lake\build\ir\GroundZero\Theorems\Nat.c --json | |
| error: Lean exited with code 3221225477 | |
| Some required builds logged failures: | |
| - GroundZero.Theorems.Nat | |
| error: build failed | |
| make: *** [library] Error 1 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| PS D:\repo\github.com\forked-from-1kasper\ground_zero_2> elan override set leanprover/lean4:nightly | |
| info: override toolchain for 'D:\repo\github.com\forked-from-1kasper\ground_zero_2' set to 'leanprover/lean4-nightly:nightly-2025-05-06' | |
| PS D:\repo\github.com\forked-from-1kasper\ground_zero_2> make clean; make | |
| lake clean | |
| lake script run updateIndex | |
| lake build | |
| ✖ [2/96] Building GroundZero.Meta.HottTheory | |
| trace: .> LEAN_PATH=D:\repo\github.com\forked-from-1kasper\ground_zero_2\.lake\build\lib\lean d:\.local\share\elan\toolchains\leanprover--lean4-nightly---nightly-2025-05-06\bin\lean.exe -Dlinter.deprecated=false -Dlinter.unusedVariables=false -DrelaxedAutoImplicit=false -DautoImplicit=false D:\repo\github.com\forked-from-1kasper\ground_zero_2\GroundZero\Meta\HottTheory.lean -R D:\repo\github.com\forked-from-1kasper\ground_zero_2 -o D:\repo\github.com\forked-from-1kasper\ground_zero_2\.lake\build\lib\lean\GroundZero\Meta\HottTheory.olean -i D:\repo\github.com\forked-from-1kasper\ground_zero_2\.lake\build\lib\lean\GroundZero\Meta\HottTheory.ilean -c D:\repo\github.com\forked-from-1kasper\ground_zero_2\.lake\build\ir\GroundZero\Meta\HottTheory.c --json | |
| error: D:\repo\github.com\forked-from-1kasper\ground_zero_2\GroundZero\Meta\HottTheory.lean:312:56: application type mismatch | |
| Core.instantiateTypeLevelParams implFnDecl | |
| argument | |
| implFnDecl | |
| has type | |
| ConstantInfo : Type | |
| but is expected to have type | |
| ConstantVal : Type | |
| error: Lean exited with code 1 | |
| Some required builds logged failures: | |
| - GroundZero.Meta.HottTheory | |
| error: build failed | |
| make: *** [library] Error 1 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| $ git diff . | |
| diff --git a/GroundZero/Meta/HottTheory.lean b/GroundZero/Meta/HottTheory.lean | |
| index e3d766c..fb6adb7 100644 | |
| --- a/GroundZero/Meta/HottTheory.lean | |
| +++ b/GroundZero/Meta/HottTheory.lean | |
| @@ -309,7 +309,7 @@ def abbrevAttrs : Array Attribute := | |
| let implOfType := implOfDecl.type | |
| let implFnType ← implOfDecl.levelParams.map mkLevelParam | |
| - |> Core.instantiateTypeLevelParams implFnDecl | |
| + |> Core.instantiateTypeLevelParams (implFnDecl.toConstantVal) | |
| |> liftCoreM; |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| PS D:\repo\github.com\forked-from-1kasper\ground_zero> make clean; make | |
| lake clean | |
| lake script run updateIndex | |
| lake build | |
| ✖ [42/96] Building GroundZero.Theorems.Univalence | |
| trace: .> LEAN_PATH=D:\repo\github.com\forked-from-1kasper\ground_zero\.lake\build\lib\lean d:\.local\share\elan\toolchains\leanprover--lean4-nightly---nightly-2025-05-06\bin\lean.exe -Dlinter.deprecated=false -Dlinter.unusedVariables=false -DrelaxedAutoImplicit=false -DautoImplicit=false D:\repo\github.com\forked-from-1kasper\ground_zero\GroundZero\Theorems\Univalence.lean -R D:\repo\github.com\forked-from-1kasper\ground_zero -o D:\repo\github.com\forked-from-1kasper\ground_zero\.lake\build\lib\lean\GroundZero\Theorems\Univalence.olean -i D:\repo\github.com\forked-from-1kasper\ground_zero\.lake\build\lib\lean\GroundZero\Theorems\Univalence.ilean -c D:\repo\github.com\forked-from-1kasper\ground_zero\.lake\build\ir\GroundZero\Theorems\Univalence.c --json | |
| error: D:\repo\github.com\forked-from-1kasper\ground_zero\GroundZero\Theorems\Univalence.lean:201:14: 'unreachable' code was reached | |
| error: Lean exited with code 1 | |
| Some required builds logged failures: | |
| - GroundZero.Theorems.Univalence | |
| error: build failed | |
| make: *** [library] Error 1 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -- error location | |
| hott exercise boolEquivEqvBool : (𝟐 ≃ 𝟐) ≃ 𝟐 := | |
| begin | |
| existsi boolDecode; fapply Qinv.toBiinv; existsi boolEncode; apply Prod.mk; | |
| { intro x; induction x using Bool.casesOn <;> reflexivity }; | |
| { intro ⟨φ, H⟩; apply equivHmtpyLem; intro x; | |
| match boolEqTotal (φ false), boolEqTotal (φ true) with | |
| | Sum.inl p₁, Sum.inl q₁ => { apply explode; apply ffNeqTt; | |
| apply eqvInj ⟨φ, H⟩; exact p₁ ⬝ q₁⁻¹ } | |
| | Sum.inr p₂, Sum.inl q₁ => { transitivity; apply ap (boolEncode · x); apply p₂; | |
| symmetry; induction x using Bool.casesOn <;> assumption } | |
| | Sum.inl p₁, Sum.inr q₂ => { transitivity; apply ap (boolEncode · x); apply p₁; | |
| symmetry; induction x using Bool.casesOn <;> assumption } | |
| | Sum.inr p₂, Sum.inr q₂ => { apply explode; apply ffNeqTt; | |
| apply eqvInj ⟨φ, H⟩; exact p₂ ⬝ q₂⁻¹ } } | |
| end |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| pogin503@DESKTOP-66Q50RC ~/g/g/f/ground_zero (master)> nix profile install nixpkgs#lean4 | |
| pogin503@DESKTOP-66Q50RC ~/g/g/f/ground_zero (master)> lake build | |
| ✖ [45/96] Building GroundZero.Theorems.Univalence | |
| trace: .> LEAN_PATH=././.lake/build/lib/lean /nix/store/hm1l63wb1fz28d8kryvl3c36sl5wbs0h-lean4-4.18.0/bin/lean -Dlinter.deprecated=false -Dlinter.unusedVariables=false -DrelaxedAutoImplicit=false -DautoImplicit=false ././././GroundZero/Theorems/Univalence.lean -R ./././. -o ././.lake/build/lib/lean/GroundZero/Theorems/Univalence.olean -i ././.lake/build/lib/lean/GroundZero/Theorems/Univalence.ilean -c ././.lake/build/ir/GroundZero/Theorems/Univalence.c --json | |
| error: Lean exited with code 139 | |
| Some required builds logged failures: | |
| - GroundZero.Theorems.Univalence | |
| error: build failed |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment