search

coq-community / run-coq-bug-minimizer

Repository for triggering runs of the Coq bug minimizer using GitHub Actions [maintainer=@JasonGross]
MIT License
2 stars 0 forks source link

Missing new lines in reply messages. #1

Closed jtcoolen closed 4 years ago

jtcoolen commented 4 years ago

They were missing new lines in the replies from coqbot, messing with the rendering of the details HTML tags.

JasonGross commented 4 years ago

Good catch, thanks!

JasonGross commented 4 years ago

Testing:

JasonGross commented 4 years ago

Testing:

JasonGross commented 4 years ago

Testing:

@coqbot minimize

# You can insert a bash script which produces the error message here,
# our bot will answer with a stripped down version of it.
# Example:
#opam install -y coq-ext-lib
#eval $(opam env)
#mkdir temp
#cd temp
#wget https://github.com/coq/coq/files/4698509/bug.v.zip
#unzip bug.v.zip
#coqc -q bug.v
JasonGross commented 4 years ago

@coqbot: run CI now

JasonGross commented 4 years ago

Testing:

@coqbot: run CI now

JasonGross commented 4 years ago

@coqbot: minimize it

opam install -y coq-ext-lib
eval $(opam env)

mkdir temp
cd temp
wget https://github.com/coq/coq/files/4698509/bug.v.zip
unzip bug.v.zip
coqc -q bug.v
coqbot commented 4 years 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 commented 4 years ago

@JasonGross, Minimized File ./bug.v

Minimized Coq File ```coq (* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "Cava" "Cava" "-top" "Netlist" "-R" "." "Top" "-Q" "/home/runner/.opam/4.08.1/lib/coq/user-contrib/ExtLib" "ExtLib" "-Q" "/home/runner/.opam/4.08.1/lib/coq/user-contrib/Ltac2" "Ltac2") -*- *) (* File reduced by coq-bug-finder from original input, then from 382 lines to 167 lines, then from 421 lines to 276 lines, then from 554 lines to 314 lines, then from 540 lines to 355 lines, then from 404 lines to 361 lines, then from 375 lines to 362 lines, then from 393 lines to 362 lines, then from 520 lines to 383 lines, then from 433 lines to 383 lines, then from 497 lines to 409 lines, then from 422 lines to 408 lines *) (* coqc version 8.11.1 (July 2020) compiled on Jul 18 2020 21:40:16 with OCaml 4.08.1 coqtop version 8.11.1 (July 2020) *) Require Coq.Strings.String. Require Coq.ZArith.ZArith. Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type := { ret : forall {t : Type@{d}}, t -> m t ; bind : forall {t u : Type@{d}}, m t -> (t -> m u) -> m u }. Section monadic. Definition mcompose@{c d} {m:Type@{d}->Type@{c}} {M: Monad m} {T U V:Type@{d}} (f: T -> m U) (g: U -> m V): (T -> m V) := fun x => bind (f x) g. End monadic. Delimit Scope monad_scope with monad. Notation "f >=> g" := (@mcompose _ _ _ _ _ f g) (at level 61, right associativity) : monad_scope. Notation "x <- c1 ;; c2" := (@bind _ _ _ _ c1 (fun x => c2)) (at level 61, c1 at next level, right associativity) : monad_scope. Notation "e1 ;; e2" := (_ <- e1%monad ;; e2%monad)%monad (at level 61, right associativity) : monad_scope. Notation "' pat <- c1 ;; c2" := (@bind _ _ _ _ c1 (fun x => match x with pat => c2 end)) (at level 61, pat pattern, c1 at next level, right associativity) : monad_scope. Module Export StateMonad. Set Implicit Arguments. Section StateType. Variable S : Type. Record state (t : Type) : Type := mkState { runState : S -> t * S }. Global Instance Monad_state : Monad state := { ret := fun _ v => mkState (fun s => (v, s)) ; bind := fun _ _ c1 c2 => mkState (fun s => let (v,s) := runState c1 s in runState (c2 v) s) }. End StateType. End StateMonad. Import Coq.Strings.String. Import Coq.ZArith.ZArith. Inductive Signal : Type := | Gnd: Signal | Vcc: Signal | Wire: N -> Signal | NamedWire: string -> Signal. Import Coq.Lists.List. Import ListNotations. Open Scope monad_scope. Inductive shape {A: Type} : Type := | Empty : shape | One : A -> shape | Tuple2 : shape -> shape -> shape. Inductive Kind : Type := | Bit : Kind | BitVec : list nat -> Kind . Notation bundle := (@shape Kind). Fixpoint denoteBitVecWith {A : Type} (T : Type) (n : list A) : Type := match n with | [] => T | [x] => list T | x::xs => list (denoteBitVecWith T xs) end. Definition denoteKindWith (k : Kind) (T : Type) : Type := match k with | Bit => T | BitVec v => denoteBitVecWith T v end. Fixpoint mapBitVec {A B} (f: A -> B) (i : list nat) (l : list nat) : @denoteBitVecWith nat A l -> @denoteBitVecWith nat B l := match l, i return @denoteBitVecWith nat A l -> @denoteBitVecWith nat B l with | [], _ => f | [x], [_] => map f | x::xs, p::ps => map (mapBitVec f ps xs) | _, _ => fun _ => [] end. Fixpoint signalTy (T : Type) (s : shape) : Type := match s with | Empty => unit | One t => denoteKindWith t T | Tuple2 s1 s2 => prod (signalTy T s1) (signalTy T s2) end. Inductive ConstExpr : Type := | HexLiteral: nat -> N -> ConstExpr | StringLiteral: string -> ConstExpr. Inductive Instance : Type := | WireInputBit: string -> Signal -> Instance | WireInputBitVec: forall sizes, string -> @denoteBitVecWith nat Signal sizes -> Instance | WireOutputBit: string -> Signal -> Instance | WireOutputBitVec: forall sizes, string -> @denoteBitVecWith nat Signal sizes -> Instance | Not: Signal -> Signal -> Instance | And: Signal -> Signal -> Signal -> Instance | Nand: Signal -> Signal -> Signal -> Instance | Or: Signal -> Signal -> Signal -> Instance | Nor: Signal -> Signal -> Signal -> Instance | Xor: Signal -> Signal -> Signal -> Instance | Xnor: Signal -> Signal -> Signal -> Instance | Buf: Signal -> Signal -> Instance | DelayBit: Signal -> Signal -> Instance | AssignBit: Signal -> Signal -> Instance | UnsignedAdd : list Signal -> list Signal -> list Signal -> Instance | IndexBitArray: list Signal -> list Signal -> Signal -> Instance | IndexArray: list (list Signal) -> list Signal -> list Signal -> Instance | Component: string -> list (string * ConstExpr) -> list (string * Signal) -> Instance. Notation Netlist := (list Instance). Import Coq.Classes.Morphisms. Reserved Infix "~>" (at level 90, no associativity). Reserved Infix ">>>" (at level 53, right associativity). Reserved Infix "=M=" (at level 54, no associativity). Reserved Infix "**" (at level 30, right associativity). Class Category := { object : Type; morphism : object -> object -> Type where "a ~> b" := (morphism a b); id {x} : x ~> x; compose {x y z} (f: y ~> z) (g : x ~> y) : x ~> z where "g >>> f" := (compose f g); morphism_equivalence: forall x y (f g: x ~> y), Prop where "f =M= g" := (morphism_equivalence _ _ f g); morphism_setoid_equivalence : forall x y , Equivalence (morphism_equivalence x y); compose_respects_equivalence : forall x y z , Proper (morphism_equivalence y z ==> morphism_equivalence x y ==> morphism_equivalence x z) compose; id_left {x y} (f: x ~> y) : (id >>> f) =M= f; id_right {x y} (f: x ~> y) : (f >>> id) =M= f; associativity {x y z w} {f: x~>y} {g: y~>z} {h: z~>w} : (f >>> g) >>> h =M= f >>> (g >>> h); }. Notation "x ~> y" := (morphism x y) : category_scope. Notation "g >>> f" := (compose f g) : category_scope. Notation "f =M= g" := (morphism_equivalence _ _ f g) : category_scope. Open Scope category_scope. Class Arrow := { cat :> Category; unit : object; product : object -> object -> object where "x ** y" := (product x y); copy {x} : x ~> x**x; drop {x} : x ~> unit; swap {x y} : x**y ~> y**x; first {x y z} (f : x ~> y) : x ** z ~> y ** z; second {x y z} (f : x ~> y) : z ** x ~> z ** y; exl {x y} : x ** y ~> x; exr {x y} : x ** y ~> y; uncancell {x} : x ~> unit**x; uncancelr {x} : x ~> x**unit; assoc {x y z} : ((x**y)**z) ~> (x**(y**z)); unassoc {x y z} : (x**(y**z)) ~> ((x**y)**z); exl_unit_uncancelr x: @exl x unit >>> uncancelr =M= id; exr_unit_uncancell x: @exr unit x >>> uncancell =M= id; uncancelr_exl x: uncancelr >>> @exl x unit =M= id; uncancell_exr x: uncancell >>> @exr unit x =M= id; drop_annhilates {x y} (f: x~>y): f >>> drop =M= drop; exl_unit_is_drop {x}: @exl unit x =M= drop; exr_unit_is_drop {x}: @exr x unit =M= drop; first_first {x y z w} (f: x~>y) (g:y~>z): @first x y w f >>> first g =M= first (f >>> g); second_second {x y z w} (f: x~>y) (g:y~>z): @second x y w f >>> second g =M= second (f >>> g); swap_swap {x y}: @swap x y >>> swap =M= id; first_id {x w}: @first x x w id =M= id; second_id {x w}: @second x x w id =M= id; first_f {x y w} (f: x~>y) (g:x~>y): f =M= g -> @first x y w f =M= first g; second_f {x y w} (f: x~>y) (g:x~>y): f =M= g -> @second x y w f =M= second g; assoc_unassoc {x y z}: @assoc x y z >>> unassoc =M= id; unassoc_assoc {x y z}: @unassoc x y z >>> assoc =M= id; first_exl {x y w} f: @first x y w f >>> exl =M= exl >>> f; second_exr {x y w} f: @second x y w f >>> exr =M= exr >>> f; }. Notation "x ** y" := (product x y) (at level 30, right associativity) : arrow_scope. Open Scope arrow_scope. Class Cava := { cava_arrow :> Arrow; bit : object; bitvec : list nat -> object; constant : bool -> (unit ~> bit); constant_vec (dimensions: list nat) : denoteBitVecWith bool dimensions -> (unit ~> bitvec dimensions); not_gate: bit ** unit ~> bit; and_gate: bit ** bit ** unit ~> bit; nand_gate: bit ** bit ** unit ~> bit; or_gate: bit ** bit ** unit ~> bit; nor_gate: bit ** bit ** unit ~> bit; xor_gate: bit ** bit ** unit ~> bit; xnor_gate: bit ** bit ** unit ~> bit; buf_gate: bit ** unit ~> bit; xorcy: bit ** bit ** unit ~> bit; muxcy: bit ** bit ** bit ** unit ~> bit; unsigned_add a b s: bitvec [a] ** bitvec [b] ** unit ~> bitvec [s]; }. #[refine] Instance NetlistCat : Category := { object := bundle; morphism X Y := signalTy Signal X -> state (Netlist * N) (signalTy Signal Y); id X x := ret x; compose X Y Z f g := g >=> f; morphism_equivalence x y f g := True; }. Proof. intros. apply Build_Equivalence. unfold Reflexive. auto. unfold Symmetric. auto. unfold Transitive. auto. intros. unfold Proper. refine (fun f => _). intros. refine (fun g => _). intros. auto. auto. auto. auto. Defined. #[refine] Instance NetlistArr : Arrow := { cat := NetlistCat; unit := Empty; product := Tuple2; first X Y Z f '(z,y) := x <- f z ;; ret (x,y); second X Y Z f '(y,z) := x <- f z ;; ret (y,x); exl X Y '(x,y) := ret x; exr X Y '(x,y) := ret y; drop _ _ := ret Datatypes.tt; copy _ x := ret (x,x); swap _ _ '(x,y) := ret (y,x); uncancell _ x := ret (tt, x); uncancelr _ x := ret (x, tt); assoc _ _ _ '((x,y),z) := ret (x,(y,z)); unassoc _ _ _ '(x,(y,z)) := ret ((x,y),z); }. Proof. intros. simpl; auto. simpl; auto. simpl; auto. simpl; auto. simpl; auto. simpl; auto. simpl; auto. simpl; auto. simpl; auto. simpl; auto. simpl; auto. simpl; auto. simpl; auto. simpl; auto. simpl; auto. simpl; auto. simpl; auto. simpl; auto. Defined. Instance NetlistCava : Cava := { cava_arrow := NetlistArr; bit := One Bit; bitvec n := One (BitVec n); constant b _ := match b with | true => ret 1%N | false => ret 0%N end; constant_vec n v _ := ret (mapBitVec (fun b => match b with | true => 1%N | false => 0%N end) n n v); not_gate '(x,tt) := '(nl, i) <- get ;; put (cons (Not x i) nl, Wire ((i+1)%N)) ;; ret i; and_gate '(x,(y,tt)) := '(nl, i) <- get ;; put (cons (And x y i) nl, Wire ((i+1)%N)) ;; ret i; nand_gate '(x,(y,tt)) := '(nl, i) <- get ;; put (cons (Nand x y i) nl, Wire ((i+1)%N)) ;; ret i; or_gate '(x,(y,tt)) := '(nl, i) <- get ;; put (cons (Or x y i) nl, Wire ((i+1)%N)) ;; ret i; nor_gate '(x,(y,tt)) := '(nl, i) <- get ;; put (cons (Nor x y i) nl, Wire ((i+1)%N)) ;; ret i; xor_gate '(x,(y,tt)) := '(nl, i) <- get ;; put (cons (Xor x y i) nl, Wire ((i+1)%N)) ;; ret i; xnor_gate '(x,(y,tt)) := '(nl, i) <- get ;; put (cons (Xnor x y i) nl, Wire ((i+1)%N)) ;; ret i; buf_gate '(x,tt) := '(nl, i) <- get ;; put (cons (Buf x i) nl, Wire ((i+1)%N)) ;; ret i; xorcy '(x, (y, tt)) := '(nl, i) <- get ;; put (cons (Component "XORCY" [] [("O", i); ("CI", x); ("LI", y)]) nl, Wire ((i+1)%N)) ;; ret i; muxcy '(s,(ci,(di, tt))) := '(nl, i) <- get ;; put (cons (Component "MUXCY" [] [("O", i); ("S", s); ("CI", ci); ("DI", di)]) nl, Wire ((i+1)%N)) ;; ret i; unsigned_add m n s '(x,(y, tt)) := '(nl, i) <- get ;; let o := map (compose Wire N.of_nat) (seq (N.to_nat i) s) in put (cons (UnsignedAdd x y o) nl, (i + N.of_nat s)%N) ;; ret o; }. ```
Build Log ``` ++ opam install -y coq-ext-lib The following actions will be performed: ∗ install coq-ext-lib 0.11.1 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> [coq-ext-lib.0.11.1] downloaded from https://github.com/coq-community/coq-ext-lib/archive/v0.11.1.tar.gz <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> ∗ installed coq-ext-lib.0.11.1 Done. # Run eval $(opam env) to update the current shell environment +++ opam env ++ eval 'OPAM_SWITCH_PREFIX='\''/home/runner/.opam/4.08.1'\'';' export 'OPAM_SWITCH_PREFIX;' 'CAML_LD_LIBRARY_PATH='\''/home/runner/.opam/4.08.1/lib/stublibs:/home/runner/.opam/4.08.1/lib/ocaml/stublibs:/home/runner/.opam/4.08.1/lib/ocaml'\'';' export 'CAML_LD_LIBRARY_PATH;' 'OCAML_TOPLEVEL_PATH='\''/home/runner/.opam/4.08.1/lib/toplevel'\'';' export 'OCAML_TOPLEVEL_PATH;' 'MANPATH='\'':/home/runner/.opam/4.08.1/man'\'';' export 'MANPATH;' 'PATH='\''/home/runner/.opam/4.08.1/bin:/opt/hostedtoolcache/Python/3.8.3/x64/bin:/opt/hostedtoolcache/Python/3.8.3/x64:/opt/hostedtoolcache/opam/2.0.5/x64:/home/linuxbrew/.linuxbrew/bin:/home/linuxbrew/.linuxbrew/sbin:/usr/share/rust/.cargo/bin:/home/runner/.config/composer/vendor/bin:/home/runner/.dotnet/tools:/snap/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games'\'';' export 'PATH;' +++ OPAM_SWITCH_PREFIX=/home/runner/.opam/4.08.1 +++ export OPAM_SWITCH_PREFIX +++ CAML_LD_LIBRARY_PATH=/home/runner/.opam/4.08.1/lib/stublibs:/home/runner/.opam/4.08.1/lib/ocaml/stublibs:/home/runner/.opam/4.08.1/lib/ocaml +++ export CAML_LD_LIBRARY_PATH +++ OCAML_TOPLEVEL_PATH=/home/runner/.opam/4.08.1/lib/toplevel +++ export OCAML_TOPLEVEL_PATH +++ MANPATH=:/home/runner/.opam/4.08.1/man +++ export MANPATH +++ PATH=/home/runner/.opam/4.08.1/bin:/opt/hostedtoolcache/Python/3.8.3/x64/bin:/opt/hostedtoolcache/Python/3.8.3/x64:/opt/hostedtoolcache/opam/2.0.5/x64:/home/linuxbrew/.linuxbrew/bin:/home/linuxbrew/.linuxbrew/sbin:/usr/share/rust/.cargo/bin:/home/runner/.config/composer/vendor/bin:/home/runner/.dotnet/tools:/snap/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games +++ export PATH ++ mkdir temp ++ cd temp ++ wget https://github.com/coq/coq/files/4698509/bug.v.zip --2020-07-18 21:52:01-- https://github.com/coq/coq/files/4698509/bug.v.zip Resolving github.com (github.com)... 140.82.112.4 Connecting to github.com (github.com)|140.82.112.4|:443... connected. HTTP request sent, awaiting response... 302 Found Location: https://github-production-repository-file-5c1aeb.s3.amazonaws.com/1377159/4698509?X-Amz-Algorithm=AWS4-HMAC-SHA256&X-Amz-Credential=AKIAIWNJYAX4CSVEH53A%2F20200718%2Fus-east-1%2Fs3%2Faws4_request&X-Amz-Date=20200718T215201Z&X-Amz-Expires=300&X-Amz-Signature=86833e2499df137df70082937298f865921e5764f1ac2c0997f6487f5e3e29b8&X-Amz-SignedHeaders=host&actor_id=0&repo_id=1377159&response-content-disposition=attachment%3Bfilename%3Dbug.v.zip&response-content-type=application%2Fx-zip-compressed [following] --2020-07-18 21:52:01-- https://github-production-repository-file-5c1aeb.s3.amazonaws.com/1377159/4698509?X-Amz-Algorithm=AWS4-HMAC-SHA256&X-Amz-Credential=AKIAIWNJYAX4CSVEH53A%2F20200718%2Fus-east-1%2Fs3%2Faws4_request&X-Amz-Date=20200718T215201Z&X-Amz-Expires=300&X-Amz-Signature=86833e2499df137df70082937298f865921e5764f1ac2c0997f6487f5e3e29b8&X-Amz-SignedHeaders=host&actor_id=0&repo_id=1377159&response-content-disposition=attachment%3Bfilename%3Dbug.v.zip&response-content-type=application%2Fx-zip-compressed Resolving github-production-repository-file-5c1aeb.s3.amazonaws.com (github-production-repository-file-5c1aeb.s3.amazonaws.com)... 52.216.113.91 Connecting to github-production-repository-file-5c1aeb.s3.amazonaws.com (github-production-repository-file-5c1aeb.s3.amazonaws.com)|52.216.113.91|:443... connected. HTTP request sent, awaiting response... 200 OK Length: 3013 (2.9K) [application/x-zip-compressed] Saving to: ‘bug.v.zip’ 0K .. 100% 118M=0s 2020-07-18 21:52:02 (118 MB/s) - ‘bug.v.zip’ saved [3013/3013] ++ unzip bug.v.zip Archive: bug.v.zip inflating: bug.v ++ coqc -q bug.v File "./bug.v", line 128, characters 0-53: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope category_scope.". [undeclared-scope,deprecated] File "./bug.v", line 183, characters 0-86: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope arrow_scope.". [undeclared-scope,deprecated] File "./bug.v", line 293, characters 2-1820: Error: Anomaly "File "pretyping/cases.ml", line 1719, characters 29-35: Assertion failed." Please report at http://coq.inria.fr/bugs/. ```
Minimization Log ``` Coq version: 8.11.1 (July 2020) compiled on Jul 18 2020 21:40:16 with OCaml 4.08.1 getting ./bug.v getting ./bug.glob First, I will attempt to factor out all of the [Require]s ./bug.v, and store the result in bug_01.v... getting bug.v getting bug.glob Now, I will attempt to coq the file, and find the error... Coqing the file (bug_01.v)... Running command: "coqc" "-R" "Cava" "Cava" "-top" "Netlist" "-R" "." "Top" "-Q" "/home/runner/.opam/4.08.1/lib/coq/user-contrib/ExtLib" "ExtLib" "-Q" "/home/runner/.opam/4.08.1/lib/coq/user-contrib/Ltac2" "Ltac2" "/tmp/tmpk3t081v4.v" "-q" The timeout has been set to: 3 This file produces the following output when Coq'ed: While loading initial state: Warning: Cannot open Cava [cannot-open-path,filesystem] File "/tmp/tmpk3t081v4.v", line 153, characters 0-53: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope category_scope.". [undeclared-scope,deprecated] File "/tmp/tmpk3t081v4.v", line 208, characters 0-86: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope arrow_scope.". [undeclared-scope,deprecated] File "/tmp/tmpk3t081v4.v", line 318, characters 2-1820: Error: Anomaly "File "pretyping/cases.ml", line 1719, characters 29-35: Assertion failed." Please report at http://coq.inria.fr/bugs/. I think the error is 'Error: Anomaly "File "pretyping/cases.ml", line 1719, characters 29-35: Assertion failed." Please report at http://coq.inria.fr/bugs/. '. The corresponding regular expression is 'File "[^"]+", line ([0-9]+), characters [0-9-]+:\n(Error:\sAnomaly\s"File\s+"pretyping/cases\.ml",\s+line\s+[\d]+,\s+characters\s+[\d]+\-[\d]+:\s+Assertion\s+failed\."\sPlease\s+report\s+at\s+http://coq\.inria\.fr/bugs/\.)'. Sanity check passed. 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... Succeeded in stripping comments. In order to efficiently manipulate the file, I have to break it into statements. I will attempt to do this by matching on periods. Splitting successful. I will now attempt to remove any lines after the line which generates the error. No lines to trim. 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... Splitting to definitions successful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to replace Qeds with Admitteds Admitting Qeds successful. 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.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit [abstract ...]s Admitting [abstract ...] successful. Admitting [abstract ...] successful. Admitting [abstract ...] unsuccessful. Admitting [abstract ...] unsuccessful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit lemmas Admitting lemmas successful. Failed to do everything at once; trying one at a time. Admitting lemmas unsuccessful. No successful changes. I will now attempt to admit definitions Non-fatal error: Failed to admit definitions and preserve the error. Writing intermediate code to tmp.v. The new error was: While loading initial state: Warning: Cannot open Cava [cannot-open-path,filesystem] File "/tmp/tmpvcp9q8l4.v", line 151, characters 0-53: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope category_scope.". [undeclared-scope,deprecated] File "/tmp/tmpvcp9q8l4.v", line 206, characters 0-86: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope arrow_scope.". [undeclared-scope,deprecated] File "/tmp/tmpvcp9q8l4.v", line 247, characters 0-8: Error: (in proof NetlistCat): Attempt to save an incomplete proof 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 successful I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to replace Qeds with Admitteds Admitting Qeds successful. 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.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit [abstract ...]s Admitting [abstract ...] successful. Admitting [abstract ...] successful. Admitting [abstract ...] unsuccessful. Admitting [abstract ...] unsuccessful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit lemmas Admitting lemmas successful. Failed to do everything at once; trying one at a time. Admitting lemmas unsuccessful. No successful changes. I will now attempt to admit definitions Non-fatal error: Failed to admit definitions and preserve the error. Writing intermediate code to tmp.v. The new error was: While loading initial state: Warning: Cannot open Cava [cannot-open-path,filesystem] File "/tmp/tmptgbt0lfp.v", line 127, characters 0-53: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope category_scope.". [undeclared-scope,deprecated] File "/tmp/tmptgbt0lfp.v", line 182, characters 0-86: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope arrow_scope.". [undeclared-scope,deprecated] File "/tmp/tmptgbt0lfp.v", line 223, characters 0-8: Error: (in proof NetlistCat): Attempt to save an incomplete proof 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.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. 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... Succeeded in stripping newlines and spaces. getting bug_01.v coq_makefile COQC = coqc -o Makefile1xeqf57n.coq -R . Top -R Cava Cava -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/ExtLib ExtLib -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/Ltac2 Ltac2 -R Cava Cava -R . Top -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/ExtLib ExtLib -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/Ltac2 Ltac2 -arg -top -arg Netlist bug.v bug_01.v tmp.v make -k -f Makefile1xeqf57n.coq bug_01.glob getting Coq/ZArith/ZArith.v Warning: Cannot inline Coq.ZArith.ZArith ([Errno 2] No such file or directory: 'Coq/ZArith/ZArith.v') getting Coq/Strings/String.v Warning: Cannot inline Coq.Strings.String ([Errno 2] No such file or directory: 'Coq/Strings/String.v') getting ../../../../.opam/4.08.1/lib/coq/user-contrib/ExtLib/Data/Monads/StateMonad.v getting ../../../../.opam/4.08.1/lib/coq/user-contrib/ExtLib/Data/Monads/StateMonad.glob Sanity check passed. Now, I will attempt to strip repeated newlines and trailing spaces from this file... Succeeded in stripping newlines and spaces. Now, I will attempt to strip the comments from this file... Succeeded in stripping comments. In order to efficiently manipulate the file, I have to break it into statements. I will attempt to do this by matching on periods. Splitting successful. I will now attempt to remove any lines after the line which generates the error. No lines to trim. 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... Splitting to definitions successful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to replace Qeds with Admitteds Admitting Qeds successful. 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.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit [abstract ...]s Admitting [abstract ...] successful. Admitting [abstract ...] successful. Admitting [abstract ...] unsuccessful. Admitting [abstract ...] unsuccessful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit lemmas Admitting lemmas successful. Failed to do everything at once; trying one at a time. Admitting lemmas unsuccessful. No successful changes. I will now attempt to admit definitions Non-fatal error: Failed to admit definitions and preserve the error. Writing intermediate code to tmp.v. The new error was: While loading initial state: Warning: Cannot open Cava [cannot-open-path,filesystem] File "/tmp/tmpz6uj2fl6.v", line 278, characters 0-53: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope category_scope.". [undeclared-scope,deprecated] File "/tmp/tmpz6uj2fl6.v", line 333, characters 0-86: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope arrow_scope.". [undeclared-scope,deprecated] File "/tmp/tmpz6uj2fl6.v", line 374, characters 0-8: Error: (in proof NetlistCat): Attempt to save an incomplete proof 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 successful 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 successful I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to replace Qeds with Admitteds Admitting Qeds successful. 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.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit [abstract ...]s Admitting [abstract ...] successful. Admitting [abstract ...] successful. Admitting [abstract ...] unsuccessful. Admitting [abstract ...] unsuccessful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit lemmas Admitting lemmas successful. Failed to do everything at once; trying one at a time. Admitting lemmas unsuccessful. No successful changes. I will now attempt to admit definitions Non-fatal error: Failed to admit definitions and preserve the error. Writing intermediate code to tmp.v. The new error was: While loading initial state: Warning: Cannot open Cava [cannot-open-path,filesystem] File "/tmp/tmpv9cqnzms.v", line 148, characters 0-53: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope category_scope.". [undeclared-scope,deprecated] File "/tmp/tmpv9cqnzms.v", line 203, characters 0-86: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope arrow_scope.". [undeclared-scope,deprecated] File "/tmp/tmpv9cqnzms.v", line 244, characters 0-8: Error: (in proof NetlistCat): Attempt to save an incomplete proof 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.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. 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... Succeeded in stripping newlines and spaces. getting bug_01.v WARNING: Assuming that bug_01.glob is not a valid reflection of bug_01.v because bug_01.v is newer (1595109287 >= 1595109191) coq_makefile COQC = coqc -o Makefilezc2l9dta.coq -R . Top -R Cava Cava -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/ExtLib ExtLib -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/Ltac2 Ltac2 -R Cava Cava -R . Top -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/ExtLib ExtLib -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/Ltac2 Ltac2 -arg -top -arg Netlist bug.v bug_01.v tmp.v make -k -f Makefilezc2l9dta.coq bug_01.glob getting ../../../../.opam/4.08.1/lib/coq/user-contrib/ExtLib/Structures/Monads.v getting ../../../../.opam/4.08.1/lib/coq/user-contrib/ExtLib/Structures/Monads.glob Sanity check passed. 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... Succeeded in stripping comments. In order to efficiently manipulate the file, I have to break it into statements. I will attempt to do this by matching on periods. Splitting successful. I will now attempt to remove any lines after the line which generates the error. No lines to trim. 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... Splitting to definitions successful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to replace Qeds with Admitteds Admitting Qeds successful. 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.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit [abstract ...]s Admitting [abstract ...] successful. Admitting [abstract ...] successful. Admitting [abstract ...] unsuccessful. Admitting [abstract ...] unsuccessful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit lemmas Admitting lemmas successful. Failed to do everything at once; trying one at a time. Admitting lemmas unsuccessful. No successful changes. I will now attempt to admit definitions Non-fatal error: Failed to admit definitions and preserve the error. Writing intermediate code to tmp.v. The new error was: While loading initial state: Warning: Cannot open Cava [cannot-open-path,filesystem] File "/tmp/tmpmbfo9eml.v", line 191, characters 0-53: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope category_scope.". [undeclared-scope,deprecated] File "/tmp/tmpmbfo9eml.v", line 246, characters 0-86: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope arrow_scope.". [undeclared-scope,deprecated] File "/tmp/tmpmbfo9eml.v", line 287, characters 0-8: Error: (in proof NetlistCat): Attempt to save an incomplete proof 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 successful 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 successful I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to replace Qeds with Admitteds Admitting Qeds successful. 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.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit [abstract ...]s Admitting [abstract ...] successful. Admitting [abstract ...] successful. Admitting [abstract ...] unsuccessful. Admitting [abstract ...] unsuccessful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit lemmas Admitting lemmas successful. Failed to do everything at once; trying one at a time. Admitting lemmas unsuccessful. No successful changes. I will now attempt to admit definitions Non-fatal error: Failed to admit definitions and preserve the error. Writing intermediate code to tmp.v. The new error was: While loading initial state: Warning: Cannot open Cava [cannot-open-path,filesystem] File "/tmp/tmpcxsqc2fp.v", line 148, characters 0-53: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope category_scope.". [undeclared-scope,deprecated] File "/tmp/tmpcxsqc2fp.v", line 203, characters 0-86: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope arrow_scope.". [undeclared-scope,deprecated] File "/tmp/tmpcxsqc2fp.v", line 243, characters 0-8: Error: (in proof NetlistCat): Attempt to save an incomplete proof 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.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. 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... Succeeded in stripping newlines and spaces. getting bug_01.v WARNING: Assuming that bug_01.glob is not a valid reflection of bug_01.v because bug_01.v is newer (1595109372 >= 1595109288) coq_makefile COQC = coqc -o Makefile0aqkogsu.coq -R . Top -R Cava Cava -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/ExtLib ExtLib -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/Ltac2 Ltac2 -R Cava Cava -R . Top -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/ExtLib ExtLib -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/Ltac2 Ltac2 -arg -top -arg Netlist bug.v bug_01.v tmp.v make -k -f Makefile0aqkogsu.coq bug_01.glob getting ../../../../.opam/4.08.1/lib/coq/user-contrib/ExtLib/Structures/Monad.v getting ../../../../.opam/4.08.1/lib/coq/user-contrib/ExtLib/Structures/Monad.glob Sanity check passed. 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... Succeeded in stripping comments. In order to efficiently manipulate the file, I have to break it into statements. I will attempt to do this by matching on periods. Splitting successful. I will now attempt to remove any lines after the line which generates the error. No lines to trim. 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... Splitting to definitions successful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to replace Qeds with Admitteds Admitting Qeds successful. 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.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit [abstract ...]s Admitting [abstract ...] successful. Admitting [abstract ...] successful. Admitting [abstract ...] unsuccessful. Admitting [abstract ...] unsuccessful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit lemmas Admitting lemmas successful. Failed to do everything at once; trying one at a time. Admitting lemmas unsuccessful. No successful changes. I will now attempt to admit definitions Non-fatal error: Failed to admit definitions and preserve the error. Writing intermediate code to tmp.v. The new error was: While loading initial state: Warning: Cannot open Cava [cannot-open-path,filesystem] File "/tmp/tmpyqkvxr3_.v", line 69, characters 2-39: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope monad_scope.". [undeclared-scope,deprecated] File "/tmp/tmpyqkvxr3_.v", line 256, characters 0-53: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope category_scope.". [undeclared-scope,deprecated] File "/tmp/tmpyqkvxr3_.v", line 311, characters 0-86: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope arrow_scope.". [undeclared-scope,deprecated] File "/tmp/tmpyqkvxr3_.v", line 351, characters 0-8: Error: (in proof NetlistCat): Attempt to save an incomplete proof 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 successful 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 successful I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to replace Qeds with Admitteds Admitting Qeds successful. 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.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit [abstract ...]s Admitting [abstract ...] successful. Admitting [abstract ...] successful. Admitting [abstract ...] unsuccessful. Admitting [abstract ...] unsuccessful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit lemmas Admitting lemmas successful. Failed to do everything at once; trying one at a time. Admitting lemmas unsuccessful. No successful changes. I will now attempt to admit definitions Non-fatal error: Failed to admit definitions and preserve the error. Writing intermediate code to tmp.v. The new error was: While loading initial state: Warning: Cannot open Cava [cannot-open-path,filesystem] File "/tmp/tmplpkzani4.v", line 22, characters 2-39: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope monad_scope.". [undeclared-scope,deprecated] File "/tmp/tmplpkzani4.v", line 185, characters 0-53: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope category_scope.". [undeclared-scope,deprecated] File "/tmp/tmplpkzani4.v", line 240, characters 0-86: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope arrow_scope.". [undeclared-scope,deprecated] File "/tmp/tmplpkzani4.v", line 278, characters 0-8: Error: (in proof NetlistCat): Attempt to save an incomplete proof 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 successful I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to replace Qeds with Admitteds Admitting Qeds successful. 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.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit [abstract ...]s Admitting [abstract ...] successful. Admitting [abstract ...] successful. Admitting [abstract ...] unsuccessful. Admitting [abstract ...] unsuccessful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit lemmas Admitting lemmas successful. Failed to do everything at once; trying one at a time. Admitting lemmas unsuccessful. No successful changes. I will now attempt to admit definitions Non-fatal error: Failed to admit definitions and preserve the error. Writing intermediate code to tmp.v. The new error was: While loading initial state: Warning: Cannot open Cava [cannot-open-path,filesystem] File "/tmp/tmpsa92hd56.v", line 19, characters 2-39: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope monad_scope.". [undeclared-scope,deprecated] File "/tmp/tmpsa92hd56.v", line 178, characters 0-53: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope category_scope.". [undeclared-scope,deprecated] File "/tmp/tmpsa92hd56.v", line 233, characters 0-86: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope arrow_scope.". [undeclared-scope,deprecated] File "/tmp/tmpsa92hd56.v", line 271, characters 0-8: Error: (in proof NetlistCat): Attempt to save an incomplete proof 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.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to remove empty sections Empty section removal successful. Now, I will attempt to strip repeated newlines and trailing spaces from this file... Succeeded in stripping newlines and spaces. getting bug_01.v WARNING: Assuming that bug_01.glob is not a valid reflection of bug_01.v because bug_01.v is newer (1595109488 >= 1595109373) coq_makefile COQC = coqc -o Makefileh1hbbpw_.coq -R . Top -R Cava Cava -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/ExtLib ExtLib -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/Ltac2 Ltac2 -R Cava Cava -R . Top -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/ExtLib ExtLib -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/Ltac2 Ltac2 -arg -top -arg Netlist bug.v bug_01.v tmp.v make -k -f Makefileh1hbbpw_.coq bug_01.glob getting bug_01.v WARNING: Assuming that bug_01.glob is not a valid reflection of bug_01.v because bug_01.v is newer (1595109489 >= 1595109489) coq_makefile COQC = coqc -o Makefile9n19d8fh.coq -R . Top -R Cava Cava -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/ExtLib ExtLib -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/Ltac2 Ltac2 -R Cava Cava -R . Top -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/ExtLib ExtLib -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/Ltac2 Ltac2 -arg -top -arg Netlist bug.v bug_01.v tmp.v make -k -f Makefile9n19d8fh.coq bug_01.glob getting bug_01.v WARNING: Assuming that bug_01.glob is not a valid reflection of bug_01.v because bug_01.v is newer (1595109489 >= 1595109489) coq_makefile COQC = coqc -o Makefilev3fgq3za.coq -R . Top -R Cava Cava -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/ExtLib ExtLib -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/Ltac2 Ltac2 -R Cava Cava -R . Top -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/ExtLib ExtLib -Q /home/runner/.opam/4.08.1/lib/coq/user-contrib/Ltac2 Ltac2 -arg -top -arg Netlist bug.v bug_01.v tmp.v make -k -f Makefilev3fgq3za.coq bug_01.glob Sanity check passed. 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... Succeeded in stripping comments. In order to efficiently manipulate the file, I have to break it into statements. I will attempt to do this by matching on periods. Splitting successful. I will now attempt to remove any lines after the line which generates the error. No lines to trim. 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... Splitting to definitions successful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to replace Qeds with Admitteds Admitting Qeds successful. 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.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit [abstract ...]s Admitting [abstract ...] successful. Admitting [abstract ...] successful. Admitting [abstract ...] unsuccessful. Admitting [abstract ...] unsuccessful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit lemmas Admitting lemmas successful. Failed to do everything at once; trying one at a time. Admitting lemmas unsuccessful. No successful changes. I will now attempt to admit definitions Non-fatal error: Failed to admit definitions and preserve the error. Writing intermediate code to tmp.v. The new error was: While loading initial state: Warning: Cannot open Cava [cannot-open-path,filesystem] File "/tmp/tmpsq1oo3se.v", line 30, characters 2-39: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope monad_scope.". [undeclared-scope,deprecated] File "/tmp/tmpsq1oo3se.v", line 183, characters 0-53: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope category_scope.". [undeclared-scope,deprecated] File "/tmp/tmpsq1oo3se.v", line 238, characters 0-86: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope arrow_scope.". [undeclared-scope,deprecated] File "/tmp/tmpsq1oo3se.v", line 276, characters 0-8: Error: (in proof NetlistCat): Attempt to save an incomplete proof 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 successful I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to replace Qeds with Admitteds Admitting Qeds successful. 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.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit [abstract ...]s Admitting [abstract ...] successful. Admitting [abstract ...] successful. Admitting [abstract ...] unsuccessful. Admitting [abstract ...] unsuccessful. I will now attempt to remove goals ending in [Abort.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. I will now attempt to admit lemmas Admitting lemmas successful. Failed to do everything at once; trying one at a time. Admitting lemmas unsuccessful. No successful changes. I will now attempt to admit definitions Non-fatal error: Failed to admit definitions and preserve the error. Writing intermediate code to tmp.v. The new error was: While loading initial state: Warning: Cannot open Cava [cannot-open-path,filesystem] File "/tmp/tmpgt_ejdtq.v", line 22, characters 2-39: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope monad_scope.". [undeclared-scope,deprecated] File "/tmp/tmpgt_ejdtq.v", line 175, characters 0-53: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope category_scope.". [undeclared-scope,deprecated] File "/tmp/tmpgt_ejdtq.v", line 230, characters 0-86: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope arrow_scope.". [undeclared-scope,deprecated] File "/tmp/tmpgt_ejdtq.v", line 268, characters 0-8: Error: (in proof NetlistCat): Attempt to save an incomplete proof 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.] Aborted removal successful. I will now attempt to remove unused Ltacs Ltac removal successful. I will now attempt to remove unused definitions Definition removal successful. I will now attempt to remove unused non-instance, non-canonical structure definitions Non-instance definition removal successful. I will now attempt to remove unused variables Variable removal successful. I will now attempt to remove unused contexts Context removal successful. 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... Succeeded in stripping newlines and spaces. ```

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.