Gaëtan Gilbert SkySkimmer
SkySkimmer
/ coq-rewriter-perf-SuperFast.NEW.opam_install.1.stdout.log
Created
December 20, 2024 12:27
This file contains 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
| The following actions will be performed: | |
| ∗ install coq-rewriter-perf-SuperFast dev | |
| <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> | |
| Processing 1/3: [coq-rewriter-perf-SuperFast.dev: git] | |
| ⬇ retrieved coq-rewriter-perf-SuperFast.dev (git+https://github.com/mit-plv/rewriter.git#master) | |
| Processing 2/3: [coq-rewriter-perf-SuperFast: make perf-SuperFast] | |
| + /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/dev/bench/wrapper.sh "make" "-j1" "perf-SuperFast" "EXTERNAL_PERF_DEPENDENCIES=1" "TIMED=1" (CWD=/home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-rewriter-perf-SuperFast.dev) | |
| - sed 's?@META@?src/Rewriter/Util/plugins/META.coq-rewriter?g' _CoqProject.in > _CoqProject | |
| - echo $COQ_VERSION_INFO (9.0+alpha) > .coq-version |
This file contains 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
| Fixpoint add n m := | |
| match n with | |
| | 0 => m | |
| | S p => S (p + m) | |
| end | |
| where "n + m" := (add n m) : nat_scope. | |
| Fixpoint mul n m := | |
| match n with |
SkySkimmer
/ tmp.v
Last active
September 18, 2024 13:28
This file contains 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
| (* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-noinit" "-indices-matter" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/theories" "HoTT" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/contrib" "HoTT.Contrib" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/test" "HoTT.Tests" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "Top.bug_01") -*- *) | |
| (* File reduced by coq-bug-minimizer from original input, then from 231 lines to 38 lines, then from 51 lines to 162 lines, then from 167 lines to 41 lines, then from 54 lines to 475 lines, then from 480 lines to 42 lines, then from 55 lines to 133 lines, then from 138 lines to 42 lines, then from 55 lines to 453 lines, then from 458 lines to 82 lines, then from 95 lines to 780 lines, then from 780 lines to 164 lines, then from 177 lines to 2432 lines, then from 2435 lines |
This file contains 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
| Inductive T := | |
| | C1 (_ _ : T) | |
| | C2 (_ _ : T). | |
| Set Debug "hcons-before-hconstr". | |
| (* or run coqchk on the result *) | |
| Lemma foo (x y:T) : {x=y} + {x<>y}. | |
| Proof. | |
| decide equality. |
SkySkimmer
/ gist:43aa1e57830665d9fabafc25726e21d1
Created
June 8, 2024 18:12
This file contains 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
| After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) | |
| ---------------------------------------------------------------------------------------------------------------------------------------------------------------------- | |
| 25m41.61s | 1425064 ko | Total Time / Peak Mem | 29m52.84s | 1315000 ko || -4m11.23s || 110064 ko | -14.01% | +8.36% | |
| ---------------------------------------------------------------------------------------------------------------------------------------------------------------------- | |
| 0m39.43s | 426784 ko | success/Nsatz.chk.log | 0m59.31s | 426000 ko || -0m19.88s || 784 ko | -33.51% | +0.18% | |
| 0m37.07s | 598040 ko | success/Nsatz.v.log | 0m54.66s | 575288 ko || -0m17.59s || 22752 ko | -32.18% | +3.95% | |
| 1m30.49s | 685560 ko |
SkySkimmer
/ both.log
Created
June 2, 2024 17:24
This file contains 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
| After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) | |
| --------------------------------------------------------------------------------------------------------------------------------------------------------------------- | |
| 9m32.98s | 2254440 ko | Total Time / Peak Mem | 10m11.28s | 2633980 ko || -0m38.30s || -379540 ko | -6.26% | -14.40% | |
| --------------------------------------------------------------------------------------------------------------------------------------------------------------------- | |
| 1m06.34s | 796208 ko | stm/Nijmegen_QArithSternBrocot_Zaux.v.log | 1m04.59s | 800772 ko || +0m01.75s || -4564 ko | +2.70% | -0.56% | |
| 0m22.18s | 348940 ko | bugs/bug_7675_3.v.log | 0m22.26s | 346336 ko || -0m00.08s || 2604 ko | -0.35% | +0.75% | |
| 0m17.20s | 620080 ko | succ |
SkySkimmer
/ tac2core.ml
Created
May 28, 2024 12:44
This file contains 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
| (* next to constr_in_context *) | |
| let () = | |
| define "constr_in_context_alt" (ident @-> constr @-> closure @-> tac constr) @@ fun id t c -> | |
| Proofview.Goal.goals >>= function | |
| | [gl] -> | |
| gl >>= fun gl -> | |
| let env = Proofview.Goal.env gl in | |
| let sigma = Proofview.Goal.sigma gl in | |
| let has_var = |
SkySkimmer
/ after
Last active
April 23, 2024 12:17
HoTT theories/ vo file sizes before / after using callback to substitute univ instances in VM (in bytes)
This file contains 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
| 90136317 total | |
| 7585417 ./Spaces/Torus/TorusEquivCircles.vo | |
| 4570944 ./Pointed/Core.vo | |
| 4353756 ./Homotopy/CayleyDickson.vo | |
| 3429253 ./Colimits/Sequential.vo | |
| 3414226 ./Spaces/Spheres.vo | |
| 3363757 ./Colimits/Colimit_Flattening.vo | |
| 3004861 ./Cubical/PathCube.vo | |
| 2570380 ./Homotopy/Syllepsis.vo | |
| 1323781 ./Algebra/Groups/FreeProduct.vo |
SkySkimmer
/ allwarn
Last active
April 15, 2024 11:43
This file contains 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
| File "./theories/Logic/ExtensionalityFacts.v", line 95, characters 0-4: | |
| Warning: Adding constraints to the global env from Qed body: | |
| FunctExt_iff_EqDeltaProjs.u1 <= Delta.u0 | |
| FunctExt_iff_EqDeltaProjs.u1 <= diagonal_projs_same_behavior.u0 | |
| FunctExt_iff_EqDeltaProjs.u1 <= FunctExt_iff_EqDeltaProjs.u0 | |
| FunctExt_iff_EqDeltaProjs.u1 = FunctExt_iff_EqDeltaProjs.u2 | |
| [private-mono,fragile,default] | |
| File "./theories/Logic/ExtensionalityFacts.v", line 104, characters 0-4: | |
| Warning: Adding constraints to the global env from Qed body: | |
| FunctExt_UniqInverse.u2 <= FunctExt_UniqInverse.u1 |
SkySkimmer
/ list
Created
June 8, 2023 10:20
This file contains 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
| 695 opam.NEW/ocaml-NEW/.opam-switch/build/coq-unimath.dev/UniMath/Tactics/EnsureStructuredProofs.v.prof.json.gz | |
| 718 opam.NEW/ocaml-NEW/.opam-switch/build/coq-engine-bench-lite.dev/coq/PerformanceExperiments/Ltac2Compat/Array.v.prof.json.gz | |
| 720 opam.NEW/ocaml-NEW/.opam-switch/build/coq-performance-tests-lite.dev/PerformanceExperiments/Ltac2Compat/Array.v.prof.json.gz | |
| 748 opam.NEW/ocaml-NEW/.opam-switch/build/coq-engine-bench-lite.dev/coq/PerformanceDemos/evar_creation.v.prof.json.gz | |
| 919 opam.NEW/ocaml-NEW/.opam-switch/build/coq-rewriter-perf-SuperFast.dev/src/Rewriter/Util/Tactics/Test.v.prof.json.gz | |
| 924 opam.NEW/ocaml-NEW/.opam-switch/build/coq-fiat-crypto-with-bedrock.dev/src/Util/Tactics/Test.v.prof.json.gz | |
| 926 opam.NEW/ocaml-NEW/.opam-switch/build/coq-rewriter.dev/src/Rewriter/Util/Tactics/Test.v.prof.json.gz | |
| 939 opam.NEW/ocaml-NEW/.opam-switch/build/coq-performance-tests-lite.dev/PerformanceExperiments/Reify/OCamlReify.v.prof.json.gz | |
| 951 opam.NEW/ocaml-NEW/.opam-switch/build/coq-engine-bench-lite.dev/coq/ |
NewerOlder