search

mattam82 / Coq-Equations

A function definition package for Coq
http://mattam82.github.io/Coq-Equations
GNU Lesser General Public License v2.1
223 stars 44 forks source link

Anomaly "in Univ.repr: Universe MetaCoq.SafeChecker.PCUICSafeConversion.12667 undefined." Please report at http://coq.inria.fr/bugs/ #545

Open JasonGross opened 1 year ago

JasonGross commented 1 year ago

@coqbot minimize coq-8.16

#!/usr/bin/env bash
opam install -y coq-equations
git clone https://github.com/JasonGross/metacoq.git --branch=quotation+typingwf
cd metacoq
./configure.sh local
make safechecker TIMED=1 -j2
JasonGross commented 1 year ago

I guess @coqbot isn't listening here, so minimization is running at https://github.com/coq-community/run-coq-bug-minimizer/issues/24

JasonGross commented 1 year ago

@JasonGross, Minimized File /github/workspace/metacoq/safechecker/theories/PCUICSafeConversion.v (full log on GitHub Actions)

Minimized Coq File (consider adding this file to the test-suite) ```coq (* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/metacoq/utils/theories" "MetaCoq.Utils" "-R" "/github/workspace/metacoq/common/theories" "MetaCoq.Common" "-R" "/github/workspace/metacoq/pcuic/theories" "MetaCoq.PCUIC" "-R" "/github/workspace/metacoq/safechecker/theories" "MetaCoq.SafeChecker" "-Q" "/github/workspace/cwd" "Top" "-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/Equations" "Equations" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "MetaCoq.SafeChecker.PCUICSafeConversion") -*- *) (* File reduced by coq-bug-minimizer from original input, then from 5927 lines to 1512 lines, then from 1095 lines to 222 lines, then from 235 lines to 2362 lines, then from 2362 lines to 1248 lines, then from 920 lines to 181 lines, then from 194 lines to 977 lines, then from 982 lines to 198 lines, then from 211 lines to 823 lines, then from 827 lines to 300 lines, then from 313 lines to 861 lines, then from 864 lines to 379 lines, then from 392 lines to 1922 lines, then from 1920 lines to 505 lines, then from 284 lines to 26 lines, then from 39 lines to 1488 lines, then from 1489 lines to 26 lines, then from 39 lines to 901 lines, then from 903 lines to 44 lines, then from 57 lines to 593 lines, then from 598 lines to 45 lines, then from 58 lines to 188 lines, then from 193 lines to 46 lines, then from 59 lines to 369 lines, then from 372 lines to 50 lines, then from 63 lines to 3850 lines, then from 3846 lines to 65 lines, then from 78 lines to 1605 lines, then from 1603 lines to 67 lines, then from 80 lines to 108 lines, then from 113 lines to 69 lines, then from 82 lines to 201 lines, then from 206 lines to 69 lines, then from 82 lines to 632 lines, then from 637 lines to 75 lines, then from 88 lines to 197 lines, then from 202 lines to 78 lines, then from 91 lines to 336 lines, then from 341 lines to 84 lines, then from 97 lines to 276 lines, then from 280 lines to 89 lines, then from 94 lines to 90 lines *) (* coqc version 8.16.1 compiled with OCaml 4.13.1 coqtop version 8.16.1 Expected coqc runtime on this file: 0.225 sec *) Require Coq.Structures.OrderedType. Require Coq.extraction.Extraction. Axiom proof_admitted : False. Tactic Notation "admit" := abstract case proof_admitted. Declare ML Module "equations_plugin:coq-equations.plugin". Variant equations_tag@{} : Set := the_equations_tag. Definition fixproto := the_equations_tag. Register fixproto as equations.fixproto. Definition block := the_equations_tag. Register block as equations.internal.block. Register Init.Logic.True as equations.top.type. Register Init.Logic.I as equations.top.intro. Module Export String. Inductive t : Set := | EmptyString | String (_ : Byte.byte) (_ : t). Notation string := String.t. Record squash (A : Type) : Prop := sq { _ : A }. Notation "∥ T ∥" := (squash T) (at level 10). Import Coq.Lists.SetoidList. Export ListNotations. Notation "#| l |" := (List.length l) (at level 0, l at level 99, format "#| l |"). Module Export All_Forall. Local Set Universe Polymorphism. Local Set Polymorphic Inductive Cumulativity. Inductive All2 {A B : Type} (R : A -> B -> Type) : list A -> list B -> Type := All2_nil : All2 R [] [] | All2_cons : forall (x : A) (y : B) (l : list A) (l' : list B), R x y -> All2 R l l' -> All2 R (x :: l) (y :: l'). Lemma All2_length {A B} {P : A -> B -> Type} {l l'} : All2 P l l' -> #|l| = #|l'|. Admitted. End All_Forall. Definition ident := string. Inductive name : Set := | nAnon | nNamed (_ : ident). Inductive relevance : Set := Relevant | Irrelevant. Record binder_annot (A : Type) := mkBindAnn { binder_name : A; binder_relevance : relevance }. Definition aname := binder_annot name. Record def term := mkdef { dname : aname; dtype : term; dbody : term; rarg : nat }. Definition mfixpoint term := list (def term). Equations isws_cumul_pb_fix_bodies {term fix_kind} (fk : fix_kind) (idx : nat) (mfix1 mfix2 : mfixpoint term) (mfix1' mfix2' : mfixpoint term) (h1 : ∥ All2 (fun u v => True) mfix1 mfix1' ∥) : True by struct mfix2 := isws_cumul_pb_fix_bodies fk idx mfix1 (u :: mfix2) mfix1' (v :: mfix2') h1 := I ; isws_cumul_pb_fix_bodies fk idx mfix1 [] mfix1' [] h1 := I ; isws_cumul_pb_fix_bodies fk idx mfix1 mfix2 mfix1' mfix2' h1 := False_rect _ _. Next Obligation. destruct h1 as [h1]. apply All2_length in h1 as e1. admit. Qed. Next Obligation. admit. Defined. ```
Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted) ```coq ```
Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 120KiB file on GitHub Actions Artifacts under build.log) ``` c MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -R /github/workspace/metacoq/utils/theories MetaCoq.Utils -R /github/workspace/metacoq/common/theories MetaCoq.Common -R /github/workspace/metacoq/pcuic/theories MetaCoq.PCUIC theories/PCUICExpandLetsCorrectness.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.KMGJvXYwDw MINIMIZER_DEBUG: files: theories/PCUICExpandLetsCorrectness.v theories/PCUICProgress.vo (real: 4.99, user: 4.63, sys: 0.34, mem: 859900 ko) COQC theories/PCUICFirstorder.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/metacoq/pcuic MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -R /github/workspace/metacoq/utils/theories MetaCoq.Utils -R /github/workspace/metacoq/common/theories MetaCoq.Common -R /github/workspace/metacoq/pcuic/theories MetaCoq.PCUIC theories/PCUICFirstorder.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.Rgykq3iS5b MINIMIZER_DEBUG: files: theories/PCUICFirstorder.v theories/PCUICFirstorder.vo (real: 4.67, user: 4.36, sys: 0.30, mem: 852412 ko) COQC theories/PCUICNormalization.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/metacoq/pcuic MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -R /github/workspace/metacoq/utils/theories MetaCoq.Utils -R /github/workspace/metacoq/common/theories MetaCoq.Common -R /github/workspace/metacoq/pcuic/theories MetaCoq.PCUIC theories/PCUICNormalization.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.tDiudtdfYq MINIMIZER_DEBUG: files: theories/PCUICNormalization.v theories/PCUICNormalization.vo (real: 2.14, user: 1.86, sys: 0.24, mem: 846968 ko) COQC theories/PCUICConsistency.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/metacoq/pcuic MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -R /github/workspace/metacoq/utils/theories MetaCoq.Utils -R /github/workspace/metacoq/common/theories MetaCoq.Common -R /github/workspace/metacoq/pcuic/theories MetaCoq.PCUIC theories/PCUICConsistency.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.Yp609R2VO0 MINIMIZER_DEBUG: files: theories/PCUICConsistency.v theories/PCUICConsistency.vo (real: 1.65, user: 1.37, sys: 0.28, mem: 846332 ko) theories/PCUICExpandLetsCorrectness.vo (real: 39.48, user: 39.05, sys: 0.37, mem: 1153108 ko) MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/metacoq/pcuic MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --print-version MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.YF6L2ob2lu MINIMIZER_DEBUG: files: make[2]: Leaving directory '/github/workspace/metacoq/pcuic' make[1]: Leaving directory '/github/workspace/metacoq/pcuic' make -C safechecker make[1]: Entering directory '/github/workspace/metacoq/safechecker' cat metacoq-config > _CoqProject cat _CoqProject.in >> _CoqProject coq_makefile -f _CoqProject -o Makefile.safechecker Warning: ../utils/theories (used in -R or -Q) is not a subdirectory of the current directory make -f Makefile.safechecker make[2]: Entering directory '/github/workspace/metacoq/safechecker' MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/metacoq/safechecker MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --print-version MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.PuXJZfFUKr MINIMIZER_DEBUG: files: COQDEP VFILES MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/metacoq/safechecker MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --print-version MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.l9YAtmZM6k MINIMIZER_DEBUG: files: MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/metacoq/safechecker MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --print-version MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.LzsKTE0qkR MINIMIZER_DEBUG: files: MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/metacoq/safechecker MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --print-version MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.isCOVKLzX5 MINIMIZER_DEBUG: files: COQC theories/PCUICEqualityDec.v COQC theories/PCUICErrors.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/metacoq/safechecker MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/metacoq/safechecker MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -R /github/workspace/metacoq/utils/theories MetaCoq.Utils -R /github/workspace/metacoq/common/theories MetaCoq.Common -R /github/workspace/metacoq/pcuic/theories MetaCoq.PCUIC -R /github/workspace/metacoq/safechecker/theories MetaCoq.SafeChecker theories/PCUICEqualityDec.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.544xXmiQOZ MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -R /github/workspace/metacoq/utils/theories MetaCoq.Utils -R /github/workspace/metacoq/common/theories MetaCoq.Common -R /github/workspace/metacoq/pcuic/theories MetaCoq.PCUIC -R /github/workspace/metacoq/safechecker/theories MetaCoq.SafeChecker theories/PCUICErrors.v MINIMIZER_DEBUG: files: theories/PCUICEqualityDec.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.IYTR8gWo1m MINIMIZER_DEBUG: files: theories/PCUICErrors.v theories/PCUICErrors.vo (real: 1.88, user: 1.59, sys: 0.25, mem: 755924 ko) COQC theories/PCUICSafeConversion.v MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/metacoq/safechecker MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -R /github/workspace/metacoq/utils/theories MetaCoq.Utils -R /github/workspace/metacoq/common/theories MetaCoq.Common -R /github/workspace/metacoq/pcuic/theories MetaCoq.PCUIC -R /github/workspace/metacoq/safechecker/theories MetaCoq.SafeChecker theories/PCUICSafeConversion.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.ANnkHV4iXe MINIMIZER_DEBUG: files: theories/PCUICSafeConversion.v File "./theories/PCUICSafeConversion.v", line 277, characters 0-8: Error: Anomaly "in Univ.repr: Universe MetaCoq.SafeChecker.PCUICSafeConversion.108 undefined." Please report at http://coq.inria.fr/bugs/. Command exited with non-zero status 129 theories/PCUICSafeConversion.vo (real: 1.72, user: 1.42, sys: 0.28, mem: 833360 ko) make[3]: *** [Makefile.safechecker:793: theories/PCUICSafeConversion.vo] Error 129 make[3]: *** Waiting for unfinished jobs.... theories/PCUICEqualityDec.vo (real: 12.39, user: 12.00, sys: 0.36, mem: 1000808 ko) make[2]: *** [Makefile.safechecker:409: all] Error 2 make[2]: Leaving directory '/github/workspace/metacoq/safechecker' make[1]: *** [Makefile:11: theory] Error 2 make[1]: Leaving directory '/github/workspace/metacoq/safechecker' make: *** [Makefile:137: safechecker] Error 2 ```
Minimization Log (truncated to last 8.0KiB; full 571KiB file on GitHub Actions Artifacts under bug.log) ``` tag was not found in the current environment. Intermediate code not saved. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-fatal error: Failed to remove non-instance definitions and preserve the error. The new error was: File "/tmp/tmppx1s9lcu/MetaCoq/SafeChecker/PCUICSafeConversion.v", line 8, characters 23-40: Error: The reference the_equations_tag was not found in the current environment. Intermediate code not saved. I will now attempt to remove unused variables  Variable removal successful. I will now attempt to remove unused contexts  Context removal successful. I will now attempt to replace Obligation with Admit Obligations Non-fatal error: Failed to admit Obligations and preserve the error. The new error was: File "/tmp/tmpsrw2h5ce/MetaCoq/SafeChecker/PCUICSafeConversion.v", line 80, characters 0-18: Error: Recursive definition of isws_cumul_pb_fix_bodies is ill-formed. In environment isws_cumul_pb_fix_bodies : forall term fix_kind : Type, fix_kind -> nat -> forall mfix1 : mfixpoint term, mfixpoint term -> forall mfix1' : mfixpoint term, mfixpoint term -> ∥ All2 (fun _ _ : def term => True) mfix1 mfix1' ∥ -> True term : Type fix_kind : Type fk : fix_kind idx : nat mfix1 : mfixpoint term mfix2 : mfixpoint term mfix1' : mfixpoint term mfix2' : mfixpoint term h1 : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1' ∥ d : def term l : list (def term) mfix1'0 := mfix1' : mfixpoint term mfix2'0 := mfix2' : mfixpoint term h0 := h1 : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1'0 ∥ h2 := h0 : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1'0 ∥ Recursive call to isws_cumul_pb_fix_bodies has not enough arguments. Recursive definition is: "fun (term fix_kind : Type) (fk : fix_kind) (idx : nat) (mfix1 mfix2 mfix1' mfix2' : mfixpoint term) (h1 : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1' ∥) => match mfix2 with | [] => fun (mfix1'0 mfix2'0 : mfixpoint term) (h2 : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1'0 ∥) => match mfix2'0 with | [] => fun _ : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1'0 ∥ => I | d :: l => fun h3 : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1'0 ∥ => False_rect True (isws_cumul_pb_fix_bodies_obligations_obligation_1 isws_cumul_pb_fix_bodies term fix_kind fk idx mfix1 mfix1'0 d l h3) end h2 | d :: l => fun (mfix1'0 mfix2'0 : mfixpoint term) (h2 : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1'0 ∥) => match mfix2'0 with | [] => fun h3 : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1'0 ∥ => False_rect True (isws_cumul_pb_fix_bodies_obligations_obligation_2 isws_cumul_pb_fix_bodies term fix_kind fk idx mfix1 d l mfix1'0 h3) | _ :: _ => fun _ : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1'0 ∥ => I end h2 end mfix1' mfix2' h1". Intermediate code not saved. Failed to do everything at once; trying one at a time. Admitting Obligations unsuccessful. No successful changes. I will now attempt to admit lemmas with Admitted  Admitting lemmas successful. Failed to do everything at once; trying one at a time. Admitting lemmas unsuccessful. No successful changes. I will now attempt to admit definitions with Admitted Non-fatal error: Failed to admit definitions and preserve the error. The new error was: File "/tmp/tmpjvog165s/MetaCoq/SafeChecker/PCUICSafeConversion.v", line 84, characters 0-9: Error: Recursive definition of isws_cumul_pb_fix_bodies is ill-formed. In environment isws_cumul_pb_fix_bodies : forall term fix_kind : Type, fix_kind -> nat -> forall mfix1 : mfixpoint term, mfixpoint term -> forall mfix1' : mfixpoint term, mfixpoint term -> ∥ All2 (fun _ _ : def term => True) mfix1 mfix1' ∥ -> True term : Type fix_kind : Type fk : fix_kind idx : nat mfix1 : mfixpoint term mfix2 : mfixpoint term mfix1' : mfixpoint term mfix2' : mfixpoint term h1 : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1' ∥ d : def term l : list (def term) mfix1'0 := mfix1' : mfixpoint term mfix2'0 := mfix2' : mfixpoint term h0 := h1 : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1'0 ∥ h2 := h0 : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1'0 ∥ Recursive call to isws_cumul_pb_fix_bodies has not enough arguments. Recursive definition is: "fun (term fix_kind : Type) (fk : fix_kind) (idx : nat) (mfix1 mfix2 mfix1' mfix2' : mfixpoint term) (h1 : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1' ∥) => match mfix2 with | [] => fun (mfix1'0 mfix2'0 : mfixpoint term) (h2 : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1'0 ∥) => match mfix2'0 with | [] => fun _ : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1'0 ∥ => I | d :: l => fun h3 : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1'0 ∥ => False_rect True (isws_cumul_pb_fix_bodies_obligations_obligation_1 isws_cumul_pb_fix_bodies term fix_kind fk idx mfix1 mfix1'0 d l h3) end h2 | d :: l => fun (mfix1'0 mfix2'0 : mfixpoint term) (h2 : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1'0 ∥) => match mfix2'0 with | [] => fun h3 : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1'0 ∥ => False_rect True (isws_cumul_pb_fix_bodies_obligations_obligation_2 isws_cumul_pb_fix_bodies term fix_kind fk idx mfix1 d l mfix1'0 h3) | _ :: _ => fun _ : ∥ All2 (fun _ _ : def term => True) mfix1 mfix1'0 ∥ => I end h2 end mfix1' mfix2' h1". Intermediate code not saved. Failed to do everything at once; trying one at a time. Admitting definitions unsuccessful. No successful changes. I will now attempt to admit lemmas with admit. Defined  Admitting lemmas successful. Failed to do everything at once; trying one at a time. Admitting lemmas unsuccessful. No successful changes. I will now attempt to admit definitions with admit. Defined Non-fatal error: Failed to admit definitions and preserve the error. The new error was: File "/tmp/tmpa7sz8l6d/MetaCoq/SafeChecker/PCUICSafeConversion.v", line 86, characters 0-8: Error: not found in table: equations.equality.type Intermediate code not saved. Failed to do everything at once; trying one at a time. Admitting definitions unsuccessful. No successful changes. I will now attempt to export modules Module exportation unsuccessful. I will now attempt to split imports and exports Import/Export splitting unsuccessful. I will now attempt to split := definitions One-line definition splitting unsuccessful. I will now attempt to remove all lines, one at a time Line removal unsuccessful. I will now attempt to remove goals ending in [Abort.]  Aborted removal successful. I will now attempt to remove unused Ltacs  Ltac removal successful. I will now attempt to remove unused definitions Non-fatal error: Failed to remove definitions and preserve the error. The new error was: File "/tmp/tmppx1s9lcu/MetaCoq/SafeChecker/PCUICSafeConversion.v", line 8, characters 23-40: Error: The reference the_equations_tag was not found in the current environment. Intermediate code not saved. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-fatal error: Failed to remove non-instance definitions and preserve the error. The new error was: File "/tmp/tmppx1s9lcu/MetaCoq/SafeChecker/PCUICSafeConversion.v", line 8, characters 23-40: Error: The reference the_equations_tag was not found in the current environment. Intermediate code not saved. I will now attempt to remove unused variables  Variable removal successful. I will now attempt to remove unused contexts  Context removal successful. I will now attempt to remove empty sections No empty sections to remove. Now, I will attempt to strip repeated newlines and trailing spaces from this file... No strippable newlines or spaces. ```

If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross). If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.

Originally posted by @coqbot in https://github.com/coq-community/run-coq-bug-minimizer/issues/24#issuecomment-1500756531