SkySkimmer

    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

   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

(* 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

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

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

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/

SkySkimmer

(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-noinit" "-indices-matter" "-type-in-type" "-w" "-notation-overridden" "-w" "-deprecated-native-compiler-option" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/UniMath/UniMath" "UniMath" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "UniMath.CategoryTheory.LeftKanExtension" "-native-compiler" "no") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 688 lines to 71 lines, then from 84 lines to 800 lines, then from 799 lines to 123 lines, then from 136 lines to 646 lines, then from 650 lines to 171 lines, then from 184 lines to 570 lines, then from 572 lines to 204 lines, then from 217 lines to 880 lines, then from 884 lines to 284 lines, then from 297 lines to 626 lines, then from 630 lines to 328 lines, then from 341 lines to 1806 lines, then from 1797 lines to 365 lines, then from 375 lines to 363 lines, then from 3

SkySkimmer

(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-noinit" "-indices-matter" "-type-in-type" "-w" "-notation-overridden" "-w" "-deprecated-native-compiler-option" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/UniMath/UniMath" "UniMath" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "UniMath.CategoryTheory.LeftKanExtension" "-native-compiler" "no") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 688 lines to 71 lines, then from 84 lines to 800 lines, then from 799 lines to 123 lines, then from 136 lines to 646 lines, then from 650 lines to 171 lines, then from 184 lines to 570 lines, then from 572 lines to 204 lines, then from 217 lines to 880 lines, then from 884 lines to 284 lines, then from 297 lines to 626 lines, then from 630 lines to 328 lines, then from 341 lines to 1806 lines, then from 1797 lines to 365 lines, then from 375 lines to 363 lines, then from 3

SkySkimmer

(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-noinit" "-indices-matter" "-type-in-type" "-w" "-notation-overridden" "-w" "-deprecated-native-compiler-option" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/UniMath/UniMath" "UniMath" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "UniMath.CategoryTheory.LeftKanExtension" "-native-compiler" "no") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 688 lines to 71 lines, then from 84 lines to 800 lines, then from 799 lines to 123 lines, then from 136 lines to 646 lines, then from 650 lines to 171 lines, then from 184 lines to 570 lines, then from 572 lines to 204 lines, then from 217 lines to 880 lines, then from 884 lines to 284 lines, then from 297 lines to 626 lines, then from 630 lines to 328 lines, then from 341 lines to 1806 lines, then from 1797 lines to 365 lines *)
(* coqc version 8.18+alpha compiled with OC

SkySkimmer

Package: firefox-skyskimmer-patches
Version: 1.0
Section: custom
Priority: optional
Architecture: all
Essential: no
Maintainer: skyskimmer.net
Depends: zip, unzip, sed, coreutils
Description: Patch firefox post-install
  - disable clickselectsall behaviour in address bar