search

JasonGross / coq-tools

Some scripts to help construct small reproducing examples of bugs, implement [Proof using], etc.
MIT License
39 stars 9 forks source link

bug minimizer fails to pass correct `-top` to passing coqc #219

Closed JasonGross closed 1 month ago

JasonGross commented 1 month ago

Error: Could not minimize file /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/metacoq/test-suite/univ.v (from ci-metacoq) (full log on GitHub Actions, cc @JasonGross)

build log (truncated to last 26KiB; full 4.5MiB file on GitHub Actions Artifacts under build.log) ``` g a view) -> rebuilding environment lookup table -> optimize_prop_discr -> rebuilding environment lookup table -> primitive projection inlining -> rebuilding environment lookup table executed in: 0.00148916244507s transforming to constuctors as blocks executed in: 0.000221967697144s switching to unguarded fixpoints -> stripping constructor parameters (using a view) -> rebuilding environment lookup table -> optimize_prop_discr -> rebuilding environment lookup table -> primitive projection inlining -> rebuilding environment lookup table -> transforming to constuctors as blocks executed in: 0.00172996520996s reorder inductive constructors -> rebuilding environment lookup table -> switching to unguarded fixpoints -> stripping constructor parameters (using a view) -> rebuilding environment lookup table -> optimize_prop_discr -> rebuilding environment lookup table -> primitive projection inlining -> rebuilding environment lookup table -> transforming to constuctors as blocks executed in: 0.00198602676392s let expansion in constructors -> erasure -> reorder inductive constructors -> rebuilding environment lookup table -> switching to unguarded fixpoints -> stripping constructor parameters (using a view) -> rebuilding environment lookup table -> optimize_prop_discr -> rebuilding environment lookup table -> primitive projection inlining -> rebuilding environment lookup table -> transforming to constuctors as blocks executed in: 0.0118219852448s rebuilding environment lookup table -> eta expand cstrs and fixpoints -> template to pcuic -> let expansion in constructors -> erasure -> reorder inductive constructors -> rebuilding environment lookup table -> switching to unguarded fixpoints -> stripping constructor parameters (using a view) -> rebuilding environment lookup table -> optimize_prop_discr -> rebuilding environment lookup table -> primitive projection inlining -> rebuilding environment lookup table -> transforming to constuctors as blocks executed in: 0.0202620029449s skipped rebuilding environment lookup table -> transforming co-inductive to lazy inductive types executed in: 9.53674316406e-07s skipped rebuilding environment lookup table -> unbox singleton constructors executed in: 0.s skipped rebuilding environment lookup table -> transforming co-inductive to lazy inductive types -> skipped rebuilding environment lookup table -> unbox singleton constructors executed in: 1.00135803223e-05s skipped inlining -> forgetting about inlining info executed in: 0.s skipped rebuilding environment lookup table -> transforming co-inductive to lazy inductive types -> skipped rebuilding environment lookup table -> unbox singleton constructors -> skipped inlining -> forgetting about inlining info executed in: 2.21729278564e-05s skipped betared -> betared executed in: 0.s skipped rebuilding environment lookup table -> transforming co-inductive to lazy inductive types -> skipped rebuilding environment lookup table -> unbox singleton constructors -> skipped inlining -> forgetting about inlining info -> skipped betared -> betared executed in: 3.38554382324e-05s rebuilding environment lookup table -> eta expand cstrs and fixpoints -> template to pcuic -> let expansion in constructors -> erasure -> reorder inductive constructors -> rebuilding environment lookup table -> switching to unguarded fixpoints -> stripping constructor parameters (using a view) -> rebuilding environment lookup table -> optimize_prop_discr -> rebuilding environment lookup table -> primitive projection inlining -> rebuilding environment lookup table -> transforming to constuctors as blocks -> skipped rebuilding environment lookup table -> transforming co-inductive to lazy inductive types -> skipped rebuilding environment lookup table -> unbox singleton constructors -> skipped inlining -> forgetting about inlining info -> skipped betared -> betared executed in: 0.0203130245209s Pretty printing executed in: 0.00238800048828s Environment: Inductive list(0 parameters,computational, elimination into any sort) := | nil 0 arguments | cons 2 arguments Inductive positive(0 parameters,computational, elimination into any sort) := | xI 1 arguments | xO 1 arguments | xH 0 arguments Inductive expr(0 parameters,computational, elimination into any sort) := | Nil 0 arguments | Var 1 arguments Inductive pn_atom(0 parameters,computational, elimination into any sort) := | Equ 2 arguments | Nequ 2 arguments Inductive space_atom(0 parameters,computational, elimination into any sort) := | Next 2 arguments | Lseg 2 arguments Inductive assertion(0 parameters,computational, elimination into any sort) := | Assertion 2 arguments Inductive entailment(0 parameters,computational, elimination into any sort) := | Entailment 2 arguments Inductive pure_atom(0 parameters,computational, elimination into any sort) := | Eqv 2 arguments Definition Stdlib.PArith.BinPosDef.Pos.succ := fun x => (let fix succ { struct 0 } := fun x0 => match x0 with xI p => xO[(succ p)] | xO p => xI[p] | xH => xO[xH] end in succ) x Definition Stdlib.PArith.BinPosDef.Pos.add := fun x => (let fix add { struct 0 } := fun x0 => fun y => match x0 with xI p => match y with xI q => xO[(add p q)] | xO q => xI[(add_carry p q)] | xH => xO[(Stdlib.PArith.BinPosDef.Pos.succ p)] end | xO p => match y with xI q => xI[(add_carry p q)] | xO q => xO[(add_carry p q)] | xH => xI[p] end | xH => match y with xI q => xO[(Stdlib.PArith.BinPosDef.Pos.succ q)] | xO q => xI[q] | xH => xO[xH] end end with add_carry { struct 0 } := fun x0 => fun y => match x0 with xI p => match y with xI q => xI[(add p q)] | xO q => xO[(add p q)] | xH => xI[(Stdlib.PArith.BinPosDef.Pos.succ p)] end | xO p => match y with xI q => xO[(add p q)] | xO q => xI[(add_carry p q)] | xH => xO[(Stdlib.PArith.BinPosDef.Pos.succ p)] end | xH => match y with xI q => xI[(Stdlib.PArith.BinPosDef.Pos.succ q)] | xO q => xO[(Stdlib.PArith.BinPosDef.Pos.succ q)] | xH => xI[xH] end end in add) x Definition MetaCoq.TestSuite.vs.add_id := Stdlib.PArith.BinPosDef.Pos.add Definition MetaCoq.TestSuite.vs.list_prio := fun A => fun weight => fun l => (let fix list_prio { struct 2 } := fun A0 => fun weight0 => fun l0 => fun p => match l0 with nil => p | cons a l' => list_prio ∎ weight0 l' (MetaCoq.TestSuite.vs.add_id weight0 p) end in list_prio) ∎ weight l Inductive Z(0 parameters,computational, elimination into any sort) := | Z0 0 arguments | Zpos 1 arguments | Zneg 1 arguments Definition MetaCoq.TestSuite.vs.Z2id := fun z => match z with Z0 => xH | Zpos p => Stdlib.PArith.BinPosDef.Pos.add p xH | Zneg p => xH end Definition MetaCoq.TestSuite.vs.var2 := MetaCoq.TestSuite.vs.Z2id (Zpos[(xO[xH])]) Definition MetaCoq.TestSuite.vs.var1 := MetaCoq.TestSuite.vs.Z2id (Zpos[xH]) Definition MetaCoq.TestSuite.vs.var0 := MetaCoq.TestSuite.vs.Z2id Z0 Definition MetaCoq.TestSuite.vs.prio := fun gamma => fun delta => MetaCoq.TestSuite.vs.list_prio ∎ MetaCoq.TestSuite.vs.var2 gamma (MetaCoq.TestSuite.vs.list_prio ∎ MetaCoq.TestSuite.vs.var1 delta MetaCoq.TestSuite.vs.var0) Inductive clause(0 parameters,computational, elimination into any sort) := | PureClause 4 arguments | PosSpaceClause 3 arguments | NegSpaceClause 3 arguments Definition Stdlib.Lists.List.fold_left := fun A => fun B => fun f => fun l => (let fix fold_left { struct 0 } := fun l0 => fun a0 => match l0 with nil => a0 | cons b t => fold_left t (f a0 b) end in fold_left) l Inductive color(0 parameters,computational, elimination into any sort) := | Red 0 arguments | Black 0 arguments Inductive tree(0 parameters,computational, elimination into any sort) := | Leaf 0 arguments | Node 4 arguments Inductive comparison(0 parameters,computational, elimination into any sort) := | Eq 0 arguments | Lt 0 arguments | Gt 0 arguments Definition Stdlib.PArith.BinPosDef.Pos.compare_cont := fun r => fun x => fun y => (let fix compare_cont { struct 2 } := fun r0 => fun x0 => fun y0 => match x0 with xI p => match y0 with xI q => compare_cont r0 p q | xO q => compare_cont Gt p q | xH => Gt end | xO p => match y0 with xI q => compare_cont Lt p q | xO q => compare_cont r0 p q | xH => Gt end | xH => match y0 with xI q => Lt | xO q => Lt | xH => r0 end end in compare_cont) r x y Definition Stdlib.PArith.BinPosDef.Pos.compare := Stdlib.PArith.BinPosDef.Pos.compare_cont Eq Definition MetaCoq.TestSuite.vs.prio1000 := MetaCoq.TestSuite.vs.Z2id (Zpos[(xO[(xO[(xO[(xI[(xO[(xI[(xI[(xI[(xI[xH])])])])])])])])])]) Definition MetaCoq.TestSuite.vs.prio1001 := MetaCoq.TestSuite.vs.Z2id (Zpos[(xI[(xO[(xO[(xI[(xO[(xI[(xI[(xI[(xI[xH])])])])])])])])])]) Definition MetaCoq.TestSuite.vs.clause_prio := fun cl => match cl with PureClause gamma delta prio prio_ok => prio | PosSpaceClause gamma delta sigma => MetaCoq.TestSuite.vs.prio1000 | NegSpaceClause gamma sigma delta => MetaCoq.TestSuite.vs.prio1001 end Definition MetaCoq.TestSuite.vs.compare_list := fun A => fun f => fun xl => (let fix compare_list { struct 2 } := fun A0 => fun f0 => fun xl0 => fun yl => match xl0 with nil => match yl with nil => Eq | cons a l => Lt end | cons x xl' => match yl with nil => Gt | cons y yl' => match f0 x y with Eq => compare_list ∎ f0 xl' yl' | Lt => Lt | Gt => Gt end end end in compare_list) ∎ f xl Definition MetaCoq.TestSuite.vs.expr_cmp := fun e => fun e' => match e with Nil => match e' with Nil => Eq | Var v => Lt end | Var v => match e' with Nil => Gt | Var v' => Stdlib.PArith.BinPosDef.Pos.compare v v' end end Definition MetaCoq.TestSuite.vs.pure_atom_cmp := fun a => fun a' => match a with Eqv e1 e2 => match a' with Eqv e1' e2' => match MetaCoq.TestSuite.vs.expr_cmp e1 e1' with Eq => MetaCoq.TestSuite.vs.expr_cmp e2 e2' | Lt => Lt | Gt => Gt end end end Definition MetaCoq.TestSuite.vs.compare_space_atom := fun a => fun b => match a with Next i j => match b with Next i' j' => match MetaCoq.TestSuite.vs.expr_cmp i i' with Eq => MetaCoq.TestSuite.vs.expr_cmp j j' | Lt => Lt | Gt => Gt end | Lseg i' j' => match MetaCoq.TestSuite.vs.expr_cmp i i' with Eq => Lt | Lt => Lt | Gt => Gt end end | Lseg i j => match b with Next i' j' => match MetaCoq.TestSuite.vs.expr_cmp i i' with Eq => Gt | Lt => Lt | Gt => Gt end | Lseg i' j' => match MetaCoq.TestSuite.vs.expr_cmp i i' with Eq => MetaCoq.TestSuite.vs.expr_cmp j j' | Lt => Lt | Gt => Gt end end end Definition MetaCoq.TestSuite.vs.compare_clause := fun cl1 => fun cl2 => match cl1 with PureClause neg pos priority prio_ok => match cl2 with PureClause neg' pos' priority0 prio_ok0 => match MetaCoq.TestSuite.vs.compare_list ∎ MetaCoq.TestSuite.vs.pure_atom_cmp neg neg' with Eq => MetaCoq.TestSuite.vs.compare_list ∎ MetaCoq.TestSuite.vs.pure_atom_cmp pos pos' | Lt => Lt | Gt => Gt end | PosSpaceClause gamma delta sigma => Lt | NegSpaceClause gamma sigma delta => Lt end | PosSpaceClause gamma delta sigma => match cl2 with PureClause gamma0 delta0 priority prio_ok => Gt | PosSpaceClause gamma' delta' sigma' => match MetaCoq.TestSuite.vs.compare_list ∎ MetaCoq.TestSuite.vs.pure_atom_cmp gamma gamma' with Eq => match MetaCoq.TestSuite.vs.compare_list ∎ MetaCoq.TestSuite.vs.pure_atom_cmp delta delta' with Eq => MetaCoq.TestSuite.vs.compare_list ∎ MetaCoq.TestSuite.vs.compare_space_atom sigma sigma' | Lt => Lt | Gt => Gt end | Lt => Lt | Gt => Gt end | NegSpaceClause gamma0 sigma0 delta0 => Lt end | NegSpaceClause gamma sigma delta => match cl2 with PureClause gamma0 delta0 priority prio_ok => Gt | PosSpaceClause gamma0 delta0 sigma0 => Gt | NegSpaceClause gamma' sigma' delta' => match MetaCoq.TestSuite.vs.compare_list ∎ MetaCoq.TestSuite.vs.pure_atom_cmp gamma gamma' with Eq => match MetaCoq.TestSuite.vs.compare_list ∎ MetaCoq.TestSuite.vs.pure_atom_cmp delta delta' with Eq => MetaCoq.TestSuite.vs.compare_list ∎ MetaCoq.TestSuite.vs.compare_space_atom sigma sigma' | Lt => Lt | Gt => Gt end | Lt => Lt | Gt => Gt end end end Definition MetaCoq.TestSuite.vs.compare_clause' := fun cl1 => fun cl2 => match Stdlib.PArith.BinPosDef.Pos.compare (MetaCoq.TestSuite.vs.clause_prio cl1) (MetaCoq.TestSuite.vs.clause_prio cl2) with Eq => MetaCoq.TestSuite.vs.compare_clause cl1 cl2 | Lt => Lt | Gt => Gt end Variant t_(0 parameters,computational, elimination into any sort) := | Mkt 2 arguments Definition MetaCoq.TestSuite.vs.M.Raw.makeBlack := fun t => match t with Leaf => Leaf | Node t0 a x b => Node[Black a x b] end Definition MetaCoq.TestSuite.vs.M.Raw.lbal := fun l => fun k => fun r => match l with Leaf => Node[Black l k r] | Node t a x c => match t with Red => match a with Leaf => match c with Leaf => Node[Black l k r] | Node t0 b y c => match t0 with Red => Node[Red (Node[Black a x b]) y (Node[Black c k r])] | Black => Node[Black l k r] end end | Node t0 a x b => match t0 with Red => Node[Red (Node[Black a x b]) x (Node[Black c k r])] | Black => match c with Leaf => Node[Black l k r] | Node t1 b y c => match t1 with Red => Node[Red (Node[Black a x b]) y (Node[Black c k r])] | Black => Node[Black l k r] end end end end | Black => Node[Black l k r] end end Definition MetaCoq.TestSuite.vs.M.Raw.rbal := fun l => fun k => fun r => match r with Leaf => Node[Black l k r] | Node t b y d => match t with Red => match b with Leaf => match d with Leaf => Node[Black l k r] | Node t0 c z d => match t0 with Red => Node[Red (Node[Black l k b]) y (Node[Black c z d])] | Black => Node[Black l k r] end end | Node t0 b y c => match t0 with Red => Node[Red (Node[Black l k b]) y (Node[Black c y d])] | Black => match d with Leaf => Node[Black l k r] | Node t1 c z d => match t1 with Red => Node[Red (Node[Black l k b]) y (Node[Black c z d])] | Black => Node[Black l k r] end end end end | Black => Node[Black l k r] end end Definition MetaCoq.TestSuite.vs.M.Raw.ins := fun x => fun s => (let fix ins { struct 1 } := fun x0 => fun s0 => match s0 with Leaf => Node[Red Leaf x0 Leaf] | Node c l y r => match MetaCoq.TestSuite.vs.compare_clause' x0 y with Eq => s0 | Lt => match c with Red => Node[Red (ins x0 l) y r] | Black => MetaCoq.TestSuite.vs.M.Raw.lbal (ins x0 l) y r end | Gt => match c with Red => Node[Red l y (ins x0 r)] | Black => MetaCoq.TestSuite.vs.M.Raw.rbal l y (ins x0 r) end end end in ins) x s Definition MetaCoq.TestSuite.vs.M.Raw.add := fun x => fun s => MetaCoq.TestSuite.vs.M.Raw.makeBlack (MetaCoq.TestSuite.vs.M.Raw.ins x s) Definition MetaCoq.TestSuite.vs.M.this := fun t => match t with Mkt this is_ok => this end Definition MetaCoq.TestSuite.vs.M.add := fun x => fun s => Mkt[(MetaCoq.TestSuite.vs.M.Raw.add x (MetaCoq.TestSuite.vs.M.this s)) ∎] Definition MetaCoq.TestSuite.vs.M.Raw.empty := Leaf Definition MetaCoq.TestSuite.vs.M.empty := Mkt[MetaCoq.TestSuite.vs.M.Raw.empty ∎] Definition MetaCoq.TestSuite.vs.clause_list2set := fun l => Stdlib.Lists.List.fold_left ∎ ∎ (fun s0 => fun c => MetaCoq.TestSuite.vs.M.add c s0) l MetaCoq.TestSuite.vs.M.empty Inductive bool(0 parameters,computational, elimination into any sort) := | true 0 arguments | false 0 arguments Definition Stdlib.Lists.List.filter := fun A => fun f => fun l => (let fix filter { struct 0 } := fun l0 => match l0 with nil => nil | cons x l => match f x with true => cons[x (filter l)] | false => filter l end end in filter) l Definition MetaCoq.TestSuite.vs.VeriStar.pureb := fun c => match c with PureClause gamma delta priority prio_ok => true | PosSpaceClause gamma delta sigma => false | NegSpaceClause gamma sigma delta => false end Definition MetaCoq.TestSuite.vs.VeriStar.pure_clauses := Stdlib.Lists.List.filter ∎ MetaCoq.TestSuite.vs.VeriStar.pureb Definition Stdlib.Lists.List.map := fun A => fun B => fun f => fun l => (let fix map { struct 0 } := fun l0 => match l0 with nil => nil | cons a t => cons[(f a) (map t)] end in map) l Definition MetaCoq.TestSuite.vs.mkPureClause := fun gamma => fun delta => PureClause[gamma delta (MetaCoq.TestSuite.vs.prio gamma delta) ∎] Definition MetaCoq.TestSuite.vs.insert_uniq := fun A => fun cmp => fun a => fun l => (let fix insert_uniq { struct 3 } := fun A0 => fun cmp0 => fun a0 => fun l0 => match l0 with nil => cons[a0 nil] | cons h t => match cmp0 a0 h with Eq => l0 | Lt => cons[h (insert_uniq ∎ cmp0 a0 t)] | Gt => cons[a0 l0] end end in insert_uniq) ∎ cmp a l Definition MetaCoq.TestSuite.vs.rsort_uniq := fun A => fun cmp => fun l => (let fix rsort_uniq { struct 2 } := fun A0 => fun cmp0 => fun l0 => match l0 with nil => nil | cons h t => MetaCoq.TestSuite.vs.insert_uniq ∎ cmp0 h (rsort_uniq ∎ cmp0 t) end in rsort_uniq) ∎ cmp l Definition MetaCoq.TestSuite.vs.order_eqv_pure_atom := fun a => match a with Eqv i j => match MetaCoq.TestSuite.vs.expr_cmp i j with Eq => Eqv[i j] | Lt => Eqv[j i] | Gt => Eqv[i j] end end Definition MetaCoq.TestSuite.vs.normalize_atoms := fun pa => MetaCoq.TestSuite.vs.rsort_uniq ∎ MetaCoq.TestSuite.vs.pure_atom_cmp (Stdlib.Lists.List.map ∎ ∎ MetaCoq.TestSuite.vs.order_eqv_pure_atom pa) Definition MetaCoq.TestSuite.vs.nonreflex_atom := fun a => match a with Eqv i j => match MetaCoq.TestSuite.vs.expr_cmp i j with Eq => false | Lt => true | Gt => true end end Definition MetaCoq.TestSuite.vs.order_eqv_clause := fun c => match c with PureClause pa pa' priority prio_ok => MetaCoq.TestSuite.vs.mkPureClause (MetaCoq.TestSuite.vs.normalize_atoms (Stdlib.Lists.List.filter ∎ MetaCoq.TestSuite.vs.nonreflex_atom pa)) (MetaCoq.TestSuite.vs.normalize_atoms pa') | PosSpaceClause pa pa' sa' => PosSpaceClause[(MetaCoq.TestSuite.vs.normalize_atoms (Stdlib.Lists.List.filter ∎ MetaCoq.TestSuite.vs.nonreflex_atom pa)) (MetaCoq.TestSuite.vs.normalize_atoms pa') sa'] | NegSpaceClause pa sa pa' => NegSpaceClause[(MetaCoq.TestSuite.vs.normalize_atoms (Stdlib.Lists.List.filter ∎ MetaCoq.TestSuite.vs.nonreflex_atom pa)) sa (MetaCoq.TestSuite.vs.normalize_atoms pa')] end Inductive prod(0 parameters,computational, elimination into any sort) := | pair 2 arguments Definition MetaCoq.TestSuite.vs.mk_pureR := fun al => (let fix mk_pureR { struct 0 } := fun al0 => match al0 with nil => pair[nil nil] | cons p l' => match p with Equ x y => match mk_pureR l' with pair p n => pair[(cons[(MetaCoq.TestSuite.vs.order_eqv_pure_atom (Eqv[x y])) p]) n] end | Nequ x y => match mk_pureR l' with pair p n => pair[p (cons[(MetaCoq.TestSuite.vs.order_eqv_pure_atom (Eqv[x y])) n])] end end end in mk_pureR) al Definition Stdlib.Init.Datatypes.app := fun A => fun l => (let fix app { struct 0 } := fun l0 => fun m => match l0 with nil => m | cons a l1 => cons[a (app l1 m)] end in app) l Definition MetaCoq.TestSuite.vs.mk_pureL := fun a => match a with Equ x y => MetaCoq.TestSuite.vs.mkPureClause nil (cons[(MetaCoq.TestSuite.vs.order_eqv_pure_atom (Eqv[x y])) nil]) | Nequ x y => MetaCoq.TestSuite.vs.mkPureClause (cons[(MetaCoq.TestSuite.vs.order_eqv_pure_atom (Eqv[x y])) nil]) nil end Definition MetaCoq.TestSuite.vs.cnf := fun en => match en with Entailment a a0 => match a with Assertion pureL spaceL => match a0 with Assertion pureR spaceR => match MetaCoq.TestSuite.vs.mk_pureR pureR with pair p n => Stdlib.Init.Datatypes.app ∎ (Stdlib.Lists.List.map ∎ ∎ MetaCoq.TestSuite.vs.mk_pureL pureL) (Stdlib.Init.Datatypes.app ∎ (cons[(PosSpaceClause[nil nil spaceL]) nil]) (match spaceL with nil => match spaceR with nil => cons[(MetaCoq.TestSuite.vs.mkPureClause p n) nil] | cons s l => cons[(NegSpaceClause[p spaceR n]) nil] end | cons s l => cons[(NegSpaceClause[p spaceR n]) nil] end )) end end end end Inductive sig(0 parameters,computational, elimination into any sort) := | exist 2 arguments Axiom MetaCoq.TestSuite.vs.VeriStar.the_loop_terminate Definition MetaCoq.TestSuite.vs.VeriStar.the_loop := fun n => fun sigma => fun nc => fun s => fun cl => match MetaCoq.TestSuite.vs.VeriStar.the_loop_terminate n sigma nc s cl with exist a b => a end Definition MetaCoq.TestSuite.vs.DebuggingHooks.print_new_pures_set := fun s => s Definition MetaCoq.TestSuite.vs.empty_clause := MetaCoq.TestSuite.vs.mkPureClause nil nil Definition MetaCoq.TestSuite.vs.VeriStar.check_entailment := fun ent => let s := MetaCoq.TestSuite.vs.clause_list2set (MetaCoq.TestSuite.vs.VeriStar.pure_clauses (Stdlib.Lists.List.map ∎ ∎ MetaCoq.TestSuite.vs.order_eqv_clause (MetaCoq.TestSuite.vs.cnf ent))) in match ent with Entailment a a0 => match a with Assertion pi sigma => match a0 with Assertion pi' sigma' => match MetaCoq.TestSuite.vs.mk_pureR pi with pair piplus piminus => match MetaCoq.TestSuite.vs.mk_pureR pi' with pair pi'plus pi'minus => MetaCoq.TestSuite.vs.VeriStar.the_loop (xO[(xO[(xO[(xO[(xO[(xO[(xO[(xO[(xO[(xI[(xO[(xI[(xO[(xO[(xI[(xI[(xO[(xI[(xO[(xI[(xI[(xO[(xO[(xI[(xI[(xI[(xO[(xI[(xI[xH])])])])])])])])])])])])])])])])])])])])])])])])])])])])]) sigma (NegSpaceClause[pi'plus sigma' pi'minus]) (MetaCoq.TestSuite.vs.DebuggingHooks.print_new_pures_set s) MetaCoq.TestSuite.vs.empty_clause end end end end end Definition MetaCoq.TestSuite.vs.c := Var[(xI[xH])] Definition MetaCoq.TestSuite.vs.e := Var[(xI[(xO[xH])])] Definition MetaCoq.TestSuite.vs.a := Var[xH] Definition MetaCoq.TestSuite.vs.b := Var[(xO[xH])] Definition MetaCoq.TestSuite.vs.d := Var[(xO[(xO[xH])])] Definition MetaCoq.TestSuite.vs.example_ent := Entailment[(Assertion[(cons[(Nequ[MetaCoq.TestSuite.vs.c MetaCoq.TestSuite.vs.e]) nil]) (cons[(Lseg[MetaCoq.TestSuite.vs.a MetaCoq.TestSuite.vs.b]) (cons[(Lseg[MetaCoq.TestSuite.vs.a MetaCoq.TestSuite.vs.c]) (cons[(Next[MetaCoq.TestSuite.vs.c MetaCoq.TestSuite.vs.d]) (cons[(Lseg[MetaCoq.TestSuite.vs.d MetaCoq.TestSuite.vs.e]) nil])])])])]) (Assertion[nil (cons[(Lseg[MetaCoq.TestSuite.vs.b MetaCoq.TestSuite.vs.c]) (cons[(Lseg[MetaCoq.TestSuite.vs.c MetaCoq.TestSuite.vs.e]) nil])])])] Definition MetaCoq.TestSuite.vs.main := MetaCoq.TestSuite.vs.VeriStar.check_entailment MetaCoq.TestSuite.vs.example_ent Program: MetaCoq.TestSuite.vs.main erasure_test.vo (real: 1.20, user: 1.00, sys: 0.19, mem: 699516 ko) COQC univ.v MINIMIZER_DEBUG_EXTRA: coqc: /github/workspace/builds/coq/coq-failing/_install_ci/bin/////coqc MINIMIZER_DEBUG_EXTRA: coqpath: MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite MINIMIZER_DEBUG_EXTRA: exec: /github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig -time-file /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite/univ.v.timing -q -w -deprecated-native-compiler-option -native-compiler no -I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq -I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq -I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq -I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq -I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure-plugin/src -I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/src -R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/utils/theories MetaCoq.Utils -R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/common/theories MetaCoq.Common -R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/pcuic/theories MetaCoq.PCUIC -R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/pcuic/theories MetaCoq.PCUIC -R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories MetaCoq.Template -R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/theories MetaCoq.SafeCheckerPlugin -R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-pcuic/theories MetaCoq.TemplatePCUIC -R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories MetaCoq.Template -R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker/theories MetaCoq.SafeChecker -R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories MetaCoq.Template -R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories MetaCoq.Template -R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-pcuic/theories MetaCoq.TemplatePCUIC -R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure/theories MetaCoq.Erasure -R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/theories MetaCoq.SafeCheckerPlugin -R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure-plugin/theories MetaCoq.ErasurePlugin -R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite MetaCoq.TestSuite univ.v MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.UveEOV3GKy MINIMIZER_DEBUG: files: univ.v File "./univ.v", line 59, characters 0-96: Error: Universe inconsistency. Cannot enforce j < i because i < j. Command exited with non-zero status 1 univ.vo (real: 1.04, user: 0.87, sys: 0.17, mem: 682628 ko) make[4]: *** [Makefile.coq:804: univ.vo] Error 1 make[3]: *** [Makefile.coq:417: all] Error 2 make[3]: Leaving directory '/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite' make[2]: *** [Makefile:6: bugs] Error 2 make[2]: Leaving directory '/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite' make[1]: *** [Makefile:182: test-suite] Error 2 make[1]: Leaving directory '/github/workspace/builds/coq/coq-failing/_build_ci/metacoq' + code=2 + echo 'Aggregating timing log...' Aggregating timing log... + echo + tools/make-one-time-file.py --real metacoq.log Time | Peak Mem | File Name -------------------------------------------- 0m02.24s | 699516 ko | Total Time / Peak Mem -------------------------------------------- 0m01.20s | 699516 ko | erasure_test.vo 0m01.04s | 682628 ko | univ.vo + '[' '' ']' + exit 2 make: *** [Makefile.ci:190: ci-metacoq] Error 2 /github/workspace/builds/coq /github/workspace ::endgroup:: ```
minimizer log ``` Coq version: 8.21+alpha compiled with OCaml 4.09.0 First, I will attempt to absolutize relevant [Require]s in /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite/univ.v, and store the result in /github/workspace/cwd/bug_01.v... getting /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite/univ.v getting /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite/univ.glob Now, I will attempt to coq the file, and find the error... Coqing the file (/github/workspace/cwd/bug_01.v)... Running command: "/github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig" "-q" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/utils/theories" "MetaCoq.Utils" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/common/theories" "MetaCoq.Common" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/pcuic/theories" "MetaCoq.PCUIC" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories" "MetaCoq.Template" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/theories" "MetaCoq.SafeCheckerPlugin" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-pcuic/theories" "MetaCoq.TemplatePCUIC" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker/theories" "MetaCoq.SafeChecker" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure/theories" "MetaCoq.Erasure" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure-plugin/theories" "MetaCoq.ErasurePlugin" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite" "MetaCoq.TestSuite" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Equations" "Equations" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure-plugin/src" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/src" "-top" "MetaCoq.TestSuite.univ" "-R" "/tmp/tmpg6x9cc8d" "" "/tmp/tmpg6x9cc8d/MetaCoq/TestSuite/univ.v" "-q" The timeout for /github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig has been set to: 3 This file produces the following output when Coq'ed: File "/tmp/tmpg6x9cc8d/MetaCoq/TestSuite/univ.v", line 1, characters 8-21: Warning: Coq.Init.Ltac has been replaced by Stdlib.Init.Ltac. [deprecated-dirpath-Coq,deprecated-since-8.21,deprecated,default] File "/tmp/tmpg6x9cc8d/MetaCoq/TestSuite/univ.v", line 7, characters 7-20: Warning: Coq.Init.Ltac has been replaced by Stdlib.Init.Ltac. [deprecated-dirpath-Coq,deprecated-since-8.21,deprecated,default] File "/tmp/tmpg6x9cc8d/MetaCoq/TestSuite/univ.v", line 68, characters 0-96: Error: Universe inconsistency. Cannot enforce j < i because i < j. I think the error is 'Error: Universe inconsistency. Cannot enforce j < i because i < j. '. The corresponding regular expression is 'File "[^"]+", line ([0-9]+), characters [0-9-]+:\n(Error:\s+Universe\s+inconsistency\.\s+Cannot\s+enforce\s+j\s+<\s+i\s+because.*)'. Now, I will attempt to find the error message in the log... Running command: "/github/workspace/builds/coq/coq-passing/_install_ci/bin/coqc.orig" "-q" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/utils/theories" "MetaCoq.Utils" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/common/theories" "MetaCoq.Common" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/pcuic/theories" "MetaCoq.PCUIC" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq/theories" "MetaCoq.Template" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/safechecker-plugin/theories" "MetaCoq.SafeCheckerPlugin" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-pcuic/theories" "MetaCoq.TemplatePCUIC" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/safechecker/theories" "MetaCoq.SafeChecker" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/erasure/theories" "MetaCoq.Erasure" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/erasure-plugin/theories" "MetaCoq.ErasurePlugin" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/test-suite" "MetaCoq.TestSuite" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/user-contrib/Equations" "Equations" "-Q" "/github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/user-contrib/MetaCoq" "MetaCoq" "-I" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq" "-I" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/erasure-plugin/src" "-I" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/safechecker-plugin/src" "-top" "univ" "-R" "/tmp/tmpmw9qa8fg" "" "/tmp/tmpmw9qa8fg/univ.v" "-q" The timeout for /github/workspace/builds/coq/coq-passing/_install_ci/bin/coqc.orig has been set to: 6 Non-fatal error: Failed to validate all coq runs and preserve the error. The alternate coqc (/github/workspace/builds/coq/coq-passing/_install_ci/bin/coqc.orig) was supposed to pass, but instead emitted an error. Writing file to /github/workspace/cwd/tmp.v (log in /github/workspace/cwd/tmp.log). The new error was: File "/tmp/tmpmw9qa8fg/univ.v", line 1, characters 8-21: Warning: Coq.Init.Ltac has been replaced by Stdlib.Init.Ltac. [deprecated-dirpath-Coq,deprecated-since-8.21,deprecated,default] File "/tmp/tmpmw9qa8fg/univ.v", line 7, characters 7-20: Warning: Coq.Init.Ltac has been replaced by Stdlib.Init.Ltac. [deprecated-dirpath-Coq,deprecated-since-8.21,deprecated,default] File "/tmp/tmpmw9qa8fg/univ.v", line 68, characters 0-96: Error: Anomaly "Constant MetaCoq.TestSuite.univ.selfpid does not appear in the environment." Please report at http://coq.inria.fr/bugs/. Moving /github/workspace/cwd/bug_01.v to /github/workspace/cwd/tmp.v... Fatal error: Sanity check failed. ```

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

Originally posted by @coqbot-app[bot] in https://github.com/coq/coq/issues/19555#issuecomment-2354158110

JasonGross commented 1 month ago

The log says

/usr/bin/python3 /github/workspace/coq-tools/find-bug.py -y /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite/univ.v /github/workspace/cwd/bug_01.v /github/workspace/cwd/tmp.v --error-log=/github/workspace/build.log --temp-file-log=/github/workspace/cwd/tmp.log --no-deps --ignore-coq-prog-args --inline-user-contrib --coqc=/github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig --coqtop=/github/workspace/builds/coq/coq-failing/_install_ci/bin/coqtop.orig --coq_makefile=/github/workspace/builds/coq/coq-passing/_install_ci/bin/coq_makefile --coqdep /github/workspace/builds/coq/coq-passing/_install_ci/bin/coqdep --base-dir=/github/workspace/builds/coq/coq-failing/_build_ci/ -Q /github/workspace/cwd Top --verbose-include-failure-warning --verbose-include-failure-warning-prefix ::warning:: --verbose-include-failure-warning-newline %0A --nonpassing-arg=-q --nonpassing-arg=-w --nonpassing-arg=-deprecated-native-compiler-option --nonpassing-arg=-native-compiler --nonpassing-arg=no --nonpassing-I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq --nonpassing-I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq --nonpassing-I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq --nonpassing-I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq --nonpassing-I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure-plugin/src --nonpassing-I /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/src --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/utils/theories MetaCoq.Utils --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/common/theories MetaCoq.Common --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/pcuic/theories MetaCoq.PCUIC --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/pcuic/theories MetaCoq.PCUIC --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories MetaCoq.Template --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/theories MetaCoq.SafeCheckerPlugin --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-pcuic/theories MetaCoq.TemplatePCUIC --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories MetaCoq.Template --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker/theories MetaCoq.SafeChecker --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories MetaCoq.Template --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories MetaCoq.Template --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-pcuic/theories MetaCoq.TemplatePCUIC --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure/theories MetaCoq.Erasure --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/theories MetaCoq.SafeCheckerPlugin --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure-plugin/theories MetaCoq.ErasurePlugin --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite MetaCoq.TestSuite --passing-coqc=/github/workspace/builds/coq/coq-passing/_install_ci/bin/coqc.orig --passing-coqtop=/github/workspace/builds/coq/coq-passing/_install_ci/bin/coqtop.orig --passing-base-dir=/github/workspace/builds/coq/coq-passing/_build_ci/ --passing-arg=-q --passing-arg=-w --passing-arg=-deprecated-native-compiler-option --passing-arg=-native-compiler --passing-arg=no --passing-I /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq --passing-I /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq --passing-I /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq --passing-I /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq --passing-I /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/erasure-plugin/src --passing-I /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/safechecker-plugin/src --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/utils/theories MetaCoq.Utils --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/common/theories MetaCoq.Common --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/pcuic/theories MetaCoq.PCUIC --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/pcuic/theories MetaCoq.PCUIC --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq/theories MetaCoq.Template --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/safechecker-plugin/theories MetaCoq.SafeCheckerPlugin --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-pcuic/theories MetaCoq.TemplatePCUIC --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq/theories MetaCoq.Template --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/safechecker/theories MetaCoq.SafeChecker --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq/theories MetaCoq.Template --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq/theories MetaCoq.Template --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-pcuic/theories MetaCoq.TemplatePCUIC --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/erasure/theories MetaCoq.Erasure --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/safechecker-plugin/theories MetaCoq.SafeCheckerPlugin --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/erasure-plugin/theories MetaCoq.ErasurePlugin --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/test-suite MetaCoq.TestSuite -l - /github/workspace/bug.log --verbose-log-file 9999,/github/workspace/bug.verbose.log
Running command: "/github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig" "-q" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/utils/theories" "MetaCoq.Utils" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/common/theories" "MetaCoq.Common" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/pcuic/theories" "MetaCoq.PCUIC" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories" "MetaCoq.Template" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/theories" "MetaCoq.SafeCheckerPlugin" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-pcuic/theories" "MetaCoq.TemplatePCUIC" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker/theories" "MetaCoq.SafeChecker" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure/theories" "MetaCoq.Erasure" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure-plugin/theories" "MetaCoq.ErasurePlugin" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite" "MetaCoq.TestSuite" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Equations" "Equations" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/erasure-plugin/src" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker-plugin/src" "-top" "MetaCoq.TestSuite.univ" "-R" "/tmp/tmpg6x9cc8d" "" "/tmp/tmpg6x9cc8d/MetaCoq/TestSuite/univ.v" "-q"
Running command: "/github/workspace/builds/coq/coq-passing/_install_ci/bin/coqc.orig" "-q" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/utils/theories" "MetaCoq.Utils" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/common/theories" "MetaCoq.Common" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/pcuic/theories" "MetaCoq.PCUIC" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq/theories" "MetaCoq.Template" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/safechecker-plugin/theories" "MetaCoq.SafeCheckerPlugin" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-pcuic/theories" "MetaCoq.TemplatePCUIC" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/safechecker/theories" "MetaCoq.SafeChecker" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/erasure/theories" "MetaCoq.Erasure" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/erasure-plugin/theories" "MetaCoq.ErasurePlugin" "-R" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/test-suite" "MetaCoq.TestSuite" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/user-contrib/Equations" "Equations" "-Q" "/github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/user-contrib/MetaCoq" "MetaCoq" "-I" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/template-coq" "-I" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/erasure-plugin/src" "-I" "/github/workspace/builds/coq/coq-passing/_build_ci/metacoq/safechecker-plugin/src" "-top" "univ" "-R" "/tmp/tmpmw9qa8fg" "" "/tmp/tmpmw9qa8fg/univ.v" "-q"

Note "-top" "MetaCoq.TestSuite.univ" vs "-top" "univ"

JasonGross commented 1 month ago

Ah, the issue seems to be that the file is /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite/univ.v and we have --nonpassing-R /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/test-suite MetaCoq.TestSuite but only --passing-R /github/workspace/builds/coq/coq-passing/_build_ci/metacoq/test-suite MetaCoq.TestSuite

JasonGross commented 1 month ago

So I guess we should always derive the topname from the failing arguments