Option to internalize a qualid passed to an Ltac as a constr with its impargs #20682
Conversation
This file contains hidden or 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
5181e99 to
7031535
Compare
2 tasks
|
🔴 CI failures at commit 7031535 without any failure in the test-suite ✔️ Corresponding jobs for the base commit f38be3d succeeded ❔ Ask me to try to extract minimal test cases that can be added to the test-suite 🏃
|
|
@coqbot ci minimize |
|
I have initiated minimization at commit 7031535 for the suggested targets ci-compcert, ci-metarocq as requested. |
|
🔴 CI failures at commit 7031535 without any failure in the test-suite ✔️ Corresponding jobs for the base commit f38be3d succeeded ❔ Ask me to try to extract minimal test cases that can be added to the test-suite 🏃
|
|
Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/compcert/backend/Unusedglobproof.v in 4h 11m 28s (from ci-compcert) (full log on GitHub Actions - verbose log) We are collecting data on the user experience of the Coq Bug Minimizer. 🌟 Minimized Coq File (consider adding this file to the test-suite)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-native-compiler" "no" "-w" "-undeclared-scope" "-w" "-omega-is-deprecated" "-coqlib" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq//" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/compcert/lib" "compcert.lib" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/compcert/common" "compcert.common" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/compcert/x86_32" "compcert.x86_32" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/compcert/x86" "compcert.x86" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/compcert/backend" "compcert.backend" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/compcert/cfrontend" "compcert.cfrontend" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/compcert/driver" "compcert.driver" "-R" "/github/workspace/builds/coq/coq-failing/
8000
_build_ci/compcert/cparser" "compcert.cparser" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/compcert/export" "compcert.export" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Flocq" "Flocq" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/MenhirLib" "MenhirLib" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Stdlib" "Stdlib" "-top" "compcert.backend.Unusedglobproof") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 1454 lines to 35 lines, then from 48 lines to 1082 lines, then from 1087 lines to 63 lines, then from 76 lines to 569 lines, then from 574 lines to 63 lines, then from 76 lines to 327 lines, then from 332 lines to 64 lines, then from 77 lines to 676 lines, then from 681 lines to 68 lines, then from 81 lines to 1377 lines, then from 1380 lines to 168 lines, then from 181 lines to 1338 lines, then from 1343 lines to 281 lines, then from 294 lines to 2110 lines, then from 2115 lines to 285 lines, then from 298 lines to 5637 lines, then from 5640 lines to 314 lines, then from 327 lines to 721 lines, then from 726 lines to 314 lines, then from 327 lines to 1394 lines, then from 1399 lines to 319 lines, then from 332 lines to 4481 lines, then from 4486 lines to 333 lines, then from 346 lines to 1946 lines, then from 1951 lines to 340 lines, then from 353 lines to 596 lines, then from 601 lines to 340 lines, then from 353 lines to 1406 lines, then from 1408 lines to 340 lines, then from 353 lines to 1041 lines, then from 1046 lines to 345 lines, then from 358 lines to 2323 lines, then from 2324 lines to 348 lines, then from 361 lines to 759 lines, then from 759 lines to 384 lines, then from 397 lines to 778 lines, then from 783 lines to 385 lines, then from 398 lines to 2673 lines, then from 2676 lines to 448 lines, then from 461 lines to 958 lines, then from 958 lines to 509 lines, then from 522 lines to 917 lines, then from 920 lines to 603 lines, then from 616 lines to 922 lines, then from 923 lines to 698 lines, then from 711 lines to 1788 lines, then from 1791 lines to 711 lines, then from 724 lines to 739 lines, then from 744 lines to 710 lines, then from 723 lines to 738 lines, then from 743 lines to 709 lines, then from 722 lines to 1122 lines, then from 1127 lines to 762 lines, then from 775 lines to 790 lines, then from 795 lines to 761 lines, then from 766 lines to 763 lines *)
(* coqc version 9.1+alpha compiled with OCaml 4.14.2
coqtop version runner-t7b1znuaq-project-4504-concurrent-2:/builds/coq/coq/_build/default,(HEAD detached at cdd06d0a2f356e) (cdd06d0a2f356e0c02e2d20356562b7deae4cf15)
Expected coqc runtime on this file: 0.291 sec *)
Require Corelib.Classes.RelationClasses.
Require Corelib.Floats.SpecFloat.
Export Corelib.BinNums.PosDef.
Module Export BinPosDef.
Local Open Scope positive_scope.
Module Export Pos.
Include BinNums.PosDef.Pos.
Definition t := positive.
Infix "?=" := compare (at level 70, no associativity) : positive_scope.
Local Notation ten := 1~0~1~0.
Fixpoint of_uint_acc (d:Decimal.uint)(acc:positive) :=
match d with
| Decimal.Nil => acc
| Decimal.D0 l => of_uint_acc l (mul ten acc)
| Decimal.D1 l => of_uint_acc l (add 1 (mul ten acc))
| Decimal.D2 l => of_uint_acc l (add 1~0 (mul ten acc))
| Decimal.D3 l => of_uint_acc l (add 1~1 (mul ten acc))
| Decimal.D4 l => of_uint_acc l (add 1~0~0 (mul ten acc))
| Decimal.D5 l => of_uint_acc l (add 1~0~1 (mul ten acc))
| Decimal.D6 l => of_uint_acc l (add 1~1~0 (mul ten acc))
| Decimal.D7 l => of_uint_acc l (add 1~1~1 (mul ten acc))
| Decimal.D8 l => of_uint_acc l (add 1~0~0~0 (mul ten acc))
| Decimal.D9 l => of_uint_acc l (add 1~0~0~1 (mul ten acc))
end.
Fixpoint of_uint (d:Decimal.uint) : N.
exact (match d with
| Decimal.Nil => N0
| Decimal.D0 l => of_uint l
| Decimal.D1 l => Npos (of_uint_acc l 1)
| Decimal.D2 l => Npos (of_uint_acc l 1~0)
| Decimal.D3 l => Npos (of_uint_acc l 1~1)
| Decimal.D4 l => Npos (of_uint_acc l 1~0~0)
| Decimal.D5 l => Npos (of_uint_acc l 1~0~1)
| Decimal.D6 l => Npos (of_uint_acc l 1~1~0)
| Decimal.D7 l => Npos (of_uint_acc l 1~1~1)
| Decimal.D8 l => Npos (of_uint_acc l 1~0~0~0)
| Decimal.D9 l => Npos (of_uint_acc l 1~0~0~1)
end).
Defined.
Fixpoint of_hex_uint (d:Hexadecimal.uint) : N.
Admitted.
Fixpoint to_little_uint p :=
match p with
| 1 => Decimal.D1 Decimal.Nil
| p~1 => Decimal.Little.succ_double (to_little_uint p)
| p~0 => Decimal.Little.double (to_little_uint p)
end.
Definition to_uint p := Decimal.rev (to_little_uint p).
End Pos.
Export Corelib.Program.Basics.
Export Corelib.Classes.RelationClasses.
Module Export Stdlib_DOT_Bool_DOT_Bool_WRAPPED.
Module Export Bool.
Definition eqb (b1 b2:bool) : bool.
Admitted.
Open Scope bool_scope.
End Bool.
Module Export Stdlib.
Module Export Bool.
Module Export Bool.
Include Stdlib_DOT_Bool_DOT_Bool_WRAPPED.Bool.
End Bool.
Module Type Typ.
Parameter Inline(10) t : Type.
End Typ.
Module Type HasEq (Import T:Typ).
Parameter Inline(30) eq : t -> t -> Prop.
End HasEq.
Module Type Eq := Typ <+ HasEq.
Module Type EqNotation (Import E:Eq).
Infix "==" := eq (at level 70, no associativity).
End EqNotation.
Module Type Eq' := Eq <+ EqNotation.
Module Type IsEq (Import E:Eq).
#[global]
Declare Instance eq_equiv : Equivalence eq.
End IsEq.
Module Type IsEqOrig (Import E:Eq').
End IsEqOrig.
Module Type HasEqDec (Import E:Eq').
Parameter eq_dec : forall x y : t, { x==y } + { ~ x==y }.
End HasEqDec.
Module Type HasEqb (Import T:Typ).
End HasEqb.
Module Type EqbSpec (T:Typ)(X:HasEq T)(Y:HasEqb T).
End EqbSpec.
Module Type EqbNotation (T:Typ)(E:HasEqb T).
End EqbNotation.
Module Type HasEqBool (E:Eq) := HasEqb E <+ EqbSpec E E.
Module Type EqualityType := Eq <+ IsEq.
Module Type EqualityTypeOrig := Eq <+ IsEqOrig.
Module Type EqualityTypeBoth <: EqualityType <: EqualityTypeOrig
:= Eq <+ IsEq <+ IsEqOrig.
Module Type DecidableType <: EqualityType
:= Eq <+ IsEq <+ HasEqDec.
Module Type DecidableTypeOrig <: EqualityTypeOrig
:= Eq <+ IsEqOrig <+ HasEqDec.
Module Type DecidableTypeBoth <: DecidableType <: DecidableTypeOrig
:= EqualityTypeBoth <+ HasEqDec.
Module Type BooleanEqualityType <: EqualityType
:= Eq <+ IsEq <+ HasEqBool.
Module Type BooleanDecidableType <: DecidableType <: BooleanEqualityType
:= Eq <+ IsEq <+ HasEqDec <+ HasEqBool.
Module Type DecidableTypeFull <: DecidableTypeBoth <: BooleanDecidableType
:= Eq <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool.
Module Type BooleanEqualityType' :=
BooleanEqualityType <+ EqNotation <+ EqbNotation.
Module BackportEq (E:Eq)(F:IsEq E) <: IsEqOrig E.
End BackportEq.
Module UpdateEq (E:Eq)(F:IsEqOrig E) <: IsEq E.
#[global]
Instance eq_equiv : Equivalence E.eq.
Admitted.
End UpdateEq.
Module HasEqDec2Bool (E:Eq)(F:HasEqDec E) <: HasEqBool E.
End HasEqDec2Bool.
Module HasEqBool2Dec (E:Eq)(F:HasEqBool E) <: HasEqDec E.
Lemma eq_dec : forall x y, {E.eq x y}+{~E.eq x y}.
Admitted.
End HasEqBool2Dec.
Module BoolEqualityFacts (Import E : BooleanEqualityType').
End BoolEqualityFacts.
Module Type HasUsualEq (Import T:Typ) <: HasEq T.
Definition eq := @Logic.eq t.
End HasUsualEq.
Module Type UsualEq <: Eq := Typ <+ HasUsualEq.
Module Type UsualIsEq (E:UsualEq) <: IsEq E.
Definition eq_equiv : Equivalence E.eq.
Admitted.
End UsualIsEq.
Module Type UsualIsEqOrig (E:UsualEq) <: IsEqOrig E.
End UsualIsEqOrig.
Module Type UsualEqualityType <: EqualityType
:= UsualEq <+ UsualIsEq.
Module Type UsualDecidableType <: DecidableType
:= UsualEq <+ UsualIsEq <+ HasEqDec.
Module Type UsualDecidableTypeFull <: DecidableTypeFull
:= UsualEq <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqDec <+ HasEqBool.
Module Type HasLt (Import T:Typ).
Parameter Inline(40) lt : t -> t -> Prop.
End HasLt.
Module Type HasLe (Import T:Typ).
Parameter Inline(40) le : t -> t -> Prop.
End HasLe.
Module Type EqLt := Typ <+ HasEq <+ HasLt.
Module Type EqLe := Typ <+ HasEq <+ HasLe.
Module Type EqLtLe := Typ <+ HasEq <+ HasLt <+ HasLe.
Module Type LtNotation (E:EqLt).
Infix "<" := E.lt.
End LtNotation.
Module Type LeNotation (E:EqLe).
End LeNotation.
Module Type LtLeNotation (E:EqLtLe).
End LtLeNotation.
Module Type EqLtNotation (E:EqLt) := EqNotation E <+ LtNotation E.
Module Type EqLtLeNotation (E:EqLtLe) := EqNotation E <+ LtLeNotation E.
Module Type EqLt' := EqLt <+ EqLtNotation.
Module Type EqLtLe' := EqLtLe <+ EqLtLeNotation.
Module Type IsStrOrder (Import E:EqLt).
End IsStrOrder.
Module Type LeIsLtEq (Import E:EqLtLe').
End LeIsLtEq.
Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder.
Module Type HasCmp (Import T:Typ).
Parameter Inline compare : t -> t -> comparison.
End HasCmp.
Module Type CmpNotation (T:Typ)(C:HasCmp T).
End CmpNotation.
Module Type CmpSpec (Import E:EqLt')(Import C:HasCmp E).
End CmpSpec.
Module Type HasCompare (E:EqLt) := HasCmp E <+ CmpSpec E.
Module Type DecStrOrder := StrOrder <+ HasCompare.
Module Type DecStrOrder' := DecStrOrder <+ EqLtNotation <+ CmpNotation.
Module Type OrderedType <: DecidableType := DecStrOrder <+ HasEqDec.
Module Type OrderedType' := OrderedType <+ EqLtNotation <+ CmpNotation.
Module Type OrderedTypeFull := OrderedType <+ HasLe <+ LeIsLtEq.
Module Type OrderedTypeFull' :=
OrderedTypeFull <+ EqLtLeNotation <+ CmpNotation.
Module Type UsualStrOrder := UsualEqualityType <+ HasLt <+ IsStrOrder.
Module Type UsualDecStrOrder := UsualStrOrder <+ HasCompare.
Module Type UsualOrderedType <: UsualDecidableType <: OrderedType
:= UsualDecStrOrder <+ HasEqDec.
Module Type UsualOrderedTypeFull := UsualOrderedType <+ HasLe <+ LeIsLtEq.
Module Type LtIsTotal (Import E:EqLt').
End LtIsTotal.
Module Type TotalOrder := StrOrder <+ HasLe <+ LeIsLtEq <+ LtIsTotal.
Module Compare2EqBool (Import O:DecStrOrder') <: HasEqBool O.
End Compare2EqBool.
Module OT_to_Full (O:OrderedType') <: OrderedTypeFull.
Include O.
Definition le x y := x<y \/ x==y.
End OT_to_Full.
Module OTF_LtIsTotal (Import O:OrderedTypeFull') <: LtIsTotal O.
End OTF_LtIsTotal.
Local Coercion is_true : bool >-> Sortclass.
Module Type HasLeb (Import T:Typ).
Parameter Inline leb : t -> t -> bool.
End HasLeb.
Module Type HasLtb (Import T:Typ).
End HasLtb.
Module Type LebNotation (T:Typ)(E:HasLeb T).
Infix "<=?" := E.leb (at level 70, no associativity).
End LebNotation.
Module Type LtbNotation (T:Typ)(E:HasLtb T).
End LtbNotation.
Module Type LebSpec (T:Typ)(X:HasLe T)(Y:HasLeb T).
End LebSpec.
Module Type LtbSpec (T:Typ)(X:HasLt T)(Y:HasLtb T).
End LtbSpec.
Module Type LeBool := Typ <+ HasLeb.
Module Type LeBool' := LeBool <+ LebNotation.
Module Type LebIsTotal (Import X:LeBool').
End LebIsTotal.
Module Type TotalLeBool := LeBool <+ LebIsTotal.
Module Type TotalLeBool' := LeBool' <+ LebIsTotal.
Module Type LebIsTransitive (Import X:LeBool').
End LebIsTransitive.
Module Type TotalTransitiveLeBool := TotalLeBool <+ LebIsTransitive.
Module Type TotalTransitiveLeBool' := TotalLeBool' <+ LebIsTransitive.
Module OTF_to_TTLB (Import O : OrderedTypeFull') <: TotalTransitiveLeBool.
Definition leb x y :=
match compare x y with Gt => false | _ => true end.
Definition t := t.
End OTF_to_TTLB.
Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull.
Definition t := t.
Definition le x y : Prop := x <=? y.
Definition eq x y : Prop := le x y /\ le y x.
Definition lt x y : Prop := le x y /\ ~le y x.
Definition compare x y :=
if x <=? y then (if y <=? x then Eq else Lt) else Gt.
Include HasEqBool2Dec.
#[global]
Instance eq_equiv : Equivalence eq.
Admitted.
End TTLB_to_OTF.
Module Type CompareFacts (Import O:DecStrOrder').
End CompareFacts.
Module OrderedTypeFullFacts (Import O:OrderedTypeFull').
End OrderedTypeFullFacts.
Module OrderedTypeFacts (Import O: OrderedType').
End OrderedTypeFacts.
Module OrderedTypeTest (Import O:OrderedType').
End OrderedTypeTest.
Module OrderedTypeRev (O:OrderedTypeFull) <: OrderedTypeFull.
Definition t := O.t.
Definition eq := O.eq.
#[global]
Program Instance eq_equiv : Equivalence eq.
Definition eq_dec := O.eq_dec.
Definition lt := flip O.lt.
Definition le := flip O.le.
Definition compare := flip O.compare.
End OrderedTypeRev.
Module Pos
<: UsualOrderedTypeFull
<: UsualDecidableTypeFull
<: TotalOrder.
Include BinPosDef.Pos.
Definition eq := @Logic.eq positive.
Definition eq_equiv := @eq_equivalence positive.
Definition lt x y := (x ?= y) = Lt.
Definition le x y := (x ?= y) <> Gt.
Lemma eq_dec : forall x y:positive, {x = y} + {x <> y}.
Admitted.
End Pos.
Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).
Local Notation "0" := Z0.
Include BinNums.IntDef.Z.
Notation pos := Zpos.
Notation neg := Zneg.
Definition of_uint (d:Decimal.uint) := of_N (Pos.of_uint d).
Definition of_hex_uint (d:Hexadecimal.uint) := of_N (Pos.of_hex_uint d).
Definition of_int (d:Decimal.int) :=
match d with
| Decimal.Pos d => of_uint d
| Decimal.Neg d => opp (of_uint d)
end.
Definition of_hex_int (d:Hexadecimal.int) :=
match d with
| Hexadecimal.Pos d => of_hex_uint d
| Hexadecimal.Neg d => opp (of_hex_uint d)
end.
Definition of_num_int (d:Number.int) :=
match d with
| Number.IntDecimal d => of_int d
| Number.IntHexadecimal d => of_hex_int d
end.
Definition to_int n :=
match n with
| 0 => Decimal.Pos Decimal.zero
| pos p => Decimal.Pos (Pos.to_uint p)
| neg p => Decimal.Neg (Pos.to_uint p)
end.
Definition to_num_int n := Number.IntDecimal (to_int n).
Number Notation Z of_num_int to_num_int : Z_scope.
Local Open Scope Z_scope.
Notation "x < y < z" := (x < y /\ y < z) : Z_scope.
Inductive string : Set :=
| EmptyString : string
| String : ascii -> string -> string.
Export Stdlib.Bool.Bool.
Ltac inv H := inversion H; clear H; subst.
Definition zeq: forall (x y: Z), {x = y} + {x <> y}.
Admitted.
Section Binary.
Variable prec emax : Z.
Notation bounded := (SpecFloat.bounded prec emax).
Inductive binary_float :=
| B754_zero (s : bool)
| B754_infinity (s : bool)
| B754_nan : binary_float
| B754_finite (s : bool) (m : positive) (e : Z) :
bounded m e = true -> binary_float.
End Binary.
Definition binary32 := binary_float 24 128.
Definition binary64 := binary_float 53 1024.
Module Type WORDSIZE.
End WORDSIZE.
Module Make(WS: WORDSIZE).
Definition modulus : Z.
Admitted.
Record int: Type := mkint { intval: Z; intrange: -1 < intval < modulus }.
End Make.
Module Export Wordsize_64.
End Wordsize_64.
Module Export Int64.
Include Make(Wordsize_64).
Notation int64 := Int64.int.
Module Export Wordsize_Ptrofs.
End Wordsize_Ptrofs.
Module Export Ptrofs.
Include Make(Wordsize_Ptrofs).
Notation ptrofs := Ptrofs.int.
Definition float := binary64.
Definition float32 := binary32.
Module Export AST.
Set Implicit Arguments.
Definition ident := positive.
Inductive typ : Type :=
| Tint
| Tfloat
| Tlong
| Tsingle
| Tany32
| Tany64.
Inductive xtype : Type :=
| Xbool
| Xint8signed
| Xint8unsigned
| Xint16signed
| Xint16unsigned
| Xint
| Xfloat
| Xlong
| Xsingle
| Xptr
| Xany32
| Xany64
| Xvoid.
Record calling_convention : Type := mkcallconv {
cc_vararg: option Z;
cc_unproto: bool;
cc_structret: bool
}.
Record signature : Type := mksignature {
sig_args: list xtype;
sig_res: xtype;
sig_cc: calling_convention
}.
Inductive memory_chunk : Type :=
| Mbool
| Mint8signed
| Mint8unsigned
| Mint16signed
| Mint16unsigned
| Mint32
| Mint64
| Mfloat32
| Mfloat64
| Many32
| Many64.
Inductive init_data: Type :=
| Init_int8: int -> init_data
| Init_int16: int -> init_data
| Init_int32: int -> init_data
| Init_int64: int64 -> init_data
| Init_float32: float32 -> init_data
| Init_float64: float -> init_data
| Init_space: Z -> init_data
| Init_addrof: ident -> ptrofs -> init_data.
Fixpoint init_data_list_size (il: list init_data) {struct il} : Z.
Admitted.
Record globvar (V: Type) : Type := mkglobvar {
gvar_info: V;
gvar_init: list init_data;
gvar_readonly: bool;
gvar_volatile: bool
}.
Inductive globdef (F V: Type) : Type :=
| Gfun (f: F)
| Gvar (v: globvar V).
Arguments Gfun [F V].
Arguments Gvar [F V].
Inductive external_function : Type :=
| EF_external (name: string) (sg: signature)
| EF_builtin (name: string) (sg: signature)
| EF_runtime (name: string) (sg: signature)
| EF_vload (chunk: memory_chunk)
| EF_vstore (chunk: memory_chunk)
| EF_malloc
| EF_free
| EF_memcpy (sz: Z) (al: Z)
| EF_annot (kind: positive) (text: string) (targs: list typ)
| EF_annot_val (kind: positive) (text: string) (targ: typ)
| EF_inline_asm (text: string) (sg: signature) (clobbers: list string)
| EF_debug (kind: positive) (text: ident) (targs: list typ).
Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} + {ef1<>ef2}.
Admitted.
Inductive fundef (F: Type): Type :=
| Internal: F -> fundef F
| External: external_function -> fundef F.
Arguments External [F].
Class Linker (A: Type) := {
link: A -> A -> option A;
linkorder: A -> A -> Prop;
linkorder_refl: forall x, linkorder x x;
linkorder_trans: forall x y z, linkorder x y -> linkorder y z -> linkorder x z;
link_linkorder: forall x y z, link x y = Some z -> linkorder x z /\ linkorder y z
}.
Definition link_fundef {F: Type} (fd1 fd2: fundef F) :=
match fd1, fd2 with
| Internal _, Internal _ => None
| External ef1, External ef2 =>
if external_function_eq ef1 ef2 then Some (External ef1) else None
| Internal f, External ef =>
match ef with EF_external id sg => Some (Internal f) | _ => None end
| External ef, Internal f =>
match ef with EF_external id sg => Some (Internal f) | _ => None end
end.
Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop :=
| linkorder_fundef_refl: forall fd, linkorder_fundef fd fd
| linkorder_fundef_ext_int: forall f id sg, linkorder_fundef (External (EF_external id sg)) (Internal f).
Global Program Instance Linker_fundef (F: Type): Linker (fundef F) := {
link := link_fundef;
linkorder := linkorder_fundef
}.
Inductive init_class : list init_data -> Type :=
| Init_extern: init_class nil
| Init_common: forall sz, init_class (Init_space sz :: nil)
| Init_definitive: forall il, init_class il.
Definition classify_init (i: list init_data) : init_class i.
Admitted.
Definition link_varinit (i1 i2: list init_data) :=
match classify_init i1, classify_init i2 with
| Init_extern, _ => Some i2
| _, Init_extern => Some i1
| Init_common sz1, _ => if zeq sz1 (init_data_list_size i2) then Some i2 else None
| _, Init_common sz2 => if zeq sz2 (init_data_list_size i1) then Some i1 else None
| _, _ => None
end.
Inductive linkorder_varinit: list init_data -> list init_data -> Prop :=
|
8000
linkorder_varinit_refl: forall il, linkorder_varinit il il
| linkorder_varinit_extern: forall il, linkorder_varinit nil il
| linkorder_varinit_common: forall sz il,
il <> nil -> init_data_list_size il = sz ->
linkorder_varinit (Init_space sz :: nil) il.
Global Program Instance Linker_varinit : Linker (list init_data) := {
link := link_varinit;
linkorder := linkorder_varinit
}.
Admit Obligations.
Definition link_vardef {V: Type} {LV: Linker V} (v1 v2: globvar V) :=
match link v1.(gvar_info) v2.(gvar_info) with
| None => None
| Some info =>
match link v1.(gvar_init) v2.(gvar_init) with
| None => None
| Some init =>
if eqb v1.(gvar_readonly) v2.(gvar_readonly)
&& eqb v1.(gvar_volatile) v2.(gvar_volatile)
then Some {| gvar_info := info; gvar_init := init;
gvar_readonly := v1.(gvar_readonly);
gvar_volatile := v1.(gvar_volatile) |}
else None
end
end.
Inductive linkorder_vardef {V: Type} {LV: Linker V}: globvar V -> globvar V -> Prop :=
| linkorder_vardef_intro: forall info1 info2 i1 i2 ro vo,
linkorder info1 info2 ->
linkorder i1 i2 ->
linkorder_vardef (mkglobvar info1 i1 ro vo) (mkglobvar info2 i2 ro vo).
Global Program Instance Linker_vardef (V: Type) {LV: Linker V}: Linker (globvar V) := {
link := link_vardef;
linkorder := linkorder_vardef
}.
Admit Obligations.
Global Program Instance Linker_unit: Linker unit := {
link := fun x y => Some tt;
linkorder := fun x y => True
}.
Definition link_def {F V: Type} {LF: Linker F} {LV: Linker V} (gd1 gd2: globdef F V) :=
match gd1, gd2 with
| Gfun f1, Gfun f2 =>
match link f1 f2 with Some f => Some (Gfun f) | None => None end
| Gvar v1, Gvar v2 =>
match link v1 v2 with Some v => Some (Gvar v) | None => None end
| _, _ => None
end.
Inductive linkorder_def {F V: Type} {LF: Linker F} {LV: Linker V}: globdef F V -> globdef F V -> Prop :=
| linkorder_def_fun: forall fd1 fd2,
linkorder fd1 fd2 ->
linkorder_def (Gfun fd1) (Gfun fd2)
| linkorder_def_var: forall v1 v2,
linkorder v1 v2 ->
linkorder_def (Gvar v1) (Gvar v2).
Global Program Instance Linker_def (F V: Type) {LF: Linker F} {LV: Linker V}: Linker (globdef F V) := {
link := link_def;
linkorder := linkorder_def
}.
Admit Obligations.
Module Export OrderedType.
Inductive Compare (X : Type) (lt eq : X -> X -> Prop) (x y : X) : Type :=
| LT : lt x y -> Compare lt eq x y
| EQ : eq x y -> Compare lt eq x y
| GT : lt y x -> Compare lt eq x y.
Definition reg: Type.
Admitted.
Definition node := positive.
Definition code: Type.
Admitted.
Record function: Type := mkfunction {
fn_sig: signature;
fn_params: list reg;
fn_stacksize: Z;
fn_code: code;
fn_entrypoint: node
}.
Definition fundef := AST.fundef function.
Remark link_def_either:
forall (gd1 gd2 gd: globdef fundef unit),
link_def gd1 gd2 = Some gd -> gd = gd1 \/ gd = gd2.
Proof with (try discriminate).
intros until gd.
Local Transparent Linker_def Linker_fundef Linker_varinit Linker_vardef Linker_unit.
destruct gd1 as [f1|v1], gd2 as [f2|v2]...
destruct f1 as [f1|ef1], f2 as [f2|ef2]; simpl...
destruct ef2; intuition congruence.
destruct ef1; intuition congruence.
destruct (external_function_eq ef1 ef2); intuition congruence.
simpl.
unfold link_vardef.
destruct v1 as [info1 init1 ro1 vo1], v2 as [info2 init2 ro2 vo2]; simpl.
destruct (link_varinit init1 init2) as [init|] eqn:LI...
destruct (eqb ro1 ro2) eqn:RO...
destruct (eqb vo1 vo2) eqn:VO...
simpl.
destruct info1, info2.
assert (EITHER: init = init1 \/ init = init2).
{
revert LI.
unfold link_varinit.
destruct (classify_init init1), (classify_init init2); intro EQ; inv EQ; auto.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (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 6.1MiB file on GitHub Actions Artifacts under
|
Minimization interrupted by timeout, being automatically continued. Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/metarocq/pcuic/theories/PCUICConfluence.v in 5h 15m 6s (from ci-metarocq) (interrupted by timeout, being automatically continued) (full log on GitHub Actions - verbose log)⭐ ⏱️ Partially Minimized Coq File (timeout) (truncated to first and last 32KiB; full 35KiB file on GitHub Actions Artifacts under
|
Minimization interrupted by timeout, being automatically continued. Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/metarocq/pcuic/theories/PCUICConfluence.v in 5h 15m 6s (from ci-metarocq) (interrupted by timeout, being automatically continued) (full log on GitHub Actions - verbose log)⭐ ⏱️ Partially Minimized Coq File (timeout) (truncated to first and last 32KiB; full 44KiB file on GitHub Actions Artifacts under
|
Minimization interrupted by timeout, being automatically continued. Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/metarocq/pcuic/theories/PCUICConfluence.v in 5h 15m 7s (from ci-metarocq) (interrupted by timeout, being automatically continued) (full log on GitHub Actions - verbose log)⭐ ⏱️ Partially Minimized Coq File (timeout) (truncated to first and last 32KiB; full 71KiB file on GitHub Actions Artifacts under
|
Minimization interrupted by timeout, being automatically continued. Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/metarocq/pcuic/theories/PCUICConfluence.v in 5h 15m 7s (from ci-metarocq) (interrupted by timeout, being automatically continued) (full log on GitHub Actions - verbose log)⭐ ⏱️ Partially Minimized Coq File (timeout) (truncated to first and last 32KiB; full 95KiB file on GitHub Actions Artifacts under
|
Minimization interrupted by timeout, being automatically continued. Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/metarocq/pcuic/theories/PCUICConfluence.v in 5h 15m 6s (from ci-metarocq) (interrupted by timeout, being automatically continued) (full log on GitHub Actions - verbose log)⭐ ⏱️ Partially Minimized Coq File (timeout) (truncated to first and last 32KiB; full 154KiB file on GitHub Actions Artifacts under
|
Minimization interrupted by timeout, being automatically continued. Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/metarocq/pcuic/theories/PCUICConfluence.v in 5h 15m 8s (from ci-metarocq) (interrupted by timeout, being automatically continued) (full log on GitHub Actions - verbose log)⭐ ⏱️ Partially Minimized Coq File (timeout) (truncated to first and last 32KiB; full 74KiB file on GitHub Actions Artifacts under
|
Minimization interrupted by timeout, being automatically continued. Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/metarocq/pcuic/theories/PCUICConfluence.v in 5h 15m 7s (from ci-metarocq) (interrupted by timeout, being automatically continued) (full log on GitHub Actions - verbose log)⭐ ⏱️ Partially Minimized Coq File (timeout) (truncated to first and last 32KiB; full 89KiB file on GitHub Actions Artifacts under
|
Minimization interrupted by timeout, being automatically continued. Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/metarocq/pcuic/theories/PCUICConfluence.v in 5h 15m 7s (from ci-metarocq) (interrupted by timeout, being automatically continued) (full log on GitHub Actions - verbose log)⭐ ⏱️ Partially Minimized Coq File (timeout) (truncated to first and last 32KiB; full 106KiB file on GitHub Actions Artifacts under
|
|
interrupted manually |
|
Reduced compcert example: Module M.
Axiom foo : bool.
End M.
Import M.
Ltac bli H := inversion H.
Goal forall n m:nat, Some n = Some m -> True /\ True.
intros n m.
intro foo; split; bli foo.(very important to get the bug: use thanks ltac |
SkySkimmer
commented
May 28, 2025
plugins/ltac/tacintern.ml
Outdated
| let intern_constr_reference strict ist qid = | ||
| let id = qualid_basename qid in | ||
| if qualid_is_ident qid && not strict && find_hyp (qualid_basename qid) ist then | ||
| (DAst.make @@ GVar id), Some (make @@ CRef (qid,None)) | ||
| else if qualid_is_ident qid && find_var (qualid_basename qid) ist then | ||
| (DAst.make @@ GVar id), if strict then None else Some (make @@ CRef (qid,None)) | ||
| else | ||
| DAst.make @@ GRef (locate_global_with_alias qid,None), | ||
| if strict then None else Some (make @@ CRef (qid,None)) | ||
| match intern_constr {ist with strict_check=true} (CAst.make (CRef (qid,None))) with |
There was a problem hiding this comment.
the problem is strict_check=true here when strict=false
#17084 had strict_check=true but then did some adhoc stuff with the returned value:
let c,_ = intern_constr {ist with strict_check=true} (CAst.make (CRef (qid,None))) in
c, if strict then None else Some (make @@ CRef (qid,None))unless someone (@herbelin?) knows a reason to keep strict_check constant true I'll do strict_check=strict
7031535 to
d999a8c
Compare
… impargs. This was the case in non-strict mode (via interpretation at runtime), but, in strict mode, it was instead the reference without its maximal implicit arguments. Also deprecate the old strict mode internalization. For compat with enabling the option, the main impact is on "class_apply" which we reformulate as a tactic notation to ensure that its argument is always interpreted as a term. Replaces rocq-prover#17084 in a more backward compatible way. Co-authored-by: Hugo Herbelin <herbelin@users.noreply.github.com>
d999a8c to
20a6687
Compare
Villetaneuse
reviewed
Jun 3, 2025
Comment on lines
+2
to
+3
| flag :flag:`Ltac Always Insert Implicits` to interprete a :n:`@qualid` argument to a ltac as a term (with insertion of any implicit arguments, unfolding notations, etc) | ||
| in a toplevel :cmd:`Ltac` definition instead of interpreting it as the reference without implicit arguments. |
There was a problem hiding this comment.
Suggested change
| flag :flag:`Ltac Always Insert Implicits` to interprete a :n:`@qualid` argument to a ltac as a term (with insertion of any implicit arguments, unfolding notations, etc) | |
| in a toplevel :cmd:`Ltac` definition instead of interpreting it as the reference without implicit arguments. | |
| flag :flag:`Ltac Always Insert Implicits` to interpret :n:`@qualid` arguments as terms (with insertion of any implicit arguments, unfolding notations, etc) | |
| in further toplevel :cmd:`Ltac` definitions instead of interpreting them as references without implicit arguments. |
Comment on lines
+2
to
+3
| interpreting a :n:`@qualid` argument to a ltac as a term (with insertion of any implicit arguments, unfolding notations, etc) | ||
| in a toplevel :cmd:`Ltac` definition instead of interpreting it as the reference without implicit arguments. |
There was a problem hiding this comment.
Suggested change
| interpreting a :n:`@qualid` argument to a ltac as a term (with insertion of any implicit arguments, unfolding notations, etc) | |
| in a toplevel :cmd:`Ltac` definition instead of interpreting it as the reference without implicit arguments. | |
| Interpreting :n:`@qualid` arguments as terms (with insertion of any implicit arguments, unfolding notations, etc) | |
| in toplevel :cmd:`Ltac` definitions instead of interpreting them as references without implicit arguments. |
| By default, ltac applications to a :n:`@qualid` inside a toplevel | ||
| :cmd:`Ltac`'s body can behave differently from the same application in | ||
| proof scripts: in proof scripts the :n:`@qualid` is interpreted as | ||
| a term, but in toplevel :cmd:`Ltac` it is interpreted as a |
There was a problem hiding this comment.
Suggested change
| a term, but in toplevel :cmd:`Ltac` it is interpreted as a | |
| a term, but in a toplevel :cmd:`Ltac` definition, it is interpreted as a |
|
Doesn't seem like it will be ready for 9.1. |
SkySkimmer
commented
Jun 6, 2025
| (* XXX enable printing implicits while printing? | ||
| currently we get "got @foo but in proof scripts foo would be produced" *) | ||
| let warn_noninserted_impls = | ||
| CWarnings.create ~name:"ltac-non-inserted-implicits" ~category:Deprecation.Version.v9_1 |
There was a problem hiding this comment.
TODO change the version since this won't be 9.1
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This was the case in non-strict mode (via interpretation at runtime), but, in strict mode, it was instead the reference without its maximal implicit arguments.
Also deprecate the old strict mode internalization.
For compat with enabling the option, the main impact is on "class_apply" which we reformulate as a tactic notation to ensure that its argument is always interpreted as a term.
Replaces #17084 in a more backward compatible way.