Anomaly "in Univ.repr: Universe MetaCoq.SafeChecker.PCUICSafeConversion.12667 undefined." Please report at http://coq.inria.fr/bugs/ #545
Comments
|
I guess @coqbot isn't listening here, so minimization is running at coq-community/run-coq-bug-minimizer#24 |
This was referenced Apr 5, 2023
|
@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)(* -*- 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)Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 120KiB file on GitHub Actions Artifacts under
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
@coqbot minimize coq-8.16
The text was updated successfully, but these errors were encountered: