rm problematic variables under evars for evar instantiation #21180
+25
−2
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
coqbot-app
bot
added
the
needs: full CI
|
I am not sure what to do about |
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
|
🔴 CI failures at commit 903d928 without any failure in the test-suite ✔️ Corresponding jobs for the base commit 3853feb succeeded ❔ Ask me to try to extract minimal test cases that can be added to the test-suite 🏃
|
…new variable when instantiating old shelved variable with the new one in `evarsolve/instantiate_evar`
|
I fail to reproduce the |
|
@coqbot ci minimize |
|
I have initiated minimization at commit 903d928 for the suggested targets ci-argosy, ci-elpi_test, ci-hott, ci-iris as requested. |
|
It reproduces on my machine |
|
Error: Could not minimize file in 3m 26s (from ci-argosy) (full log on GitHub Actions, cc @JasonGross) build log (truncated to last 26KiB; full 3.1MiB file on GitHub Actions Artifacts under
|
|
Error: Could not minimize file in 8m 27s (from ci-elpi_test) (full log on GitHub Actions, cc @JasonGross) build log (truncated to last 26KiB; full 4.0MiB file on GitHub Actions Artifacts under
|
|
Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/hott/theories/Algebra/Groups/Group.v in 25m 7s (from ci-hott) (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" "-noinit" "-indices-matter" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-coqlib" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq//" "-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" "HoTT.Algebra.Groups.Group") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 1283 lines to 36 lines, then from 49 lines to 593 lines, then from 599 lines to 49 lines, then from 62 lines to 654 lines, then from 659 lines to 82 lines, then from 95 lines to 136 lines, then from 142 lines to 83 lines, then from 96 lines to 809 lines, then from 812 lines to 137 lines, then from 150 lines to 964 lines, then from 969 lines to 183 lines, then from 196 lines to 286 lines, then from 292 lines to 192 lines, then from 205 lines to 521 lines, then from 523 lines to 216 lines, then from 230 lines to 215 lines, then from 229 lines to 180 lines, then from 194 lines to 180 lines *)
(* coqc version 9.2+alpha compiled with OCaml 4.14.2
coqtop version 9.2+alpha
Expected coqc runtime on this file: 0.124 sec *)
Declare Scope type_scope.
Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
Reserved Notation "x = y :> T"
(at level 70, y at next level, no associativity).
Reserved Notation "x * y" (at level 40, left associativity).
Reserved Notation "p ^" (at level 1, format "p '^'").
Delimit Scope trunc_scope with trunc.
Global Open Scope trunc_scope.
Global Open Scope type_scope.
Declare ML Module "ltac_plugin:coq-core.plugins.ltac".
Global Set Default Proof Mode "Classic".
Global Set Universe Polymorphism.
Global Unset Strict Universe Declaration.
Create HintDb typeclass_instances discriminated.
Notation "A -> B" := (forall (_ : A), B) : type_scope.
Record prod (A B : Type) := pair { fst : A ; snd : B }.
Notation "x * y" := (prod x y) : type_scope.
Notation Type0 := Set.
Definition flip A B `{P : A -> B -> Type}
: (forall a b, P a b) -> (forall b a, P a b).
Admitted.
Arguments flip {A B P} f b a /.
Inductive paths {A : Type} (a : A) : A -> Type :=
idpath : paths a a.
Notation "x = y :> A" := (@paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope.
Inductive trunc_index : Type0 :=
| minus_two : trunc_index
| trunc_S : trunc_index -> trunc_index.
Notation "n .+1" := (trunc_S n) : trunc_scope.
Notation "n .+2" := (n.+1.+1)%trunc : trunc_scope.
Inductive IsTrunc_internal (A : Type@{u}) : trunc_index -> Type@{u} :=
| Build_Contr : forall (center : A) (contr : forall y, center = y), IsTrunc_internal A minus_two
| istrunc_S : forall {n:trunc_index}, (forall x y:A, IsTrunc_internal (x = y) n) -> IsTrunc_internal A (trunc_S n).
Notation IsTrunc n A := (IsTrunc_internal A n).
Notation IsHSet A := (IsTrunc minus_two.+2 A).
Tactic Notation "do_with_holes" tactic3(x) uconstr(p) :=
x uconstr:(p) ||
x uconstr:(p _) ||
x uconstr:(p _ _) ||
x uconstr:(p _ _ _) ||
x uconstr:(p _ _ _ _) ||
x uconstr:(p _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _).
Class IsGlobalAxiom (A : Type) : Type0 := {}.
Ltac is_global_axiom A := let _ := constr:(_ : IsGlobalAxiom A) in idtac.
Ltac global_axiom := try match goal with
| |- ?G => is_global_axiom G; exact _
end.
Tactic Notation "snrefine" uconstr(term) := simple notypeclasses refine term; global_axiom.
Tactic Notation "snapply" uconstr(term)
:= do_with_holes ltac:(fun x => snrefine x) term.
Class SgOp A := sg_op: A -> A -> A.
Class MonUnit A := mon_unit: A.
Class Plus A := plus: A -> A -> A.
Class Mult A := mult: A -> A -> A.
Class One A := one: A.
Class Zero A := zero: A.
Class Negate A := negate: A -> A.
Class Inverse A := inv: A -> A.
#[global] Typeclasses Transparent SgOp MonUnit Plus Mult Zero One Negate.
Notation "(.*.)" := sg_op (only parsing) : mc_mult_scope.
Notation "x ^" := (inv x) : mc_mult_scope.
Notation "(^)" := inv (only parsing) : mc_mult_scope.
Class LeftIdentity {A B} (op : A -> B -> B) (x : A): Type
:= left_identity: forall y, op x y = y.
Class RightIdentity {A B} (op : A -> B -> A) (y : B): Type
:= right_identity: forall x, op x y = x.
Class LeftInverse {A} {B} {C} (op : A -> B -> C) (inv : B -> A) (unit : C)
:= left_inverse: forall x, op (inv x) x = unit.
Class RightInverse {A} {B} {C} (op : A -> B -> C) (inv : A -> B) (unit : C)
:= right_inverse: forall x, op x (inv x) = unit.
Class HeteroAssociative {A B C AB BC ABC}
(fA_BC: A -> BC -> ABC) (fBC: B -> C -> BC)
(fAB_C: AB -> C -> ABC) (fAB : A -> B -> AB): Type
:= associativity : forall x y z, fA_BC x (fBC y z) = fAB_C (fAB x y) z.
Class Associative {A} (f : A -> A -> A)
:= simple_associativity :: HeteroAssociative f f f f.
Section upper_classes.
Context (A : Type@{i}).
Local Open Scope mc_mult_scope.
Class IsSemiGroup {Aop: SgOp A} :=
{ sg_set :: IsHSet A
; sg_ass :: Associative (.*.) }.
Class IsMonoid {Aop : SgOp A} {Aunit : MonUnit A} :=
{ monoid_semigroup :: IsSemiGroup
; monoid_left_id :: LeftIdentity (.*.) mon_unit
; monoid_right_id :: RightIdentity (.*.) mon_unit }.
Class IsGroup {Aop : SgOp A} {Aunit : MonUnit A} {Ainv : Inverse A} :=
{ group_monoid :: @IsMonoid (.*.) mon_unit
; inverse_l :: LeftInverse (.*.) (^) mon_unit
; inverse_r :: RightInverse (.*.) (^) mon_unit
}.
End upper_classes.
Local Open Scope mc_mult_scope.
Record Group := Build_Group_internal {
group_type :> Type;
group_sgop :: SgOp group_type;
group_unit :: MonUnit group_type;
group_inverse :: Inverse group_type;
group_isgroup :: IsGroup group_type;
group_assoc_opp : Associative (flip group_sgop);
}.
Definition Build_Group (G : Type)
`(op : SgOp G, unit : MonUnit G, inv : Inverse G, grp : !IsGroup G)
: Group.
Admitted.
Definition grp_prod : Group -> Group -> Group.
Proof.
intros G H.
snapply (Build_Group (G * H)).
4: repeat split.🛠️ 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 2.6MiB file on GitHub Actions Artifacts under
|
|
@coqbot ci minimize ci-argosy |
|
I am now running minimization at commit 903d928 on requested target ci-argosy. I'll come back to you with the results once it's done. |
|
It's not going to work, the passing job doesn't make install so doesn't upload artifacts |
|
Ah, given the error message I thought it was the connection going wonky... |
|
Error: Could not minimize file in 3m 15s (from ci-argosy) (full log on GitHub Actions, cc @JasonGross) build log (truncated to last 26KiB; full 3.1MiB file on GitHub Actions Artifacts under
|
|
Can't we just fix argosy to make install? |
|
It has some weird build system with no install target |
|
Here is a reproducible example hand-extracted from argosy: Definition relation := fun A B T : Type => A -> B -> T -> Prop.
Axiom addr : Type.
Axiom block : Type.
Axiom D_State : Type.
Axiom State : Type.
Axiom Op : Type -> Type.
Axiom proc : (Type -> Type) -> Type -> Type.
Axiom read : addr -> proc Op block.
Axiom Recover : proc Op unit.
Axiom rd_abstraction : D_State -> State -> unit -> Prop.
Axiom Specification : Type -> Type -> Type -> Type.
Axiom refine_spec :
forall [AState CState : Type],
relation AState CState unit ->
forall [T R : Type], Specification T R AState -> AState -> Specification T R CState.
Axiom proc_hspec :
forall {Op : Type -> Type} {State : Type},
forall [T : Type], proc Op T -> Specification T unit State -> Prop.
Axiom proc_rspec :
forall {Op : Type -> Type} {State : Type},
forall [T R : Type], proc Op T -> proc Op R -> Specification T R State -> Prop.
Axiom proc_hspec_to_rspec :
forall {Op : Type -> Type} {State : Type} [A' T R : Type]
[rec_hspec : A' -> Specification R unit State] (p_rspec : Specification T R State)
[p : proc Op T] [rec : proc Op R],
(forall a : A', @proc_hspec Op State R rec (rec_hspec a)) ->
@proc_rspec Op State T R p rec p_rspec.
Axiom read_spec : addr -> Specification block unit D_State.
Theorem read_rec_ok : forall (a : addr) (d : D_State),
@proc_rspec Op State block unit (read a) Recover
(@refine_spec D_State State rd_abstraction block unit (read_spec a) d).
Proof.
intros a d.
eapply proc_hspec_to_rspec.
solve[eauto]. (* works on master, fails on this PR *)We can probably simplify it further. |
|
Even shorter: Axiom Specification : Type.
Axiom proc_hspec : Specification -> Prop.
Axiom proc_rspec : Prop.
Axiom proc_hspec_to_rspec : forall [A' : Type] [rec_hspec : A' -> Specification],
(forall a : A', @proc_hspec (rec_hspec a)) -> proc_rspec.
Theorem read_rec_ok : proc_rspec.
Proof.
eapply proc_hspec_to_rspec.
solve[eauto]. |
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/iris/iris/base_logic/lib/cancelable_invariants.v in 5h 15m 8s (from ci-iris) (interrupted by timeout, being automatically continued) (full log on GitHub Actions - verbose log)⭐ ⏱️ Partially Minimized Coq File (timeout)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-notation-overridden" "-w" "-redundant-canonical-projection" "-w" "-notation-incompatible-prefix" "-w" "-deprecated-from-Coq" "-w" "-deprecated-dirpath-Coq" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-coqlib" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq//" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris" "iris" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris_heap_lang" "iris.heap_lang" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris_unstable" "iris.unstable" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris_deprecated" "iris.deprecated" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Autosubst" "Autosubst" "-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/Stdlib" "Stdlib" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/stdpp" "stdpp" "-top" "iris.base_logic.lib.cancelable_invariants") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 204 lines to 32 lines, then from 45 lines to 651 lines, then from 657 lines to 31 lines, then from 44 lines to 706 lines, then from 712 lines to 58 lines, then from 71 lines to 654 lines, then from 660 lines to 77 lines, then from 90 lines to 482 lines, then from 488 lines to 104 lines, then from 117 lines to 987 lines, then from 990 lines to 132 lines, then from 145 lines to 702 lines, then from 708 lines to 148 lines, then from 161 lines to 1079 lines, then from 1085 lines to 175 lines, then from 188 lines to 735 lines, then from 736 lines to 195 lines, then from 208 lines to 591 lines, then from 597 lines to 197 lines, then from 210 lines to 923 lines, then from 929 lines to 201 lines, then from 214 lines to 587 lines, then from 593 lines to 206 lines, then from 219 lines to 899 lines, then from 905 lines to 219 lines, then from 232 lines to 1231 lines, then from 1237 lines to 236 lines, then from 249 lines to 1215 lines, then from 1221 lines to 248 lines, then from 261 lines to 791 lines, then from 797 lines to 261 lines, then from 274 lines to 586 lines, then from 592 lines to 539 lines *)
(* coqc version 9.2+alpha compiled with OCaml 4.14.2
coqtop version 9.2+alpha
Expected coqc runtime on this file: 0.922 sec *)
Require iris.base_logic.bi.
Require iris.bi.lib.cmra.
Require iris.proofmode.proofmode.
Require iris.proofmode.class_instances_updates.
Require iris.proofmode.class_instances.
Require iris.proofmode.ltac_tactics.
Require iris.proofmode.notation.
Require iris.proofmode.coq_tactics.
Require iris.proofmode.class_instances_later.
Require iris.proofmode.class_instances_frame.
Require iris.proofmode.class_instances_internal_eq.
Require iris.proofmode.class_instances_plainly.
Require iris.proofmode.class_instances_embedding.
Require iris.proofmode.modality_instances.
Require iris.proofmode.reduction.
Require iris.proofmode.classes.
Require iris.proofmode.environments.
Require iris.proofmode.intro_patterns.
Require iris.proofmode.spec_patterns.
Require iris.proofmode.sel_patterns.
Require iris.proofmode.tokens.
Require iris.proofmode.modalities.
Require iris.proofmode.class_instances_make.
Require iris.bi.telescopes.
Require iris.proofmode.classes_make.
Require iris.proofmode.base.
Require iris.bi.bi.
Require iris.bi.embedding.
Require iris.bi.updates.
Require iris.bi.plainly.
Require iris.bi.internal_eq.
Require iris.bi.big_op.
Require iris.algebra.gmap.
Require iris.algebra.gset.
Require iris.algebra.list.
Require iris.algebra.big_op.
Require stdpp.gmultiset.
Require iris.bi.derived_laws_later.
Require iris.bi.derived_laws.
Require iris.bi.extensions.
Require iris.bi.derived_connectives.
Require iris.base_logic.upred.
Require stdpp.namespaces.
Require iris.bi.interface.
Require iris.algebra.csum.
Require stdpp.coPset.
Require stdpp.gmap.
Require iris.algebra.updates.
Require iris.algebra.stepindex_finite.
Require iris.algebra.proofmode_classes.
Require iris.algebra.local_updates.
Require iris.algebra.excl.
Require iris.algebra.agree.
Require iris.algebra.cmra.
Require iris.algebra.monoid.
Require iris.algebra.ofe.
Require iris.algebra.stepindex.
Require iris.prelude.prelude.
Require stdpp.infinite.
Require stdpp.ssreflect.
Require stdpp.pretty.
Require stdpp.pmap.
Require stdpp.prelude.
Require stdpp.mapset.
Require stdpp.fin_map_dom.
Require stdpp.fin_maps.
Require stdpp.fin_sets.
Require stdpp.relations.
Require stdpp.listset.
Require stdpp.sets.
Require stdpp.strings.
Require stdpp.finite.
Require stdpp.vector.
Require stdpp.countable.
Require stdpp.list.
Require stdpp.list_numbers.
Require stdpp.list_tactics.
Require stdpp.list_misc.
Require stdpp.list_monad.
Require stdpp.list_relations.
Require stdpp.nat_cancel.
Require stdpp.list_basics.
Require stdpp.lexico.
Require stdpp.numbers.
Require Stdlib.ZArith.ZArith.
Require stdpp.fin.
Require stdpp.telescopes.
Require stdpp.orders.
Require stdpp.option.
Require stdpp.hlist.
Require stdpp.functions.
Require stdpp.tactics.
Require iris.proofmode.string_ident.
Require Stdlib.ZArith.Znumtheory.
Require Stdlib.ZArith.ZNsatz.
Require Stdlib.ZArith.Zbitwise.
Require Stdlib.btauto.Btauto.
Require Stdlib.micromega.ZArith_hints.
Require Stdlib.btauto.Reflect.
Require Stdlib.btauto.Algebra.
Require Stdlib.ZArith.Zcong.
Require Stdlib.ZArith.ZModOffset.
Require Stdlib.ZArith.Zdivisibility.
Require Stdlib.ZArith.Zdiv_facts.
Require Stdlib.micromega.Lia.
Require Stdlib.QArith.QArith.
Require Stdlib.micromega.ZMicromega.
Require Stdlib.QArith.QNsatz.
Require Stdlib.ZArith.Zdiv.
Require Stdlib.ZArith.Zpower.
Require Stdlib.ZArith.Zcomplements.
Require Stdlib.QArith.Qring.
Require Stdlib.QArith.Qfield.
Require Stdlib.QArith.Qcanon.
Require Stdlib.omega.PreOmega.
Require Stdlib.QArith.Qreduction.
Require Stdlib.micromega.Zify.
Require Stdlib.Strings.String.
Require Stdlib.QArith.QArith_base.
Require Stdlib.micromega.ZifyInst.
Require Stdlib.ZArith.ZArith_base.
Require Stdlib.Arith.Arith.
Require Stdlib.micromega.ZCoeff.
Require Stdlib.ZArith.Zhints.
Require Stdlib.NArith.NArith.
Require Stdlib.nsatz.NsatzTactic.
Require Stdlib.micromega.RingMicromega.
Require Stdlib.ZArith.Zabs.
Require Stdlib.setoid_ring.Integral_domain.
Require Stdlib.setoid_ring.Field.
Require Stdlib.ZArith.Zbool.
Require Stdlib.setoid_ring.ZArithRing.
Require Stdlib.setoid_ring.Field_tac.
Require Stdlib.setoid_ring.Cring.
Require Stdlib.setoid_ring.ArithRing.
Require Stdlib.ZArith.Wf_Z.
Require Stdlib.setoid_ring.NArithRing.
Require Stdlib.setoid_ring.Field_theory.
Require Stdlib.micromega.OrderedRing.
Require Stdlib.ZArith.ZArith_dec.
Require Stdlib.setoid_ring.Ring.
Require Stdlib.setoid_ring.Ncring_tac.
Require Stdlib.setoid_ring.Ring_base.
Require Stdlib.setoid_ring.Ncring_initial.
Require Stdlib.omega.OmegaLemmas.
Require Stdlib.ZArith.auxiliary.
Require Stdlib.ZArith.Zmisc.
Require Stdlib.ZArith.Zminmax.
Require Stdlib.ZArith.Zmin.
Require Stdlib.ZArith.Zmax.
Require Stdlib.setoid_ring.Ring_tac.
Require Stdlib.setoid_ring.Ncring_polynom.
Require Stdlib.ZArith.Zorder.
Require Stdlib.ZArith.Znat.
Require Stdlib.setoid_ring.InitialRing.
Require Stdlib.setoid_ring.Ring_polynom.
Require Stdlib.micromega.EnvRing.
Require Stdlib.micromega.VarMap.
Require Stdlib.micromega.Env.
Require Stdlib.setoid_ring.Ncring.
Require Stdlib.ZArith.Zpow_def.
Require Stdlib.ZArith.Zeven.
Require Stdlib.ZArith.Zcompare.
Require Stdlib.ZArith.BinInt.
Require Stdlib.micromega.DeclConstantZ.
Require Stdlib.Strings.Ascii.
Require stdpp.decidable.
Require iris.proofmode.ident_name.
Require Stdlib.Strings.Byte.
Require Stdlib.NArith.NArith_base.
Require stdpp.well_founded.
Require stdpp.proof_irrel.
Require Stdlib.Vectors.Vector.
Require stdpp.base.
Require Stdlib.Vectors.VectorEq.
Require Stdlib.ZArith.BinIntDef.
Require Stdlib.Vectors.VectorSpec.
Require Stdlib.NArith.Nnat.
Require Stdlib.setoid_ring.Ring_theory.
Require Stdlib.NArith.Nsqrt_def.
Require Stdlib.NArith.Ngcd_def.
Require Stdlib.NArith.Ndiv_def.
Require Stdlib.setoid_ring.BinList.
Require Stdlib.NArith.BinNat.
Require Stdlib.Vectors.VectorDef.
Require Stdlib.PArith.PArith.
Require Stdlib.NArith.BinNatDef.
Require Stdlib.Vectors.Fin.
Require Stdlib.PArith.Pnat.
Require Stdlib.PArith.POrderedType.
Require Stdlib.Arith.Arith_base.
Require Stdlib.PArith.BinPos.
Require Stdlib.Sorting.Permutation.
Require Stdlib.Lists.ListTactics.
Require Stdlib.micromega.Tauto.
Require Stdlib.Lists.Finite.
Require Stdlib.micromega.Refl.
Require Stdlib.Lists.ListDec.
Require Stdlib.Lists.List.
Require Stdlib.Arith.Peano_dec.
Require Stdlib.Arith.Wf_nat.
Require Stdlib.Arith.Factorial.
Require Stdlib.Arith.EqNat.
Require Stdlib.Arith.Compare_dec.
Require Stdlib.Arith.Between.
Require Stdlib.Arith.PeanoNat.
Require Stdlib.Numbers.Natural.Abstract.NProperties.
Require Stdlib.Numbers.Integer.Abstract.ZProperties.
Require Stdlib.Numbers.Natural.Abstract.NLcm0.
Require Stdlib.Numbers.Natural.Abstract.NBits.
Require Stdlib.Numbers.Integer.Abstract.ZLcm.
Require Stdlib.Numbers.Integer.Abstract.ZBits.
Require Stdlib.Numbers.Natural.Abstract.NLog.
Require Stdlib.Numbers.Natural.Abstract.NLcm.
Require Stdlib.Numbers.Integer.Abstract.ZPow.
Require Stdlib.Numbers.Natural.Abstract.NPow.
Require Stdlib.Numbers.Natural.Abstract.NDiv0.
Require Stdlib.Numbers.Integer.Abstract.ZGcd.
Require Stdlib.Numbers.Integer.Abstract.ZDivTrunc.
Require Stdlib.Numbers.Integer.Abstract.ZDivFloor.
Require Stdlib.Numbers.Natural.Abstract.NSqrt.
Require Stdlib.Numbers.Natural.Abstract.NParity.
Require Stdlib.Numbers.Natural.Abstract.NMaxMin.
Require Stdlib.Numbers.Natural.Abstract.NGcd.
Require Stdlib.Numbers.Natural.Abstract.NDiv.
Require Stdlib.Numbers.Integer.Abstract.ZSgnAbs.
Require Stdlib.Numbers.Integer.Abstract.ZParity.
Require Stdlib.Numbers.Integer.Abstract.ZMaxMin.
Require Stdlib.Numbers.Natural.Abstract.NSub.
Require Stdlib.Numbers.Integer.Abstract.ZMulOrder.
Require Stdlib.Numbers.Natural.Abstract.NMulOrder.
Require Stdlib.Numbers.Integer.Abstract.ZAddOrder.
Require Stdlib.Numbers.Natural.Abstract.NAddOrder.
Require Stdlib.Numbers.Integer.Abstract.ZLt.
Require Stdlib.Numbers.Natural.Abstract.NOrder.
Require Stdlib.Numbers.Integer.Abstract.ZMul.
Require Stdlib.Numbers.Natural.Abstract.NAdd.
Require Stdlib.Numbers.Integer.Abstract.ZAdd.
Require Stdlib.Numbers.Natural.Abstract.NBase.
Require Stdlib.Numbers.Integer.Abstract.ZBase.
Require Stdlib.Numbers.Natural.Abstract.NAxioms.
Require Stdlib.Numbers.Integer.Abstract.ZAxioms.
Require Stdlib.Numbers.NatInt.NZBits.
Require Ltac2.Ltac2.
Require Stdlib.Numbers.NatInt.NZLog.
Module Export frac.
Export iris.algebra.cmra.
Notation frac := Qp (only parsing).
Canonical Structure fracO := leibnizO frac.
Local Instance frac_valid_instance : Valid frac. exact (λ x, (x ≤ 1)%Qp). Defined.
Local Instance frac_pcore_instance : PCore frac. exact (λ _, None). Defined.
Local Instance frac_op_instance : Op frac. exact (λ x y, (x + y)%Qp). Defined.
Definition frac_ra_mixin : RAMixin frac.
Admitted.
Canonical Structure fracR := discreteR frac frac_ra_mixin.
End frac.
Module Export iris_DOT_algebra_DOT_frac.
Module Export iris.
Module Export algebra.
Module Export frac.
End frac.
End algebra.
End iris.
End iris_DOT_algebra_DOT_frac.
Export iris.base_logic.bi.
Module Export iris_DOT_base_logic_DOT_derived.
Module Export iris.
Module Export base_logic.
Module Export derived.
End derived.
End base_logic.
End iris.
End iris_DOT_base_logic_DOT_derived.
Export iris.algebra.frac.
Export iris.algebra.agree.
Module Export iris_DOT_algebra_DOT_view.
Module Export iris.
Module Export algebra.
Module Export view.
End view.
End algebra.
End iris.
End iris_DOT_algebra_DOT_view.
Export iris.algebra.gmap.
Definition gmap_viewR {SI : sidx} (K : Type) `{Countable K} (V : cmra) : cmra.
Admitted.
Module Export iris_DOT_algebra_DOT_lib_DOT_gmap_view.
Module Export iris.
Module Export algebra.
Module Export lib.
Module Export gmap_view.
End gmap_view.
End lib.
End algebra.
End iris.
End iris_DOT_algebra_DOT_lib_DOT_gmap_view.
Export iris.algebra.view.
Definition authR {SI : sidx} (A : ucmra) : cmra.
Admitted.
Module Export iris_DOT_algebra_DOT_auth.
Module Export iris.
Module Export algebra.
Module Export auth.
End auth.
End algebra.
End iris.
End iris_DOT_algebra_DOT_auth.
Module Export iris_DOT_algebra_DOT_lib_DOT_excl_auth.
Module Export excl_auth.
End excl_auth.
End iris_DOT_algebra_DOT_lib_DOT_excl_auth.
Module Export algebra.
End algebra.
Export iris.base_logic.derived.
Module Export base_logic.
End base_logic.
Structure gFunctor := GFunctor {
gFunctor_F :> rFunctor;
gFunctor_map_contractive : rFunctorContractive gFunctor_F;
}.
Record gFunctors := GFunctors {
gFunctors_len : nat;
gFunctors_lookup : fin gFunctors_len → gFunctor
}.
Definition gid (Σ : gFunctors) := fin (gFunctors_len Σ).
Definition gname := positive.
Definition iResUR (Σ : gFunctors) : ucmra.
Admitted.
Notation iProp Σ := (uPred (iResUR Σ)).
Notation iPropO Σ := (uPredO (iResUR Σ)).
Module Export iprop.
End iprop.
Class inG (Σ : gFunctors) (A : cmra) := InG {
inG_id : gid Σ;
inG_apply := rFunctor_apply (gFunctors_lookup Σ inG_id);
inG_prf : A = inG_apply (iPropO Σ) _;
}.
Local Definition own_def `{!inG Σ A} (γ : gname) (a : A) : iProp Σ.
Admitted.
Local Definition own_aux : seal (@own_def).
Admitted.
Definition own := own_aux.(unseal).
Global Arguments own {Σ A _} γ a.
Module Export iris_DOT_base_logic_DOT_lib_DOT_own.
Module Export iris.
Module Export base_logic.
Module Export lib.
Module Export own.
End own.
End lib.
End base_logic.
End iris.
End iris_DOT_base_logic_DOT_lib_DOT_own.
Export iris.algebra.cmra.
Local Instance nat_valid_instance : Valid nat.
Admitted.
Local Instance nat_pcore_instance : PCore nat.
Admitted.
Local Instance nat_op_instance : Op nat.
Admitted.
Lemma nat_ra_mixin : RAMixin nat.
Admitted.
Canonical Structure natR : cmra.
exact (discreteR nat nat_ra_mixin).
Defined.
Local Instance nat_unit_instance : Unit nat.
Admitted.
Lemma nat_ucmra_mixin : UcmraMixin nat.
Admitted.
Canonical Structure natUR : ucmra.
exact (Ucmra nat nat_ucmra_mixin).
Defined.
Module Export numbers.
End numbers.
Export iris.algebra.auth.
Import iris.base_logic.lib.own.
Class lcGS (Σ : gFunctors) := LcGS {
#[local] lcGS_inG :: inG Σ (authR natUR);
lcGS_name : gname;
}.
Module Export le_upd_if.
End le_upd_if.
Module Export iris_DOT_base_logic_DOT_lib_DOT_later_credits.
Module Export iris.
Module Export base_logic.
Module Export lib.
Module Export later_credits.
End later_credits.
End lib.
End base_logic.
End iris.
End iris_DOT_base_logic_DOT_lib_DOT_later_credits.
Export stdpp.coPset.
Inductive coPset_disj :=
| CoPset : coPset → coPset_disj
| CoPsetInvalid : coPset_disj.
Canonical Structure coPset_disjO := leibnizO coPset_disj.
Local Instance coPset_disj_valid_instance : Valid coPset_disj.
Admitted.
Local Instance coPset_disj_op_instance : Op coPset_disj.
Admitted.
Local Instance coPset_disj_pcore_instance : PCore coPset_disj.
Admitted.
Lemma coPset_disj_ra_mixin : RAMixin coPset_disj.
Admitted.
Canonical Structure coPset_disjR := discreteR coPset_disj coPset_disj_ra_mixin.
Module Export iris_DOT_algebra_DOT_coPset.
Module Export iris.
Module Export algebra.
Module Export coPset.
End coPset.
End algebra.
End iris.
End iris_DOT_algebra_DOT_coPset.
Import iris.algebra.lib.gmap_view.
Import iris.algebra.gset.
Import iris.algebra.coPset.
Export iris.base_logic.lib.own.
Class wsatGpreS (Σ : gFunctors) : Set := WsatGpreS {
wsatGpreS_inv : inG Σ (gmap_viewR positive (agreeR $ laterO (iPropO Σ)));
wsatGpreS_enabled : inG Σ coPset_disjR;
wsatGpreS_disabled : inG Σ (gset_disjR positive);
}.
Class wsatGS (Σ : gFunctors) : Set := WsatG {
wsat_inG : wsatGpreS Σ;
invariant_name : gname;
enabled_name : gname;
disabled_name : gname;
}.
Module Export iris_DOT_base_logic_DOT_lib_DOT_wsat.
Module Export wsat.
End wsat.
End iris_DOT_base_logic_DOT_lib_DOT_wsat.
Export iris.base_logic.lib.later_credits.
Inductive has_lc := HasLc | HasNoLc.
Class invGS_gen (hlc : has_lc) (Σ : gFunctors) : Set := InvG {
#[global] invGS_wsat :: wsatGS Σ;
#[global] invGS_lc :: lcGS Σ;
}.
Global Instance uPred_bi_fupd `{!invGS_gen hlc Σ} : BiFUpd (uPredI (iResUR Σ)).
Admitted.
Global Instance uPred_bi_bupd_fupd `{!invGS_gen hlc Σ} : BiBUpdFUpd (uPredI (iResUR Σ)).
Admitted.
Module Export iris.
Module Export base_logic.
Module Export lib.
Module Export fancy_updates.
End fancy_updates.
End lib.
End base_logic.
End iris.
Export stdpp.namespaces.
Export iris.base_logic.lib.fancy_updates.
Export iris.algebra.excl.
Import iris.proofmode.proofmode.
Class cinvG Σ := {
#[local] cinv_inG :: inG Σ (prodR (optionR (exclR unitO)) (optionR fracR)) ;
}.
Section defs.
Context `{!invGS_gen hlc Σ, !cinvG Σ}.
Definition cinv_own (γ : gname) (p : frac) : iProp Σ.
Admitted.
Definition cinv_excl γ : iProp Σ := own γ (Some (Excl ()), None).
Definition cinv (N : namespace) (γ : gname) (P : iProp Σ) : iProp Σ.
Admitted.
Lemma cinv_own_excl_alloc P :
pred_infinite P → ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ cinv_excl γ ∗ cinv_own γ 1.
Admitted.
Lemma cinv_alloc_strong (I : gname → Prop) E N :
pred_infinite I →
⊢ |={E}=> ∃ γ, ⌜ I γ ⌝ ∗ cinv_own γ 1 ∗ ∀ P, ▷ P ={E}=∗ cinv N γ P.
Proof.
iIntros (?).
iMod cinv_own_excl_alloc as (γ) "[$ [Hexcl $]]"; first done.🛠️ 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.4MiB file on GitHub Actions Artifacts under
|
What about adding something like printf '\nMakefile.coq: _CoqProject\n\tcoq_makefile -f _CoqProject -o $@ $(ALL_VFILES)\n' >> Makefile
make Makefile.coq
make -f Makefile.coq installto Coq's CI? |
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/iris/iris/base_logic/lib/cancelable_invariants.v in 5h 15m 7s (from ci-iris) (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 64KiB 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/iris/iris/base_logic/lib/cancelable_invariants.v in 5h 15m 6s (from ci-iris) (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 104KiB file on GitHub Actions Artifacts under
|
6 tasks
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/iris/iris/base_logic/lib/cancelable_invariants.v in 5h 15m 7s (from ci-iris) (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 139KiB 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/iris/iris/base_logic/lib/cancelable_invariants.v in 5h 15m 8s (from ci-iris) (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 148KiB 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/iris/iris/base_logic/lib/cancelable_invariants.v in 5h 15m 7s (from ci-iris) (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 220KiB 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/iris/iris/base_logic/lib/cancelable_invariants.v in 5h 15m 8s (from ci-iris) (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 188KiB file on GitHub Actions Artifacts under
|
coqbot-app
bot
added
the
needs: full CI
|
Hopefully I correctly did the overlays and the |
|
May I ask for a CI? |
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
|
🔴 CI failure at commit 9faf9e6 without any failure in the test-suite ✔️ Corresponding job for the base commit 034677a succeeded ❔ Ask me to try to extract a minimal test case that can be added to the test-suite 🏃
|
coqbot-app
bot
added
the
needs: full CI
|
I am trying to look into https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1152 It would be great if the new behavior, and in particular the difference between I suppose this only affects legacy unification (used by |
|
I will look into that, although I am not sure where this would go, as it is would not change the description of either |
|
Since the light CI is happy (and the elpi_test overlay is done), can I ask for a full CI? |
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
So this also affect evar_conv, and thus |
coqbot-app
bot
added
the
needs: full CI
|
My apologies, I can not do an overlay. The overlay has been merged anyway, so I reverted the change. Can we try again? |
|
Note that for Iris you no longer need an overlay, an alternative fix has been merged. |
|
This is very artificial, but fails on master and succeeds on my branch. |
|
May I have a CI? |
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
|
I do not understand the |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
6 participants
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.
The unification algorithm sometimes fails on problems of the form
?a = tbecause variables that are not in the scope of?aappear int. This PR solves the case where the variable appears in an argument of an evar, e.g.?b x, by instantiating the evar (?b) to forget the argument.For instance, unifying
forall x : ?T, f (?a x)andforall _ : ?T, ?breduces to unifyingf (?a x)and?b, which fails becausexis not available when instantiating?b.Fixes / closes #????
make doc_gram_rsts.Overlays (to be merged before this)
https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1152