anomaly uncaught exception not_found

JasonGross commented 6 months ago

This blocks the bug minimizer from reducing ci-relation_algebra, or at least blocks it from reporting accurate information about why it can't minimize more. Can we fix it?

Seems interesting that it hit a not found anomaly in the middle of the relation algebra minimization after inlining a file.

Originally posted by @JasonGross in https://github.com/coq/coq/issues/19066#issuecomment-2127831197

@coqbot minimize coq.dev

opam install -y coq-relation-algebra
cat > bug.v <<EOF
(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-projection-no-head-constant" "-w" "-notation-overridden" "-w" "-redundant-canonical-projection" "-w" "-future-coercion-class-field" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/relation_algebra/theories" "RelationAlgebra" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/AAC_tactics" "AAC_tactics" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/HB" "HB" "-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/elpi" "elpi" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/mathcomp" "mathcomp" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/relation_algebra/src" "-top" "RelationAlgebra.ugregex_dec") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 380 lines to 52 lines, then from 65 lines to 348 lines, then from 348 lines to 157 lines, then from 170 lines to 308 lines, then from 312 lines to 157 lines, then from 170 lines to 391 lines, then from 393 lines to 234 lines, then from 247 lines to 890 lines, then from 881 lines to 268 lines, then from 281 lines to 347 lines, then from 352 lines to 278 lines, then from 291 lines to 371 lines, then from 374 lines to 303 lines, then from 316 lines to 371 lines, then from 376 lines to 310 lines, then from 323 lines to 582 lines, then from 581 lines to 344 lines, then from 357 lines to 519 lines, then from 522 lines to 376 lines, then from 389 lines to 790 lines, then from 789 lines to 409 lines, then from 422 lines to 669 lines, then from 666 lines to 452 lines, then from 465 lines to 1009 lines *)
(* coqc version 8.20+alpha compiled with OCaml 4.14.1
   coqtop version runner-cabngxqim-project-4504-concurrent-2:/builds/coq/coq/_build/default,(HEAD detached at 00f8d4428b91a) (00f8d4428b91ac91a5179d770e66d36b9643cd49)
   Expected coqc runtime on this file: 0.000 sec *)
Require Coq.Init.Ltac.
Module Export AdmitTactic.
Module Import LocalFalse.
Inductive False : Prop := .
End LocalFalse.
Axiom proof_admitted : False.
Import Coq.Init.Ltac.
Tactic Notation "admit" := abstract case proof_admitted.
End AdmitTactic.
Require Coq.Classes.Morphisms.
Require Coq.Numbers.BinNums.
Require Coq.Setoids.Setoid.
Require RelationAlgebra.common.
Require RelationAlgebra.level.
Require RelationAlgebra.lattice.

Module RelationAlgebra_DOT_monoid_WRAPPED.
Module monoid.
(** * monoid: typed structures, from ordered monoids to residuated Kleene allegories *)

(** We define here all (typed) structures ranging from partially
   ordered monoids to residuated Kleene allegories *)
Export RelationAlgebra.lattice.

(** * Monoid operations *)

(** The following class packages an ordered typed monoid (i.e., a
   category enriched over a partial order) together with all kinds of
   operations it can come with: iterations, converse, residuals. We
   use dummy values when working in structures lacking some
   operations.

   Like for [lattice.ops], we use a Class but we mainly exploit
   Canonical structures inference mechanism. *)

Universe M.

Class ops := mk_ops {
  ob: Type@{M};                     (** objects of the category *)
  mor: ob -> ob -> lattice.ops; (** morphisms (each homset is a partially ordered structure) *)
  dot: forall n m p, mor n m -> mor m p -> mor n p; (** composition  *)
  one: forall n, mor n n;                           (** identity *)
  itr: forall n, mor n n -> mor n n;                (** strict iteration (transitive closure) *)
  str: forall n, mor n n -> mor n n;                (** Kleene star (reflexive transitive closure) *)
  cnv: forall n m, mor n m -> mor m n;              (** converse (transposed relation) *)
  ldv: forall n m p, mor n m -> mor n p -> mor m p; (** left residual/factor/division  *)
  rdv: forall n m p, mor m n -> mor p n -> mor p m  (** right residual/factor/division *)
}.
Coercion mor: ops >-> Funclass.
Arguments ob : clear implicits.

(** Hints for simpl *)
Arguments mor {ops} n m / : simpl nomatch.
Arguments dot {ops} n m p (x y)%ra / : simpl nomatch.
Arguments one {ops} n / : simpl nomatch.
Arguments itr {ops} n (x)%ra / : simpl nomatch.
Arguments str {ops} n (x)%ra / : simpl nomatch.
Arguments cnv {ops} n m (x)%ra / : simpl nomatch.
Arguments ldv {ops} n m p (x y)%ra / : simpl nomatch.
Arguments rdv {ops} n m p (x y)%ra / : simpl nomatch.

(** Notations (note that "+" and "∩" are just specialisations of the
   notations "⊔" and "⊓", when these operations actually come
   from a monoid) *)

(**
   ∩ : \cap (company-coq) or INTERSECTION (0x2229)

   ⋅ : \cdot (company coq) or DOT OPERATOR (0x22c5)
*)

Notation "x ⋅ y" := (dot _ _ _ x y) (left associativity, at level 25, format "x ⋅ y"): ra_terms.
Notation "x + y" := (@cup (mor _ _) x y) (left associativity, at level 50): ra_terms.
Notation "x ∩ y" := (@cap (mor _ _) x y) (left associativity, at level 40): ra_terms. 
Notation "1" := (one _): ra_terms.
Notation zer n m := (@bot (mor n m)).
Notation top' n m := (@top (mor n m)) (only parsing).
Notation "0" := (zer _ _): ra_terms.
Notation "x °"  := (cnv _ _ x) (left associativity, at level 5, format "x °"): ra_terms.
Notation "x ^+" := (itr _ x)   (left associativity, at level 5, format "x ^+"): ra_terms.
Notation "x ^*" := (str _ x)   (left associativity, at level 5, format "x ^*"): ra_terms.
Notation "x -o y" := (ldv _ _ _ x y) (right associativity, at level 60): ra_terms. 
Notation "y o- x" := (rdv _ _ _ x y) (left associativity, at level 61): ra_terms. 

(** Like for [lattice.ops], we declare most projections as Opaque for
   typeclass resolution, to save on compilation time. *)
#[export] Typeclasses Opaque (* ob mor *) dot one str cnv ldv rdv.

Set Implicit Arguments.
Unset Strict Implicit.

(** * Monoid laws (axioms) *)

(** [laws l X] provides the laws corresponding to the various
   operations of [X], provided these operations belong to the level
   [l]. For instance, the specification of Kleene star ([str]) is
   available only if the level contains [STR].

   Note that [l] indirectly specifies which lattice operations are
   available on each homset, via the field [lattice_laws]. We add
   additional properties when needed (e.g., [dotplsx_]: composition
   ([dot]) distribute over sums ([pls]), provided there are sums)

   The partially ordered categorical structure (leq,weq,dot,one) is
   always present.

   Like for [lattices.laws], some axioms end with an underscore,
   either because they can be strengthened to an equality (e.g.,
   [cnvdot_]), or because they become derivable in presence of other
   axiomes (e.g., [dotx1_]), or both (e.g., [dotplsx_]).

   Unlike for operations ([ops]), laws are actually inferred by
   typeclass resolution. *)

Class laws (l: level) (X: ops) := {
  lattice_laws::       forall n m, lattice.laws l (X n m);
  (** po-monoid laws *)
  dotA:                forall n m p q (x: X n m) y (z: X p q), x⋅(y⋅z) ≡ (x⋅y)⋅z;
  dot1x:               forall n m (x: X n m), 1⋅x ≡ x;
  dotx1_:              CNV ≪ l \/ forall n m (x: X m n), x⋅1 ≡ x;
  dot_leq_:            DIV ≪ l \/ forall n m p, Proper (leq ==> leq ==> leq) (dot n m p);
  (** slo-monoid laws (distribution of ⋅ over + and 0) *)
  dotplsx_  `{CUP ≪ l}: DIV ≪ l \/ forall n m p (x y: X n m) (z: X m p), (x+y)⋅z ≦ x⋅z+y⋅z;
  dotxpls_  `{CUP ≪ l}: DIV ≪ l \/ CNV ≪ l \/ forall n m p (x y: X m n) (z: X p m), z⋅(x+y) ≦ z⋅x+z⋅y;
  dot0x_    `{BOT ≪ l}: DIV ≪ l \/ forall n m p (x: X m p), 0⋅x ≦ zer n p;
  dotx0_    `{BOT ≪ l}: DIV ≪ l \/ CNV ≪ l \/ forall n m p (x: X p m), x⋅0 ≦ zer p n;
  (** converse laws *)
  cnvdot_   `{CNV ≪ l}: forall n m p (x: X n m) (y: X m p), (x⋅y)° ≦ y°⋅x°;
  cnv_invol `{CNV ≪ l}: forall n m (x: X n m), x°° ≡ x;
  cnv_leq   `{CNV ≪ l}::forall n m, Proper (leq ==> leq) (cnv n m);
  cnv_ext_  `{CNV ≪ l}: CAP ≪ l \/ forall n m (x: X n m), x ≦ x⋅x°⋅x;
  (** star laws *)
  str_refl  `{STR ≪ l}: forall n (x: X n n), 1 ≦ x^*;
  str_cons  `{STR ≪ l}: forall n (x: X n n), x⋅x^* ≦ x^*;
  str_ind_l `{STR ≪ l}: forall n m (x: X n n) (z: X n m), x⋅z ≦ z -> x^*⋅z ≦ z;
  str_ind_r_`{STR ≪ l}: DIV ≪ l \/ CNV ≪ l \/ forall n m (x: X n n) (z: X m n), z⋅x ≦ z -> z⋅x^* ≦ z;
  itr_str_l `{STR ≪ l}: forall n (x: X n n), x^+ ≡ x⋅x^*;
  (** modularity law *)
  capdotx   `{AL ≪ l}: forall n m p (x: X n m) (y: X m p) (z: X n p), (x⋅y) ∩ z ≦ x⋅(y ∩ (x°⋅z));
  (** left and right residuals *)
  ldv_spec  `{DIV ≪ l}: forall n m p (x: X n m) (y: X n p) z, z ≦ x -o y <-> x⋅z ≦ y;
  rdv_spec  `{DIV ≪ l}: forall n m p (x: X m n) (y: X p n) z, z ≦ y o- x <-> z⋅x ≦ y
}.

(** * Basic properties *)

#[export] Instance dot_leq `{laws}: forall n m p, Proper (leq ==> leq ==> leq) (dot n m p). 
Proof.
  destruct dot_leq_. 2: assumption. 
  intros n m p x x' Hx y y' Hy. 
  rewrite <-rdv_spec, Hx, rdv_spec. 
  rewrite <-ldv_spec, Hy, ldv_spec. 
  reflexivity.
Qed.

#[export] Instance dot_weq `{laws} n m p: Proper (weq ==> weq ==> weq) (dot n m p) := op_leq_weq_2.

(** ** Basic properties of the converse operation *)

#[export] Instance cnv_weq `{laws} `{CNV ≪ l} n m: Proper (weq ==> weq) (cnv n m) := op_leq_weq_1.

Lemma cnv_leq_iff `{laws} `{CNV ≪ l} n m (x y: X n m): x° ≦ y° <-> x ≦ y. 
Proof. split. intro E. apply cnv_leq in E. now rewrite 2cnv_invol in E. apply cnv_leq. Qed.
Lemma cnv_leq_iff' `{laws} `{CNV ≪ l} n m (x: X n m) y: x ≦ y° <-> x° ≦ y. 
Proof. now rewrite <- cnv_leq_iff, cnv_invol. Qed.

Lemma cnv_weq_iff `{laws} `{CNV ≪ l} n m (x y: X n m): x° ≡ y° <-> x ≡ y. 
Proof. now rewrite 2weq_spec, 2cnv_leq_iff. Qed.
Lemma cnv_weq_iff' `{laws} `{CNV ≪ l} n m (x: X n m) y: x ≡ y° <-> x° ≡ y. 
Proof. now rewrite <-cnv_weq_iff, cnv_invol. Qed.

(** simple tactic to move converse from one side to the other of an (in)equation *)
Ltac cnv_switch := first [
  rewrite cnv_leq_iff |
  rewrite cnv_leq_iff' |
  rewrite <-cnv_leq_iff' |
  rewrite <-cnv_leq_iff |
  rewrite cnv_weq_iff |
  rewrite cnv_weq_iff' |
  rewrite <-cnv_weq_iff' |
  rewrite <-cnv_weq_iff ].

Lemma cnvdot `{laws} `{CNV ≪ l} n m p (x: X n m) (y: X m p): (x⋅y)° ≡ y°⋅x°.
Proof. apply antisym. apply cnvdot_. cnv_switch. now rewrite cnvdot_, 2cnv_invol. Qed.

Lemma cnv1 `{laws} `{CNV ≪ l} n: (one n)° ≡ 1.
Proof. rewrite <- (dot1x (1°)). cnv_switch. now rewrite cnvdot, cnv_invol, dot1x. Qed.

Lemma cnvpls `{laws} `{CNV+CUP ≪ l} n m (x y: X n m): (x+y)° ≡ x°+y°.
Proof.
  apply antisym.
  cnv_switch. apply leq_cupx; cnv_switch; lattice.
  apply leq_cupx; cnv_switch; lattice.
Qed.

Lemma cnvcap `{laws} `{AL ≪ l} n m (x y: X n m): (x ∩ y)° ≡ x° ∩ y°.
Proof.
  apply antisym. 
  apply leq_xcap; apply cnv_leq; lattice.
  cnv_switch. apply leq_xcap; cnv_switch; lattice.
Qed.

Lemma cnv0 `{laws} `{CNV+BOT ≪ l} n m: (zer n m)° ≡ 0.
Proof. apply antisym; [cnv_switch|]; apply leq_bx. Qed.

Lemma cnvtop `{laws} `{CNV+TOP ≪ l} n m: (top: X n m)° ≡ top.
Proof. apply antisym; [|cnv_switch]; apply leq_xt. Qed.

Lemma cnvneg `{laws} `{CNV+BL ≪ l} n m (x: X n m): (neg x)° ≡ neg (x°).
Proof.
  apply neg_unique. 
  rewrite <-cnvpls, cupC, cupneg. now rewrite cnvtop.
  rewrite <-cnvcap, capC, capneg. now rewrite cnv0.
Qed.

(** ** Basic properties of composition *)

Lemma dotx1 `{laws} n m (x: X m n): x⋅1 ≡ x.
Proof. destruct dotx1_; trivial. cnv_switch. now rewrite cnvdot, cnv1, dot1x. Qed.

Lemma dotplsx `{laws} `{CUP ≪ l} n m p (x y: X n m) (z: X m p): (x+y)⋅z ≡ x⋅z+y⋅z.
Proof. 
  apply antisym. 2: apply leq_cupx; apply dot_leq; lattice. 
  destruct dotplsx_ as [Hl|E]. 2: apply E.
  rewrite <-rdv_spec. apply leq_cupx; rewrite rdv_spec; lattice.
Qed.

Lemma dotxpls `{laws} `{CUP ≪ l} n m p (x y: X m n) (z: X p m): z⋅(x+y) ≡ z⋅x+z⋅y.
Proof. 
  apply antisym. 2: apply leq_cupx; apply dot_leq; lattice. 
  destruct dotxpls_ as [Hl|[Hl|E]]. 
   rewrite <-ldv_spec. apply leq_cupx; rewrite ldv_spec; lattice.
   cnv_switch. rewrite cnvpls,3cnvdot,cnvpls. apply weq_leq, dotplsx. 
  apply E. 
Qed.

Lemma dot0x `{laws} `{BOT ≪ l} n m p (x: X m p): 0⋅x ≡ zer n p.
Proof.
  apply antisym. 2: apply leq_bx. 
  destruct dot0x_ as [Hl|E]. 2: apply E. 
  rewrite <-rdv_spec. apply leq_bx.
Qed.

Lemma dotx0 `{laws} `{BOT ≪ l} n m p (x: X p m): x⋅0 ≡ zer p n.
Proof. 
  apply antisym. 2: apply leq_bx. 
  destruct dotx0_ as [Hl|[Hl|E]]. 
   rewrite <-ldv_spec. apply leq_bx.
   cnv_switch. rewrite cnvdot,2cnv0. apply weq_leq, dot0x.
  apply E.
Qed.

Lemma dotxcap `{laws} `{CAP ≪ l} n m p (x: X n m) (y z: X m p): 
  x ⋅ (y ∩ z) ≦ (x⋅y) ∩ (x⋅z). 
Proof. apply leq_xcap; apply dot_leq; lattice. Qed.

Lemma cnv_ext `{laws} `{CNV ≪ l} n m (x: X n m): x ≦ x⋅x°⋅x.
Proof. 
  destruct cnv_ext_; trivial.
  transitivity ((x⋅1) ∩ x). rewrite dotx1. lattice.
  rewrite capdotx, <-dotA. apply dot_leq; lattice.
Qed.

Lemma capxdot `{laws} `{AL ≪ l} n m p (x: X m n) (y: X p m) (z: X p n):
  (y⋅x) ∩ z ≦ (y ∩ (z⋅x°))⋅x.
Proof. cnv_switch. now rewrite cnvdot, 2cnvcap, 2cnvdot, capdotx. Qed.

(** ** Basic properties of left division *)

(** only those properties that are required to derive [str_ind_r] out
   of divisions, see module [factor] for other properties *)

Lemma ldv_cancel `{laws} `{DIV ≪ l} n m p (x: X n m) (y: X n p): x⋅(x -o y) ≦ y.
Proof. now rewrite <-ldv_spec. Qed.

Lemma ldv_trans `{laws} `{DIV ≪ l} n m p q (x: X n m) (y: X n p) (z: X n q): 
  (x -o y)⋅(y -o z) ≦ x -o z.
Proof. now rewrite ldv_spec, dotA, 2ldv_cancel. Qed.

Lemma leq_ldv `{laws} `{DIV ≪ l} n m (x y: X n m): x ≦ y <-> 1 ≦ x -o y. 
Proof. now rewrite ldv_spec, dotx1. Qed.

Lemma ldv_xx `{laws} `{DIV ≪ l} n m (x: X n m): 1 ≦ x -o x.
Proof. now rewrite <-leq_ldv. Qed.

#[export] Instance ldv_leq `{laws} `{DIV ≪ l} n m p: Proper (leq --> leq ++> leq) (ldv n m p).
Proof. intros x x' Hx y y' Hy. now rewrite ldv_spec, <-Hx, <-Hy, <-ldv_spec. Qed.

#[export] Instance ldv_weq `{laws} `{DIV ≪ l} n m p: Proper (weq ==> weq ==> weq) (ldv n m p).
Proof. simpl. setoid_rewrite weq_spec. split; apply ldv_leq; tauto. Qed.

Lemma cnvldv `{laws} `{CNV+DIV ≪ l} n m p (x: X n m) (y: X n p): (x -o y)° ≡ y° o- x°.
Proof.
  apply from_below. intro z. 
  cnv_switch. rewrite ldv_spec.
  cnv_switch. rewrite cnvdot, cnv_invol. 
  now rewrite rdv_spec. 
Qed.

(** ** Schroeder rules  *)
Lemma Schroeder_  `{laws} `{BL+CNV ≪ l} n m p (x : X n m) (y : X m p) (z : X n p): 
  x°⋅!z ≦ !y -> x⋅y ≦ z.
Proof.
  intro E. apply leq_cap_neg in E. rewrite negneg in E. 
  apply leq_cap_neg. now rewrite capdotx, capC, E, dotx0. 
Qed.

Lemma Schroeder_l `{laws} `{BL+CNV ≪ l} n m p (x : X n m) (y : X m p) (z : X n p): 
  x⋅y ≦ z <-> x°⋅!z ≦ !y. 
Proof.
  split. 2: apply Schroeder_. intro.
  apply Schroeder_. now rewrite 2negneg, cnv_invol. 
Qed.

(** ** Basic properties of Kleene star *)
(** (more properties in [kleene]) *)

Lemma str_ext `{laws} `{STR ≪ l} n (x: X n n): x ≦ x^*.
Proof. now rewrite <-str_cons, <-str_refl, dotx1. Qed.

Lemma str_ind_l' `{laws} `{STR ≪ l} n m (x: X n n) (y z: X n m): y ≦ z -> x⋅z ≦ z -> x^*⋅y ≦ z.
Proof. intro E. rewrite E. apply str_ind_l. Qed.

Lemma str_ind_l1 `{laws} `{STR ≪ l} n (x z: X n n): 1 ≦ z -> x⋅z ≦ z -> x^* ≦ z.
Proof. rewrite <-(dotx1 (x^*)). apply str_ind_l'. Qed.

#[export] Instance str_leq `{laws} `{STR ≪ l} n: Proper (leq ==> leq) (str n).
Proof.
  intros x y E. apply str_ind_l1. apply str_refl. 
  rewrite E. apply str_cons.
Qed.

#[export] Instance str_weq `{laws} `{STR ≪ l} n: Proper (weq ==> weq) (str n) := op_leq_weq_1.

Lemma str_snoc `{laws} `{STR ≪ l} n (x: X n n): x^*⋅x ≦ x^*.
Proof. apply str_ind_l'. apply str_ext. apply str_cons. Qed.

Lemma str_unfold_l `{laws} `{KA ≪ l} n (x: X n n): x^* ≡ 1+x⋅x^*.
Proof. 
  apply antisym. apply str_ind_l1. lattice. 
  rewrite dotxpls. apply leq_cupx. rewrite <-str_refl. lattice.
  rewrite <-str_cons at 2. lattice.
  rewrite str_cons, (str_refl x). lattice.
Qed. 

Lemma str_itr `{laws} `{KA ≪ l} n (x: X n n): x^* ≡ 1+x^+.
Proof. rewrite itr_str_l. apply str_unfold_l. Qed.

Lemma cnvstr_ `{laws} `{CNV+STR ≪ l} n (x: X n n): x^*° ≦ x°^*.
Proof.
  cnv_switch. apply str_ind_l1. now rewrite <-str_refl, cnv1.  
  cnv_switch. rewrite cnvdot, cnv_invol. apply str_snoc. 
Qed.

Lemma str_ldv_ `{laws} `{STR+DIV ≪ l} n m (x: X m n): (x -o x)^* ≦ x -o x.
Proof. apply str_ind_l1. apply ldv_xx. apply ldv_trans. Qed.

Lemma str_ind_r `{laws} `{STR ≪ l} n m (x: X n n) (z: X m n): z⋅x ≦ z -> z⋅x^* ≦ z.
Proof. 
  destruct str_ind_r_ as [Hl|[Hl|?]]. 3: auto. 
  - rewrite <-2ldv_spec. intro E. apply str_leq in E. rewrite E. apply str_ldv_.
  - intros. cnv_switch. rewrite cnvdot, cnvstr_. 
    apply str_ind_l; cnv_switch; now rewrite cnvdot, 2cnv_invol.
Qed.

Lemma itr_move `{laws} `{STR ≪ l} n (x: X n n): x ⋅ x^* ≡ x^* ⋅ x.
Proof.
  apply antisym. 
   rewrite <-dot1x, (str_refl x), dotA. apply str_ind_r. now rewrite str_snoc at 1. 
   apply str_ind_l'. now rewrite <-str_refl, dotx1. now rewrite str_cons at 1.
Qed.

Lemma itr_str_r `{laws} `{STR ≪ l} n (x: X n n): x^+ ≡ x^* ⋅ x.
Proof. rewrite itr_str_l. apply itr_move. Qed.

(** * Subtyping / weakening *)  

(** laws that hold at any level [h] hold for all level [k ≪ h]  *)
Lemma lower_laws {h k} {X} {H: laws h X} {le: k ≪ h}: laws k X.
Proof. 
  constructor; [ intros; apply lower_lattice_laws | .. ]; 
    try solve [ apply H | intro; apply H; eauto using lower_trans ].
  right. apply dotx1. 
  right. apply dot_leq. 
  intro H'. right. intros. apply weq_leq. apply (lower_trans _ _ _ H') in le. apply dotplsx.
  intro H'. right. right. intros. apply weq_leq. apply (lower_trans _ _ _ H') in le. apply dotxpls.
  intro H'. right. intros. apply weq_leq. apply (lower_trans _ _ _ H') in le. apply dot0x.
  intro H'. right. right. intros. apply weq_leq. apply (lower_trans _ _ _ H') in le. apply dotx0.
  intro H'. right. intros. apply (lower_trans _ _ _ H') in le. apply cnv_ext.
  intro H'. right. right. apply (lower_trans _ _ _ H') in le. apply str_ind_r.
Qed.

(** * Reasoning by duality *)

(** dual monoid operations: we reverse all arrows (or morphisms), swap
   the arguments of [dot], and swap left and right residuals.

   Note that this corresponds to categorical duality, not to be
   confused with lattice duality, as defined in [lattice.dual]. *)
Definition dual (X: ops) := {|
  ob := ob X;
  mor n m := X m n;
  dot n m p x y := y⋅x;
  one := one;
  cnv n m := cnv m n;
  itr := itr;
  str := str;
  ldv := rdv;
  rdv := ldv
|}.
Notation "X ^op" := (dual X) (at level 1): ra_scope.

(** laws on a given structure can be transferred to the dual one *)
Lemma dual_laws l X (L: laws l X): laws l X^op.
Proof.
  constructor; simpl; repeat right; intros.
   apply lattice_laws.
   symmetry. apply dotA.
   apply dotx1.
   apply dot1x.
   now apply dot_leq.
   apply weq_leq, dotxpls.
   apply weq_leq, dotplsx.
   apply weq_leq, dotx0.
   apply weq_leq, dot0x.
   apply weq_leq, cnvdot.
   apply cnv_invol.
   now apply cnv_leq.
   rewrite dotA. apply cnv_ext.
   apply str_refl.
   apply str_snoc.
   now apply str_ind_r.
   now apply str_ind_l.
   apply itr_str_r.
   apply capxdot.
   apply rdv_spec. 
   apply ldv_spec. 
Qed.

(** this gives us a tactic to prove properties by categorical duality *)
Lemma dualize {h} {P: ops -> Prop} (L: forall l X, laws l X -> h ≪ l -> P X) 
  {l X} {H: laws l X} {Hl:h ≪ l}: P X^op.
Proof. eapply L. apply dual_laws, H. assumption. Qed.

Ltac dual x := apply (dualize x).

(** the following are examples of the benefits of such dualities *)
#[export] Instance rdv_leq `{laws} `{DIV ≪ l} n m p: Proper (leq --> leq ++> leq) (rdv n m p).
Proof. dual @ldv_leq. Qed.

#[export] Instance rdv_weq `{laws} `{DIV ≪ l} n m p: Proper (weq ==> weq ==> weq) (rdv n m p).
Proof. dual @ldv_leq. Qed.

#[export] Instance rdv_weq `{laws} `{DIV ≪ l} n m p: Proper (weq ==> weq ==> weq) (rdv n m p).
Proof. dual @ldv_weq. Qed.

Lemma cnvrdv `{laws} `{CNV+DIV ≪ l} n m p (x: X m n) (y: X p n): (y o- x)° ≡ x° -o y°.
Proof. dual @cnvldv. Qed.

Lemma dotcapx `{laws} `{CAP ≪ l} n m p (x: X m n) (y z: X p m): (y ∩ z) ⋅ x ≦ (y⋅x) ∩ (z⋅x). 
Proof. dual @dotxcap. Qed.

Lemma Schroeder_r `{laws} `{BL+CNV ≪ l} n m p (x : X n m) (y : X m p) (z : X n p): 
  x⋅y ≦ z <-> !z⋅y° ≦ !x.
Proof. dual @Schroeder_l. Qed.

(** * Functors (i.e., monoid morphisms) *)

Class functor l {X Y: ops} (f': ob X -> ob Y) (f: forall {n m}, X n m -> Y (f' n) (f' m)) := {
  fn_morphism::     forall n m, morphism l (@f n m);
  fn_dot:           forall n m p (x: X n m) (y: X m p), f (x⋅y) ≡ f x ⋅ f y;
  fn_one:           forall n, f (one n) ≡ 1;
  fn_itr `{STR ≪ l}: forall n (x: X n n), f (x^+) ≡ (f x)^+;
  fn_str `{STR ≪ l}: forall n (x: X n n), f (x^*) ≡ (f x)^*;
  fn_cnv `{CNV ≪ l}: forall n m (x: X n m), f (x°) ≡ (f x)°;
  fn_ldv `{DIV ≪ l}: forall n m p (x: X n m) (y: X n p), f (x -o y) ≡ f x -o f y;
  fn_rdv `{DIV ≪ l}: forall n m p (x: X m n) (y: X p n), f (y o- x) ≡ f y o- f x
}.

(** generating a structure by faithful embedding *)

Lemma laws_of_faithful_functor {h l X Y} {L: laws h Y} {Hl: l ≪ h} f' f:
  @functor l X Y f' f -> 
  (forall n m x y, f n m x ≦ f n m y -> x ≦ y) ->
  (forall n m x y, f n m x ≡ f n m y -> x ≡ y) ->
  laws l X.
  intros Hf Hleq Hweq.
  assert (Hleq_iff: forall n m x y, f n m x ≦ f n m y <-> x ≦ y).
   split. apply Hleq. apply fn_leq.
  assert (Hweq_iff: forall n m x y, f n m x ≡ f n m y <-> x ≡ y).
   split. apply Hweq. apply fn_weq.
  assert (L' := @lower_laws _ _ _ L Hl).
  constructor; repeat right; intro_vars. 
   apply (laws_of_injective_morphism (f n m)); auto using fn_morphism.
   rewrite <-Hweq_iff, 4fn_dot. apply dotA. 
   rewrite <-Hweq_iff, fn_dot, fn_one. apply dot1x. 
   rewrite <-Hweq_iff, fn_dot, fn_one. apply dotx1. 
   repeat intro. apply Hleq. rewrite 2fn_dot. now apply dot_leq; apply Hleq_iff. 
   apply Hleq. now rewrite fn_cup, 3fn_dot, fn_cup, dotplsx. 
   apply Hleq. now rewrite fn_cup, 3fn_dot, fn_cup, dotxpls. 
   apply Hleq. now rewrite fn_dot, 2fn_bot, dot0x. 
   apply Hleq. now rewrite fn_dot, 2fn_bot, dotx0.
   intro. apply Hleq. now rewrite fn_cnv, 2fn_dot, 2fn_cnv, cnvdot.
   intro. rewrite <-Hweq_iff, 2fn_cnv. apply cnv_invol.
   repeat intro. apply Hleq. rewrite 2fn_cnv. now apply cnv_leq; apply Hleq_iff. 
   apply Hleq. rewrite 2fn_dot,fn_cnv. apply cnv_ext.
   intro. apply Hleq. rewrite fn_one, fn_str. apply str_refl.
   intro. apply Hleq. rewrite fn_str, fn_dot, fn_str. apply str_cons.
   intro. rewrite <-2Hleq_iff, 2fn_dot, fn_str. apply str_ind_l.
   rewrite <-2Hleq_iff, 2fn_dot, fn_str. apply str_ind_r.
   intro. apply Hweq. rewrite fn_itr, fn_dot, fn_str. apply itr_str_l.
   intro. apply Hleq. rewrite fn_cap,2fn_dot,fn_cap,fn_dot,fn_cnv. apply capdotx.
   intro. rewrite <-2Hleq_iff, fn_dot, fn_ldv. apply ldv_spec. 
   intro. rewrite <-2Hleq_iff, fn_dot, fn_rdv. apply rdv_spec. 
Qed.

(** injection from Booleans into monoids (actually a functor, although we don't need it) *)
Definition ofbool {X: ops} {n} (a: bool): X n n := if a then 1 else 0.
Global Arguments ofbool {_ _} !_ /.
(* does not respect the uniform inheritance condition *)
(* Coercion ofbool: bool >-> car. *)

(** ML modules *)
(* loading this one here explicitly enforces the dependency for proper compilation *)
Declare ML Module "coq-relation-algebra.common". 
Declare ML Module "coq-relation-algebra.fold".

(** tricks for reification  *)
Lemma catch_weq `{L: laws} n m (x y: X n m): 
  (let L:=L in x <=[false]= y) -> x ≡ y.
Proof. trivial. Defined.
Lemma catch_leq `{L: laws} n m (x y: X n m): 
  (let L:=L in x <=[true]= y) -> x ≦ y.
Proof. trivial. Defined.

Ltac catch_rel := apply catch_weq || apply catch_leq.

End monoid.

End RelationAlgebra_DOT_monoid_WRAPPED.
Module Export RelationAlgebra_DOT_monoid.
Module Export RelationAlgebra.
Module monoid.
Include RelationAlgebra_DOT_monoid_WRAPPED.monoid.
End monoid.

End RelationAlgebra.

End RelationAlgebra_DOT_monoid.
Require Coq.Lists.List.
Set Implicit Arguments.

Inductive reflect (P: Prop): bool -> Set :=
| reflect_t : P -> reflect P true
| reflect_f : ~ P -> reflect P false.

Inductive compare_spec (P: Prop): comparison -> Set :=
| compare_eq: P -> compare_spec P Eq
| compare_lt: ~P -> compare_spec P Lt
| compare_gt: ~P -> compare_spec P Gt.
Definition eqb_of_compare A (f: A -> A -> comparison): A -> A -> bool.
Admitted.

Lemma eqb_of_compare_spec A f:
  (forall a b: A, compare_spec (a=b) (f a b)) ->
  forall a b, reflect (a=b) (eqb_of_compare f a b).
Admitted.

Notation lex a b := match a with Eq => b | Lt => Lt | Gt => Gt end.

Structure cmpType := mk_cmp {
  carr:> Set;
  eqb: carr -> carr -> bool;
  _: forall x y, reflect (x=y) (eqb x y);
  cmp: carr -> carr -> comparison;
  _: forall x y, compare_spec (x=y) (cmp x y)
}.
Arguments cmp {c} x y.

Definition mk_simple_cmp A cmp cmp_spec :=
  @mk_cmp A _ (eqb_of_compare_spec _ cmp_spec) cmp cmp_spec.

Fixpoint eqb_nat i j :=
  match i,j with
    | O,O => true
    | S i,S j=> eqb_nat i j
    | _,_ => false
  end.
Fixpoint nat_compare i j :=
  match i,j with
    | O,O => Eq
    | S i,S j=> nat_compare i j
    | O,_ => Lt
    | _,O => Gt
  end.

Import RelationAlgebra.common.

Record ord n := Ord {nat_of_ord:> nat; ord_lt: nat_of_ord<n}.

Definition eqb_ord {n} (i j: ord n) := eqb_nat i j.

Lemma eqb_ord_spec n (i j: ord n): reflect (i=j) (eqb_ord i j).
Admitted.

Definition ord_compare {n} (i j: ord n) := nat_compare i j.
Lemma ord_compare_spec n (i j: ord n): compare_spec (i=j) (ord_compare i j).
Admitted.

Canonical Structure cmp_ord n := mk_cmp _ (@eqb_ord_spec n) _ (@ord_compare_spec n).

Module Export set.

Fixpoint od x :=
  match x with
    | O => (false,O)
    | S O => (true,O)
    | S (S x) => let (o,x) := od x in (o,S x)
  end.

Fixpoint mem' n x :=
  match n with
    | 0 => fun i => assert_false false
    | S n =>
      let (o,x) := od x in
      let f := mem' n x in
      fun i => match i with O => o | S i => f i end
  end.
Definition mem n (x: ord (pow2 n)) (i: ord n) := mem' n x i.
Import RelationAlgebra.lattice.
Export Coq.Lists.List.
Export ListNotations.

Universe lset.

Canonical Structure lset_ops (A:Type@{lset}) := lattice.mk_ops (list A)
  (fun h k => forall a, In a h -> In a k)
  (fun h k => forall a, In a h <-> In a k)
  (@app A) (@app A) (assert_false id) (@nil A) (@nil A).

Section m.
 Context {A: cmpType}.

 Fixpoint union (l1: list A) :=
   match l1 with
     | nil => fun l2 => l2
     | h1::t1 =>
       let fix union' l2 :=
         match l2 with
           | nil => l1
           | h2::t2 =>
             match cmp h1 h2 with
               | Eq => h1::union t1 t2
               | Lt => h1::union t1 l2
               | Gt => h2::union' t2
             end
         end
         in union'
   end.

 Lemma union_app: forall h k, union h k ≡ h ++ k.
Admitted.

End m.

Section s.
Context `{L:laws} `{Hl:BSL ≪ l}.

Universe S.

Section i.

Context {I: Type@{S}}.

Fixpoint sup (f: I -> X) J :=
  match J with
    | nil => bot
    | cons i J => f i ⊔ sup f J
  end.

Lemma sup_app f h k: sup f (h++k) ≡ sup f h ⊔ sup f k.
Admitted.

Lemma sup_singleton f i: sup f (i::nil) ≡ f i.
Admitted.

Global Instance sup_weq: Proper (pwr weq ==> weq ==> weq) sup.
Admitted.

End i.

Lemma sup_map I J (f: J -> X) (m: I -> J) I':
  sup f (map m I') = sup (fun i => f (m i)) I'.
Admitted.

End s.

Import RelationAlgebra.monoid.

Notation "\sum_ ( i \in l ) f" := (@sup (mor _ _) _ (fun i => f) l)
  (at level 41, f at level 41, i, l at level 50,
    format "'[' \sum_ ( i \in  l ) '/  '  f ']'"): ra_terms.

Lemma dotsumx `{laws} `{BSL ≪ l} I J n m p (f: I -> X n m) (x: X m p):
  (\sum_(i\in J) f i) ⋅ x ≡ \sum_(i\in J) (f i ⋅ x).
Admitted.

Export Coq.Numbers.BinNums.

Fixpoint eqb_pos i j :=
  match i,j with
    | xH,xH => true
    | xI i,xI j | xO i, xO j => eqb_pos i j
    | _,_ => false
  end.

Lemma eqb_pos_spec: forall i j, reflect (i=j) (eqb_pos i j).
Admitted.

Fixpoint pos_compare i j :=
  match i,j with
    | xH, xH => Eq
    | xO i, xO j | xI i, xI j => pos_compare i j
    | xH, _ => Lt
    | _, xH => Gt
    | xO _, _ => Lt
    | _,_ => Gt
  end.

Lemma pos_compare_spec: forall i j, compare_spec (i=j) (pos_compare i j).
Admitted.

Canonical Structure cmp_pos := mk_cmp _ eqb_pos_spec _ pos_compare_spec.
Canonical Structure Prop_lattice_ops: lattice.ops.
exact ({|
  leq := impl;
  weq := iff;
  cup := or;
  cap := and;
  neg := not;
  bot := False;
  top := True
|}).
Defined.

Section l.

Variable State: Type.
Notation Sigma := positive.

Inductive trace :=
| tnil (a: State)
| tcons (a: State) (i: Sigma) (w: trace).

Definition traces := trace -> Prop.

Canonical Structure traces_lattice_ops :=
  lattice.mk_ops traces leq weq cup cap neg bot top.

CoInductive traces_unit := traces_tt.
Definition traces_dot (n m p: traces_unit) (x y: traces): traces.
Admitted.
Definition traces_ldv (n m p: traces_unit) (x y: traces): traces.
Admitted.
Definition traces_rdv (n m p: traces_unit) (x y: traces): traces.
Admitted.
Definition traces_one (n: traces_unit): traces.
Admitted.
Definition traces_cnv (n m: traces_unit) (x: traces): traces.
Admitted.
Definition traces_itr (n: traces_unit) (x: traces): traces.
Admitted.
Definition traces_str (n: traces_unit) (x: traces): traces.
Admitted.

Canonical Structure traces_monoid_ops :=
  monoid.mk_ops _ (fun _ _ => traces_lattice_ops)
  traces_dot traces_one traces_itr traces_str traces_cnv traces_ldv traces_rdv.

End l.
Import RelationAlgebra.lattice.

Section s.
Variable A: Set.

Inductive expr :=
| e_bot
| e_top
| e_cup (e f: expr)
| e_cap (e f: expr)
| e_neg (e: expr)
| e_var (a: A).

Section e.
Context {X: ops}.
Variable f: A -> X.

Fixpoint eval e: X :=
  match e with
    | e_bot => bot
    | e_top => top
    | e_cup x y => eval x ⊔ eval y
    | e_cap x y => eval x ⊓ eval y
    | e_neg x => ! eval x
    | e_var a => f a
  end.
End e.

Section l.
Variable l: level.

Definition e_leq (x y: expr) := forall X (L: laws l X) (f: A -> X), eval f x ≦ eval f y.
Definition e_weq (x y: expr) := forall X (L: laws l X) (f: A -> X), eval f x ≡ eval f y.

Canonical Structure expr_ops := {|
  car := expr;
  leq := e_leq;
  weq := e_weq;
  cup := e_cup;
  cap := e_cap;
  neg := e_neg;
  bot := e_bot;
  top := e_top
|}.

End l.

End s.
Arguments e_bot {A}.
Arguments e_top {A}.

Section expr_cmp.
Context {A: cmpType}.
Fixpoint expr_compare (x y: expr A) :=
  match x,y with
    | e_bot, e_bot
    | e_top, e_top => Eq
    | e_var a, e_var b => cmp a b
    | e_cup x x', e_cup y y'
    | e_cap x x', e_cap y y' => lex (expr_compare x y) (expr_compare x' y')
    | e_neg x, e_neg y => expr_compare x y
    | e_bot, _      => Lt
    | _, e_bot      => Gt
    | e_top, _      => Lt
    | _, e_top      => Gt
    | e_var _, _    => Lt
    | _, e_var _    => Gt
    | e_cup _ _, _  => Lt
    | _, e_cup _ _  => Gt
    | e_cap _ _, _  => Lt
    | _, e_cap _ _  => Gt
  end.

Lemma expr_compare_spec: forall x y, compare_spec (x=y) (expr_compare x y).
Admitted.

Canonical Structure cmp_expr := mk_simple_cmp _ expr_compare_spec.
End expr_cmp.

Module Export ugregex.

Section l.
Variable Pred: nat.
Notation Sigma := positive.
Notation Atom := (ord (pow2 Pred)).
Notation uglang := (traces_monoid_ops Atom traces_tt traces_tt).

Inductive ugregex :=
| u_var(i: Sigma)
| u_prd(p: expr (ord Pred))
| u_pls(e f: ugregex)
| u_dot(e f: ugregex)
| u_itr(e: ugregex).

Definition u_zer := u_prd e_bot.
Definition u_one := u_prd e_top.
Definition u_str e := u_pls u_one (u_itr e).
Fixpoint lang (e: ugregex): uglang.
Admitted.

Definition u_leq e f := lang e ≦ lang f.
Definition u_weq e f := lang e ≡ lang f.

Canonical Structure ugregex_lattice_ops :=
  lattice.mk_ops _ u_leq u_weq u_pls u_pls id u_zer u_zer.

CoInductive ugregex_unit := ugregex_tt.

Canonical Structure ugregex_monoid_ops :=
  monoid.mk_ops ugregex_unit _
  (fun _ _ _ => u_dot) (fun _ => u_one) (fun _ => u_itr) (fun _ => u_str)
  (fun _ _ _ => u_zer) (fun _ _ _ _ _ => u_zer) (fun _ _ _ _ _ => u_zer).

Notation tt := ugregex_tt.
Notation ugregex' := (ugregex_monoid_ops tt tt).

Global Instance ugregex_monoid_laws: monoid.laws BKA ugregex_monoid_ops.
Admitted.

Global Instance ugregex_lattice_laws: lattice.laws BKA ugregex_lattice_ops.
Admitted.

Fixpoint epsilon_pred a (e: expr_ops (ord Pred) BL) :=
  match e with
    | e_bot => false
    | e_top => true
    | e_var i => a i
    | e_cup e f => epsilon_pred a e ||| epsilon_pred a f
    | e_cap e f => epsilon_pred a e &&& epsilon_pred a f
    | e_neg e => negb (epsilon_pred a e)
  end.

Fixpoint epsilon a (e: ugregex) :=
  match e with
    | u_var _ => false
    | u_prd p => epsilon_pred a p
    | u_pls e f => epsilon a e ||| epsilon a f
    | u_dot e f => epsilon a e &&& epsilon a f
    | u_itr e => epsilon a e
  end.

Fixpoint deriv a i (e: ugregex'): ugregex' :=
  match e with
    | u_prd _ => 0
    | u_var j => ofbool (eqb_pos i j)
    | u_pls e f => deriv a i e + deriv a i f
    | u_dot e f => deriv a i e ⋅ f + ofbool (epsilon (set.mem a) e) ⋅ deriv a i f
    | u_itr e => deriv a i e ⋅ (e: ugregex')^*
  end.

Fixpoint ugregex_compare (x y: ugregex) :=
  match x,y with
    | u_prd a, u_prd b
    | u_var a, u_var b       => cmp a b
    | u_pls x x', u_pls y y'
    | u_dot x x', u_dot y y' => lex (ugregex_compare x y) (ugregex_compare x' y')
    | u_itr x, u_itr y       => ugregex_compare x y
    | u_var _, _             => Lt
    | _, u_var _             => Gt
    | u_prd _, _             => Lt
    | _, u_prd _             => Gt
    | u_itr _ , _            => Lt
    | _, u_itr _             => Gt
    | u_pls _ _ , _          => Lt
    | _, u_pls _ _           => Gt
  end.

Lemma ugregex_compare_spec x y: compare_spec (x=y) (ugregex_compare x y).
Admitted.

Canonical Structure ugregex_cmp := mk_simple_cmp _ ugregex_compare_spec.

End l.

End ugregex.
Variable Pred: nat.
Notation tt := ugregex_tt.
Notation ugregex := (ugregex_monoid_ops Pred tt tt).

Ltac fold_ugregex_type := change (@ugregex.ugregex Pred) with (@car ugregex) in *.
Ltac fold_ugregex := ra_fold ugregex_monoid_ops tt; fold_ugregex_type.

Notation tod e := (fun f => u_dot f e) (only parsing).

Fixpoint pderiv a i (e: ugregex): list ugregex :=
  match e with
    | u_prd _ => []
    | u_var _ j => if eqb_pos i j then [u_one _] else []
    | u_pls e f => union (pderiv a i e) (pderiv a i f)
    | u_dot e f =>
        if epsilon a e then union (map (tod f) (pderiv a i e)) (pderiv a i f)
        else map (tod f) (pderiv a i e)
    | u_itr e => map (tod (u_str e)) (pderiv a i e)
  end.

Lemma deriv_eq a i e: deriv a i e ≡ sup id (pderiv (set.mem a) i e).
Proof.
  induction e; simpl; fold_ugregex.
   case eqb_pos.
2: reflexivity.
now rewrite sup_singleton.
   reflexivity.
   rewrite union_app, sup_app.
now apply cup_weq.
   assert (H: deriv a i e1 ⋅ e2 ≡ sup id (map (tod e2) (pderiv (set.mem a) i e1))).
    rewrite sup_map.
setoid_rewrite <-(dotsumx (X:=ugregex_monoid_ops _)).
    now apply dot_weq.
   case epsilon.
    rewrite union_app, sup_app.
    setoid_rewrite dot1x.
now apply cup_weq.
    setoid_rewrite dot0x.
now rewrite cupxb.
   rewrite sup_map.
setoid_rewrite <-(dotsumx (X:=ugregex_monoid_ops _)).
    now apply dot_weq.
Qed.
EOF
coqc -q bug.v

coqbot-app[bot] commented 6 months ago

Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.

coqbot-app[bot] commented 6 months ago

@JasonGross, Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/bug.v (full log on GitHub Actions - verbose log)

:star2: 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-disabled" "-native-compiler" "ondemand" "-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/Ltac2" "Ltac2" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/RelationAlgebra" "RelationAlgebra" "-top" "Top.bug_01") -*- *) (* File reduced by coq-bug-minimizer from original input, then from 380 lines to 52 lines, then from 65 lines to 348 lines, then from 348 lines to 157 lines, then from 170 lines to 308 lines, then from 312 lines to 157 lines, then from 170 lines to 391 lines, then from 393 lines to 234 lines, then from 247 lines to 890 lines, then from 881 lines to 268 lines, then from 281 lines to 347 lines, then from 352 lines to 278 lines, then from 291 lines to 371 lines, then from 374 lines to 303 lines, then from 316 lines to 371 lines, then from 376 lines to 310 lines, then from 323 lines to 582 lines, then from 581 lines to 344 lines, then from 357 lines to 519 lines, then from 522 lines to 376 lines, then from 389 lines to 790 lines, then from 789 lines to 409 lines, then from 422 lines to 669 lines, then from 666 lines to 452 lines, then from 465 lines to 1009 lines, then from 727 lines to 42 lines, then from 55 lines to 662 lines, then from 652 lines to 60 lines, then from 73 lines to 263 lines, then from 268 lines to 79 lines, then from 92 lines to 212 lines, then from 211 lines to 81 lines, then from 86 lines to 83 lines *) (* coqc version 8.20+alpha compiled with OCaml 4.13.1 coqtop version buildkitsandbox:/home/coq/.opam/4.13.1+flambda/.opam-switch/build/coq-core.dev/_build/default,master (e05a8eea9fafd242a1e41272d8f9dbbcdabca1e5) Expected coqc runtime on this file: 0.123 sec *) Require Coq.Setoids.Setoid. Export Coq.Setoids.Setoid. Notation "a <<< b" := (if (a:bool) then (b:bool) else true) (at level 49). Notation "a &&& b" := (if (a:bool) then (b:bool) else false) (right associativity, at level 59). Record level := mk_level { has_cup: bool; has_bot: bool; has_cap: bool; has_top: bool; has_str: bool; has_cnv: bool; has_neg: bool; has_div: bool }. Class lower (k k': level) := mk_lower: let 'mk_level a b c d e f g h := k in let 'mk_level a' b' c' d' e' f' g' h' := k' in is_true (a<< car -> car; cap: car -> car -> car; neg: car -> car; bot: car; top: car }. Coercion car: ops >-> Sortclass. Infix "≡" := weq (at level 79): ra_scope. End lattice. Universe M. Class ops := mk_ops { ob: Type@{M}; mor: ob -> ob -> lattice.ops; dot: forall n m p, mor n m -> mor m p -> mor n p; one: forall n, mor n n; itr: forall n, mor n n -> mor n n; str: forall n, mor n n -> mor n n; cnv: forall n m, mor n m -> mor m n; ldv: forall n m p, mor n m -> mor n p -> mor m p; rdv: forall n m p, mor m n -> mor p n -> mor p m }. Notation "x ⋅ y" := (dot _ _ _ x y) (left associativity, at level 25, format "x ⋅ y"): ra_terms. Class laws (l: level) (X: ops) := { lattice_laws:: forall n m, lattice.laws l (X n m); dotA: forall n m p q (x: X n m) y (z: X p q), x⋅(y⋅z) ≡ (x⋅y)⋅z; dot1x: forall n m (x: X n m), 1⋅x ≡ x; dotx1_: CNV ≪ l \/ forall n m (x: X m n), x⋅1 ≡ x; dot_leq_: DIV ≪ l \/ forall n m p, Proper (leq ==> leq ==> leq) (dot n m p); dotplsx_ {CUP ≪ l}: DIV ≪ l \/ CNV ≪ l \/ forall n m p (x y: X m n) (z: X p m), z⋅(x+y) ≦ z⋅x+z⋅y; dot0x_ {BOT ≪ l}: DIV ≪ l \/ CNV ≪ l \/ forall n m p (x: X p m), x⋅0 ≦ zer p n; cnvdot_ {CNV ≪ l}: forall n m (x: X n m), x°° ≡ x; cnv_leq {CNV ≪ l}: CAP ≪ l \/ forall n m (x: X n m), x ≦ x⋅x°⋅x; str_refl {STR ≪ l}: forall n (x: X n n), x⋅x^* ≦ x^*; str_ind_l {STR ≪ l}: DIV ≪ l \/ CNV ≪ l \/ forall n m (x: X n n) (z: X m n), z⋅x ≦ z -> z⋅x^* ≦ z; itr_str_l {AL ≪ l}: forall n m p (x: X n m) (y: X m p) (z: X n p), (x⋅y) ∩ z ≦ x⋅(y ∩ (x°⋅z)); ldv_spec {DIV ≪ l}: forall n m p (x: X m n) (y: X p n) z, z ≦ y o- x <-> z⋅x ≦ y }. ```

:hammer_and_wrench: Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)

```coq ```

:hammer_and_wrench: :scroll: Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)

```coq ```

:scroll: Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 20KiB file on GitHub Actions Artifacts under build.log)

``` /coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{STR ≪ l} n m (x: X n n) (y z: X n m): y ≦ z -> x⋅z ≦ z -> x^*⋅y ≦ z.' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{STR ≪ l} n (x z: X n n): 1 ≦ z -> x⋅z ≦ z -> x^* ≦ z.' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{STR ≪ l} n: Proper (leq ==> leq) (str n).' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{STR ≪ l} n: Proper (weq ==> weq) (str n) := op_leq_weq_1.' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{STR ≪ l} n (x: X n n): x^*⋅x ≦ x^*.' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{KA ≪ l} n (x: X n n): x^* ≡ 1+x⋅x^*.' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{KA ≪ l} n (x: X n n): x^* ≡ 1+x^+.' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{CNV+STR ≪ l} n (x: X n n): x^*° ≦ x°^*.' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{STR+DIV ≪ l} n m (x: X m n): (x -o x)^* ≦ x -o x.' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{STR ≪ l} n m (x: X n n) (z: X m n): z⋅x ≦ z -> z⋅x^* ≦ z.' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{STR ≪ l} n (x: X n n): x ⋅ x^* ≡ x^* ⋅ x.' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{STR ≪ l} n (x: X n n): x^+ ≡ x^* ⋅ x.' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{DIV ≪ l} n m p: Proper (leq --> leq ++> leq) (rdv n m p).' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{DIV ≪ l} n m p: Proper (weq ==> weq ==> weq) (rdv n m p).' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{DIV ≪ l} n m p: Proper (weq ==> weq ==> weq) (rdv n m p).' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{CNV+DIV ≪ l} n m p (x: X m n) (y: X p n): (y o- x)° ≡ x° -o y°.' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{CAP ≪ l} n m p (x: X m n) (y z: X p m): (y ∩ z) ⋅ x ≦ (y⋅x) ∩ (z⋅x). ' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{BL+CNV ≪ l} n m p (x : X n m) (y : X m p) (z : X n p): ' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{STR ≪ l}: forall n (x: X n n), f (x^*) ≡ (f x)^*;' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{DIV ≪ l}: forall n m p (x: X n m) (y: X n p), f (x -o y) ≡ f x -o f y;' /github/workspace/coqbot.sh: command substitution: line 2: syntax error near unexpected token `(' /github/workspace/coqbot.sh: command substitution: line 2: `{L: laws} n m (x y: X n m): ' +++ [33;1m(/github/workspace/run-script.sh @ line 2) $[0m '{L:laws}' /github/workspace/coqbot.sh: line 2: {L:laws}: command not found +++ [33;1m(/github/workspace/run-script.sh @ line 2) $[0m '{laws}' /github/workspace/coqbot.sh: line 2: {laws}: command not found ++ [33;1m(/github/workspace/run-script.sh @ line 1020) $[0m coqc -q bug.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 MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q bug.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.nL9Fd3r5sU MINIMIZER_DEBUG: files: bug.v File "./bug.v", line 59, characters 0-53: Warning: The '%' scope delimiter in 'Arguments' commands is deprecated, use '%_' instead (available since 8.19). The '%' syntax will be reused in a future version with the same semantics as in terms, that is adding scope to the stack for all subterms. Code can be adapted with a script like: for f in $(find . -name '*.v'); do sed '/Arguments/ s/%/%_/g' -i $f ; done [argument-scope-delimiter,deprecated-since-8.19,deprecated,default] File "./bug.v", line 61, characters 0-47: Warning: The '%' scope delimiter in 'Arguments' commands is deprecated, use '%_' instead (available since 8.19). The '%' syntax will be reused in a future version with the same semantics as in terms, that is adding scope to the stack for all subterms. Code can be adapted with a script like: for f in $(find . -name '*.v'); do sed '/Arguments/ s/%/%_/g' -i $f ; done [argument-scope-delimiter,deprecated-since-8.19,deprecated,default] File "./bug.v", line 62, characters 0-47: Warning: The '%' scope delimiter in 'Arguments' commands is deprecated, use '%_' instead (available since 8.19). The '%' syntax will be reused in a future version with the same semantics as in terms, that is adding scope to the stack for all subterms. Code can be adapted with a script like: for f in $(find . -name '*.v'); do sed '/Arguments/ s/%/%_/g' -i $f ; done [argument-scope-delimiter,deprecated-since-8.19,deprecated,default] File "./bug.v", line 63, characters 0-49: Warning: The '%' scope delimiter in 'Arguments' commands is deprecated, use '%_' instead (available since 8.19). The '%' syntax will be reused in a future version with the same semantics as in terms, that is adding scope to the stack for all subterms. Code can be adapted with a script like: for f in $(find . -name '*.v'); do sed '/Arguments/ s/%/%_/g' -i $f ; done [argument-scope-delimiter,deprecated-since-8.19,deprecated,default] File "./bug.v", line 64, characters 0-53: Warning: The '%' scope delimiter in 'Arguments' commands is deprecated, use '%_' instead (available since 8.19). The '%' syntax will be reused in a future version with the same semantics as in terms, that is adding scope to the stack for all subterms. Code can be adapted with a script like: for f in $(find . -name '*.v'); do sed '/Arguments/ s/%/%_/g' -i $f ; done [argument-scope-delimiter,deprecated-since-8.19,deprecated,default] File "./bug.v", line 65, characters 0-53: Warning: The '%' scope delimiter in 'Arguments' commands is deprecated, use '%_' instead (available since 8.19). The '%' syntax will be reused in a future version with the same semantics as in terms, that is adding scope to the stack for all subterms. Code can be adapted with a script like: for f in $(find . -name '*.v'); do sed '/Arguments/ s/%/%_/g' -i $f ; done [argument-scope-delimiter,deprecated-since-8.19,deprecated,default] File "./bug.v", line 128, characters 17-20: Error: Syntax error: '}' or ':' or [name] expected after [name] (in [closed_binder]). ```

:scroll: :mag_right: Minimization Log (truncated to last 8.0KiB; full 76KiB file on GitHub Actions Artifacts under bug.log)

``` 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/Ltac2 Ltac2 -Q /home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/RelationAlgebra RelationAlgebra -top Top.bug_01 -o /tmp/bug_01.vo -dump-glob bug_01.glob bug_01.v getting bug_01.glob (/github/workspace/cwd/bug_01.glob) getting Coq/Setoids/Setoid.v (/github/workspace/cwd/Coq/Setoids/Setoid.v) Warning: Cannot inline Coq.Setoids.Setoid ([Errno 2] No such file or directory: 'Coq/Setoids/Setoid.v') Recursively Searched: () Nonrecursively Searched: (('/github/workspace/cwd', 'Top'), ('/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums', 'Bignums'), ('/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2', 'Ltac2'), ('/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/RelationAlgebra', 'RelationAlgebra')) getting /github/workspace/cwd/bug_01.glob [92m Sanity check passed.[0m Now, I will attempt to strip repeated newlines and trailing spaces from this file... No strippable newlines or spaces. Now, I will attempt to strip the comments from this file... [92m Succeeded in stripping comments.[0m Now, I will attempt to factor out all of the [Require]s... getting bug_01.v (/github/workspace/cwd/bug_01.v) NOTE: The file bug_01.v is very new (1716491378, 0 seconds old), delaying until it's a bit older /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -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/Ltac2 Ltac2 -Q /home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/RelationAlgebra RelationAlgebra -q -w -deprecated-native-compiler-option,-native-compiler-disabled -native-compiler ondemand -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/Ltac2 Ltac2 -Q /home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/RelationAlgebra RelationAlgebra -top Top.bug_01 -o /tmp/bug_01.vo -dump-glob bug_01.glob bug_01.v getting bug_01.glob (/github/workspace/cwd/bug_01.glob) getting bug_01.glob (/github/workspace/cwd/bug_01.glob) [92m Succeeded in normalizing Requires.[0m Now, I will attempt to split up [Require] statements... getting /github/workspace/cwd/bug_01.v NOTE: The file /github/workspace/cwd/bug_01.v is very new (1716491380, 0 seconds old), delaying until it's a bit older getting /github/workspace/cwd/bug_01.glob getting /github/workspace/cwd/bug_01.glob No Requires to split. In order to efficiently manipulate the file, I have to break it into statements. I will attempt to do this by matching on periods. [92m Splitting successful.[0m I will now attempt to remove any lines after the line which generates the error. [92m Trimming successful. We removed all lines after 89; the error was on line 75.[0m In order to efficiently manipulate the file, I have to break it into definitions. I will now attempt to do this. Sending statements to coqtop... Done. Splitting to definitions... Warning: Could not find timing info in "Toplevel input, characters 430-433:\n> dotplsx_ {CUP ≪ l}: DIV ≪ l \\/ CNV ≪ l \\/ forall n m p (x y: X m n) (z: X p m), z⋅(x+y) ≦ z⋅x+z⋅y;\n> ^\nError:\nSyntax error: '}' or ':' or [name] expected after [name] (in [closed_binder]).\n\nCoq < 17 || 0 < " [92m Splitting to definitions successful.[0m I will now attempt to remove goals ending in [Abort.] [92m Aborted removal successful.[0m I will now attempt to remove unused Ltacs [92m Ltac removal successful.[0m I will now attempt to remove unused definitions [92m Definition removal successful.[0m I will now attempt to remove unused non-instance, non-canonical structure definitions [92m Non-instance definition removal successful.[0m I will now attempt to remove unused variables [92m Variable removal successful.[0m I will now attempt to remove unused contexts [92m Context removal successful.[0m I will now attempt to replace Qed Obligation with Admit Obligations [92m Admitting Qed Obligations successful.[0m Failed to do everything at once; trying one at a time. Admitting Qed Obligations unsuccessful. No successful changes. I will now attempt to replace Qeds with Admitteds [92m Admitting Qeds successful.[0m Failed to do everything at once; trying one at a time. Admitting Qeds unsuccessful. No successful changes. I will now attempt to replace Qeds with admit. Defined. [92m Admitting Qeds successful.[0m Failed to do everything at once; trying one at a time. Admitting Qeds unsuccessful. No successful changes. I will now attempt to remove goals ending in [Abort.] [92m Aborted removal successful.[0m I will now attempt to remove unused Ltacs [92m Ltac removal successful.[0m I will now attempt to remove unused definitions [92m Definition removal successful.[0m I will now attempt to remove unused non-instance, non-canonical structure definitions [92m Non-instance definition removal successful.[0m I will now attempt to remove unused variables [92m Variable removal successful.[0m I will now attempt to remove unused contexts [92m Context removal successful.[0m I will now attempt to admit [abstract ...]s [92m Admitting [abstract ...] successful.[0m [92m Admitting [abstract ...] successful.[0m Admitting [abstract ...] unsuccessful. Admitting [abstract ...] unsuccessful. I will now attempt to remove goals ending in [Abort.] [92m Aborted removal successful.[0m I will now attempt to remove unused Ltacs [92m Ltac removal successful.[0m I will now attempt to remove unused definitions [92m Definition removal successful.[0m I will now attempt to remove unused non-instance, non-canonical structure definitions [92m Non-instance definition removal successful.[0m I will now attempt to remove unused variables [92m Variable removal successful.[0m I will now attempt to remove unused contexts [92m Context removal successful.[0m I will now attempt to replace Obligation with Admit Obligations [92m Admitting Obligations successful.[0m 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 [92m Admitting lemmas successful.[0m 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 [92m Admitting definitions successful.[0m 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 [92m Admitting lemmas successful.[0m 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 [92m Admitting definitions successful.[0m 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.] [92m Aborted removal successful.[0m I will now attempt to remove unused Ltacs [92m Ltac removal successful.[0m I will now attempt to remove unused definitions [92m Definition removal successful.[0m I will now attempt to remove unused non-instance, non-canonical structure definitions [92m Non-instance definition removal successful.[0m I will now attempt to remove unused variables [92m Variable removal successful.[0m I will now attempt to remove unused contexts [92m Context removal successful.[0m 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... [92m Succeeded in stripping newlines and spaces.[0m ```

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.

JasonGross commented 6 months ago

That is not the minimal example I was looking for...

JasonGross commented 6 months ago

@coqbot minimize coq.dev

opam install -y coq-relation-algebra
wget https://github.com/coq-community/run-coq-bug-minimizer/actions/runs/9205215847/artifacts/1530397207 -O tmp.v.zip
unzip tmp.v.zip
mv tmp.v bug.v
coqc -q bug.v

coqbot-app[bot] commented 6 months ago

Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.

coqbot-app[bot] commented 6 months ago

@JasonGross, Error: Could not minimize file (full log on GitHub Actions, cc @JasonGross)

build log

``` + [33;1m(/github/workspace/run-script.sh @ line 47) $[0m ocamlc -config version: 4.13.1 standard_library_default: /home/coq/.opam/4.13.1+flambda/lib/ocaml standard_library: /home/coq/.opam/4.13.1+flambda/lib/ocaml ccomp_type: cc c_compiler: gcc ocamlc_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlc_cppflags: -D_FILE_OFFSET_BITS=64 ocamlopt_cflags: -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC ocamlopt_cppflags: -D_FILE_OFFSET_BITS=64 bytecomp_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 native_c_compiler: gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 bytecomp_c_libraries: -lm -ldl -lpthread native_c_libraries: -lm -ldl native_pack_linker: ld -r -o ranlib: ranlib architecture: amd64 model: default int_size: 63 word_size: 64 system: linux asm: as asm_cfi_supported: true with_frame_pointers: false ext_exe: ext_obj: .o ext_asm: .s ext_lib: .a ext_dll: .so os_type: Unix default_executable_name: a.out systhread_supported: true host: x86_64-pc-linux-gnu target: x86_64-pc-linux-gnu flambda: true safe_string: true default_safe_string: true flat_float_array: true function_sections: true afl_instrument: false windows_unicode: false supports_shared_libraries: true exec_magic_number: Caml1999X030 cmi_magic_number: Caml1999I030 cmo_magic_number: Caml1999O030 cma_magic_number: Caml1999A030 cmx_magic_number: Caml1999y030 cmxa_magic_number: Caml1999z030 ast_impl_magic_number: Caml1999M030 ast_intf_magic_number: Caml1999N030 cmxs_magic_number: Caml1999D030 cmt_magic_number: Caml1999T030 linear_magic_number: Caml1999L030 + [33;1m(/github/workspace/run-script.sh @ line 48) $[0m coqc --config MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --config MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.m9DXY8FrAB MINIMIZER_DEBUG: files: COQLIB=/home/coq/.opam/4.13.1+flambda/lib/coq/ COQCORELIB=/home/coq/.opam/4.13.1+flambda/lib/coq/../coq-core/ DOCDIR=/home/coq/.opam/4.13.1+flambda/share/doc/ OCAMLFIND=/home/coq/.opam/4.13.1+flambda/bin/ocamlfind CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 WARN=-warn-error +a-3 HASNATDYNLINK=true COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/ltac2_ltac1 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax COQ_NATIVE_COMPILER_DEFAULT=no + [33;1m(/github/workspace/run-script.sh @ line 49) $[0m coqc --version MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --version MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.tKEHTMWswO MINIMIZER_DEBUG: files: The Coq Proof Assistant, version 8.20+alpha compiled with OCaml 4.13.1 + [33;1m(/github/workspace/run-script.sh @ line 50) $[0m true + [33;1m(/github/workspace/run-script.sh @ line 50) $[0m coqtop MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqtop MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqtop.orig MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.aH5p1a1kZf MINIMIZER_DEBUG: files: Welcome to Coq buildkitsandbox:/home/coq/.opam/4.13.1+flambda/.opam-switch/build/coq-core.dev/_build/default,master (e05a8eea9fafd242a1e41272d8f9dbbcdabca1e5) Coq < + [33;1m(/github/workspace/run-script.sh @ line 52) $[0m source /github/workspace/coqbot.sh ++ [33;1m(/github/workspace/run-script.sh @ line 1) $[0m opam install -y coq-relation-algebra The following actions will be performed: - install coq-relation-algebra dev <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> -> retrieved coq-relation-algebra.dev (git+https://github.com/damien-pous/relation-algebra.git#master) -> installed coq-relation-algebra.dev Done. ::group::opam wrap files wrapping /usr/local/bin/opam attempting to wrap coqc wrapping /home/coq/.opam/4.13.1+flambda/bin/coqc attempting to wrap coqtop wrapping /home/coq/.opam/4.13.1+flambda/bin/coqtop ::endgroup:: ++ [33;1m(/github/workspace/run-script.sh @ line 2) $[0m wget https://github.com/coq-community/run-coq-bug-minimizer/actions/runs/9205215847/artifacts/1530397207 -O tmp.v.zip --2024-05-23 19:27:38-- https://github.com/coq-community/run-coq-bug-minimizer/actions/runs/9205215847/artifacts/1530397207 Resolving github.com (github.com)... 140.82.112.3 Connecting to github.com (github.com)|140.82.112.3|:443... connected. HTTP request sent, awaiting response... 307 Temporary Redirect Location: https://github.com/coq-community/run-coq-bug-minimizer/suites/24093794502/artifacts/1530397207 [following] --2024-05-23 19:27:38-- https://github.com/coq-community/run-coq-bug-minimizer/suites/24093794502/artifacts/1530397207 Reusing existing connection to github.com:443. HTTP request sent, awaiting response... 404 Not Found 2024-05-23 19:27:38 ERROR 404: Not Found. ++ [33;1m(/github/workspace/run-script.sh @ line 3) $[0m unzip tmp.v.zip Archive: tmp.v.zip End-of-central-directory signature not found. Either this file is not a zipfile, or it constitutes one disk of a multi-part archive. In the latter case the central directory and zipfile comment will be found on the last disk(s) of this archive. unzip: cannot find zipfile directory in one of tmp.v.zip or tmp.v.zip.zip, and cannot find tmp.v.zip.ZIP, period. ++ [33;1m(/github/workspace/run-script.sh @ line 4) $[0m mv tmp.v bug.v mv: cannot stat 'tmp.v': No such file or directory ++ [33;1m(/github/workspace/run-script.sh @ line 5) $[0m coqc -q bug.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 MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q bug.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.URMIBdlrUS MINIMIZER_DEBUG: files: bug.v Error: Can't find file ./bug.v ```

minimizer log

``` ```

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.

SkySkimmer commented 5 months ago

reopen if you manage to minimize

coq / coq

anomaly uncaught exception not_found #19077