SkySkimmer

(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-R" "." "IsomorphismChecker" "-top" "IsomorphismChecker.test") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 3393 lines to 3304 lines, then from 3318 lines to 3490 lines, then from 3497 lines to 3327 lines, then from 3341 lines to 5219 lines, then from 5221 lines to 3351 lines, then from 3365 lines to 5967 lines, then from 5970 lines to 3356 lines, then from 3370 lines to 3523 lines, then from 3530 lines to 3386 lines, then from 3399 lines to 3384 lines, then from 3399 lines to 3364 lines, then from 3379 lines to 3366 lines, then from 3381 lines to 3364 lines, then from 3379 lines to 3364 lines *)
(* coqc version 9.1+alpha compiled with OCaml 4.14.2
   coqtop version 9.1+alpha
   Expected coqc runtime on this file: 1.603 sec
   Expected coqc peak memory usage on this file: 352512.0 kb *)
Require Ltac2.Ltac2.

Module Export IsomorphismChecker

SkySkimmer

Require Import Wellfounded Relations List.
Import ListNotations.

Arguments slexprod {_ _} _ _ _ _.

Section EmptyRel.
  Definition emptyrel A : relation A := fun _ _ => False.

  Lemma wf_emptyrel A : well_founded (emptyrel A).
  Proof.

SkySkimmer

Require Import Wellfounded Relations List.
Import ListNotations.

Inductive PrefixLt (x: nat): relation (list nat) :=
| p_head (m m': list nat) (n n': nat):
  length (n :: m) <= x ->
  length (n' :: m') <= x ->
  n < n' ->
  PrefixLt x (n :: m) (n' :: m')
| p_tail (m m': list nat) (n n': nat):

SkySkimmer

From iris.algebra Require Export ofe stepindex_finite.

CoInductive stream := SCons {
  head : nat;
  tail : stream;
}.
Add Printing Constructor stream.

Fixpoint nth (s : stream) (n : nat) : nat :=
  match n with

SkySkimmer

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

SkySkimmer

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

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

SkySkimmer

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

    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