Error: Conversion test raised an anomaly: Anomaly "in Univ.repr: Universe plugin.51 undefined."

[JasonGross]

Fails QuickChick unit test on Coq dev: QuickChick/QuickChick@235f6f2/test/plugin/plugin.v#L51

File "./plugin.v", line 51, characters 0-22:
Error: Conversion test raised an anomaly:
Anomaly "in Univ.repr: Universe plugin.51 undefined."

@JasonGross any idea regarding the new (Universe?) issue with QuickChick?
The failing example blocks this PR from being merged, otherwise IIUC would break Coq CI.

Originally posted by @liyishuai in rocq-community/coq-ext-lib#136 (comment)

Can we get coqbot to minimize it for us? Something like
@coqbot minimize coq.dev

git clone git@github.com:JasonGross/coq-ext-lib.git --branch=cumul
cd coq-ext-lib
opam pin add -y .
opam install -y coq-quickchick

Originally posted by @JasonGross in rocq-community/coq-ext-lib#136 (comment)

[coqbot-app]

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

[JasonGross]

@coqbot minimize coq.dev

git clone https://github.com/JasonGross/coq-ext-lib.git --branch=cumul
cd coq-ext-lib
opam pin add -y .
opam install -y coq-quickchick

[coqbot-app]

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

[JasonGross]

@coqbot minimize coq.dev

git clone https://github.com/JasonGross/coq-ext-lib.git --branch=cumul
cd coq-ext-lib
opam pin add -y .
opam install -y -vv -t coq-quickchick

[coqbot-app]

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

[liyishuai]

Consider:

git clone https://github.com/QuickChick/QuickChick.git
cd QuickChick
opam pin add -n .
opam install --deps-only -y coq-quickchick
make
make install
make tests

[JasonGross]

@coqbot minimize coq.dev

git clone https://github.com/JasonGross/coq-ext-lib.git --branch=cumul
cd coq-ext-lib
opam pin add -y .
cd ..
git clone https://github.com/QuickChick/QuickChick.git
cd QuickChick
opam pin add -n .
opam install --deps-only -y coq-quickchick
make
make install
make tests

[coqbot-app]

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

[JasonGross]

Running here, in case the minimizer is still having trouble responding.

[coqbot-app]

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

🌟 Minimized Coq File (consider adding this file to the test-suite)

(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/QuickChick/src" "QuickChick" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/ExtLib" "ExtLib" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/HB" "HB" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/QuickChick" "QuickChick" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/SimpleIO" "SimpleIO" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/elpi" "elpi" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/mathcomp" "mathcomp" "-top" "plugin") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 81 lines to 7 lines, then from 20 lines to 191 lines, then from 193 lines to 11 lines, then from 24 lines to 961 lines, then from 959 lines to 36 lines, then from 49 lines to 1451 lines, then from 1441 lines to 35 lines, then from 48 lines to 961 lines, then from 964 lines to 36 lines, then from 49 lines to 86 lines, then from 91 lines to 36 lines, then from 49 lines to 168 lines, then from 173 lines to 53 lines, then from 66 lines to 435 lines, then from 440 lines to 76 lines, then from 81 lines to 76 lines *)
(* coqc version 8.20+alpha compiled with OCaml 4.13.1
   coqtop version buildkitsandbox:/home/coq/.opam/4.13.1+flambda/.opam-switch/build/coq-core.dev/_build/default,master (8561d71d3b0440ce7fe2e903055e314fa174d6c2)
   Expected coqc runtime on this file: 0.224 sec *)
Require Coq.Strings.String.

Module Export QuickChick_DOT_Show_WRAPPED.
Module Export Show.
Import Coq.Strings.String.

Class Show (A : Type) : Type :=
{
  show : A -> string
}.
#[global]
Instance showNat : Show nat.
Admitted.
#[global]
Instance showList {A : Type} `{_ : Show A} : Show (list A).
Admitted.
#[global]
Instance showOpt {A : Type} `{_ : Show A} : Show (option A).
Admitted.

End Show.
Module Export QuickChick.
Module Export Show.
Include QuickChick_DOT_Show_WRAPPED.Show.
Module Export Monad.
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.

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 liftM@{d c}
              {m : Type@{d} -> Type@{c}}
              {M : Monad m}
              {T U : Type@{d}} (f : T -> U) : m T -> m U.
Admitted.

End monadic.

End Monad.

Axiom RandomSeed : Type.

Module Export QuickChick_DOT_Generators_WRAPPED.
Module Export Generators.

Set Implicit Arguments.

Inductive GenType (A:Type) : Type := MkGen : (nat -> RandomSeed -> A) -> GenType A.

Definition G := GenType.
Definition returnGen {A : Type} (x : A) : G A.
Admitted.
Definition bindGen {A B : Type} (g : G A) (k : A -> G B) : G B.
Admitted.

#[global] Instance MonadGen : Monad G :=
  { ret := @returnGen
  ; bind := @bindGen }.
Definition sampleGen (A : Type) (g : G A) : list A.
Admitted.

End Generators.
Module Export QuickChick.
Module Export Generators.
Include QuickChick_DOT_Generators_WRAPPED.Generators.

Declare ML Module "coq-quickchick.plugin".
Definition a : G nat.
Admitted.
Sample (liftM Some a).

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

🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)

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

chThat A%type_scope P%function_scope
Arguments Build_GenSizedSuchThat A%type_scope
  (P arbitrarySizeST)%function_scope
QuickChecking (genST (fun t => balanced 1 t))
File "./Automation.v", line 244, characters 0-39:
Warning: The identifier Datatypes_nat__canonical__eqtype_Equality contains __
which is reserved for the extraction
[extraction-reserved-identifier,extraction,default]
File "./Automation.v", line 244, characters 0-39:
Warning: The identifier Datatypes_nat__canonical__eqtype_Equality contains __
which is reserved for the extraction
[extraction-reserved-identifier,extraction,default]
[Some Leaf; Some Leaf; Some Leaf; Some Leaf; Some Node 4 Leaf Leaf; Some Leaf; Some Leaf; Some Node 3 Leaf Leaf; Some Node 1 Leaf Leaf; Some Leaf; Some Leaf]
Time Elapsed: 0.002830s

QuickChecking prop_gen_balanced_is_balanced
File "./Automation.v", line 274, characters 0-41:
Warning: The identifier Datatypes_nat__canonical__eqtype_Equality contains __
which is reserved for the extraction
[extraction-reserved-identifier,extraction,default]
File "./Automation.v", line 274, characters 0-41:
Warning: The identifier Datatypes_nat__canonical__eqtype_Equality contains __
which is reserved for the extraction
[extraction-reserved-identifier,extraction,default]
+++ Passed 10000 tests (0 discards)
Time Elapsed: 0.204384s

QuickChecking (balanced_preserves_balanced 10 5)
File "./Automation.v", line 290, characters 0-46:
Warning: The identifier Datatypes_nat__canonical__eqtype_Equality contains __
which is reserved for the extraction
[extraction-reserved-identifier,extraction,default]
File "./Automation.v", line 290, characters 0-46:
Warning: The identifier Datatypes_nat__canonical__eqtype_Equality contains __
which is reserved for the extraction
[extraction-reserved-identifier,extraction,default]
*** Gave up! Passed only 0 tests
Discarded: 20000
Time Elapsed: 0.198567s

QuickChecking (prop_balanced_preserves_balanced 5)
File "./Automation.v", line 309, characters 0-48:
Warning: The identifier Datatypes_nat__canonical__eqtype_Equality contains __
which is reserved for the extraction
[extraction-reserved-identifier,extraction,default]
File "./Automation.v", line 309, characters 0-48:
Warning: The identifier Datatypes_nat__canonical__eqtype_Equality contains __
which is reserved for the extraction
[extraction-reserved-identifier,extraction,default]
Node 0 (Node 0 (Node 0 (Node 0 (Node 0 Leaf Leaf) (Node 0 Leaf Leaf)) (Node 0 Leaf Leaf)) (Node 0 (Node 0 Leaf (Node 0 Leaf Leaf)) (Node 0 (Node 0 Leaf Leaf) Leaf))) (Node 0 (Node 0 (Node 0 Leaf Leaf) (Node 0 Leaf (Node 0 Leaf Leaf))) (Node 0 (Node 0 Leaf (Node 0 Leaf Leaf)) (Node 0 (Node 0 Leaf Leaf) (Node 0 Leaf Leaf))))
10
*** Failed after 1 tests and 0 shrinks. (0 discards)
Time Elapsed: 0.003014s

COQC DerivingProofs.v
MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/QuickChick/tutorials
MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -w -deprecated-native-compiler-option -native-compiler no -I /github/workspace/QuickChick/tutorials -R /github/workspace/QuickChick/tutorials Top DerivingProofs.v 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.F1xv9suqYY
MINIMIZER_DEBUG: files:  DerivingProofs.v
EnumSizedreg_exp : forall {T : Type}, Enum T -> EnumSized (reg_exp T)

EnumSizedreg_exp is not universe polymorphic
Arguments EnumSizedreg_exp {T}%type_scope {mu0_}
EnumSizedreg_exp is transparent
Expands to: Constant Top.DerivingProofs.EnumSizedreg_exp
DecOptexp_match :
forall {T : Type},
Dec_Eq T ->
Enum T -> forall (l_ : list T) (e_ : reg_exp T), DecOpt (l_ =~ e_)

DecOptexp_match is not universe polymorphic
Arguments DecOptexp_match {T}%type_scope {mu9_ mu10_} l_%list_scope e_
DecOptexp_match is transparent
Expands to: Constant Top.DerivingProofs.DecOptexp_match
EnumSizedSuchThatexp_match :
forall {T : Type},
Dec_Eq T ->
Enum T ->
forall e_ : reg_exp T,
EnumSizedSuchThat (list T) (fun l_ : list T => l_ =~ e_)

EnumSizedSuchThatexp_match is not universe polymorphic
Arguments EnumSizedSuchThatexp_match {T}%type_scope {mu19_ mu20_} e_
EnumSizedSuchThatexp_match is transparent
Expands to: Constant Top.DerivingProofs.EnumSizedSuchThatexp_match
MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/QuickChick/tutorials
MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig --print-version 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.RbDFQZv00y
MINIMIZER_DEBUG: files: 
make[2]: Leaving directory '/github/workspace/QuickChick/tutorials'
make[1]: Leaving directory '/github/workspace/QuickChick/tutorials'
make -C test
make[1]: Entering directory '/github/workspace/QuickChick/test'
cd mutation/; sh mutation.sh
MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/QuickChick/test/mutation
MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -Q /github/workspace/QuickChick/src QuickChick mutation.v 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.StjRXVzBH6
MINIMIZER_DEBUG: files:  mutation.v
File "./mutation.v", line 17, characters 0-30:
Warning: The extraction is currently set to bypass opacity, the following
opaque constant bodies have been accessed
: ssrnat.eqnP StringOT.StringOT.compare ssrbool.iffP ssrbool.idP
  StringOT.AsciiOT.compare.
 [extraction-opaque-accessed,extraction,default]
File "./mutation.v", line 17, characters 0-30:
Warning: Setting extraction output directory by default to
"/github/workspace/QuickChick/test/mutation". Use
"Set Extraction Output Directory" to set a different directory for extracted
files to appear in. [extraction-default-directory,extraction,default]
File "./mutation.v", line 17, characters 0-30:
Warning: The identifier Datatypes_nat__canonical__eqtype_Equality contains __
which is reserved for the extraction
[extraction-reserved-identifier,extraction,default]
File "./mutation.v", line 17, characters 0-30:
Warning: The identifier Datatypes_nat__canonical__eqtype_Equality contains __
which is reserved for the extraction
[extraction-reserved-identifier,extraction,default]
ocamlfind ocamldep -package zarith -modules mutation.ml > mutation.ml.depends
ocamlfind ocamldep -package zarith -modules mutation.mli > mutation.mli.depends
ocamlfind ocamlc -c -package zarith -o mutation.cmi mutation.mli
ocamlfind ocamlopt -c -package zarith -o mutation.cmx mutation.ml
ocamlfind ocamlopt -linkpkg -package zarith mutation.cmx -o mutation.native
Checking example...
+++ Passed 10000 tests (0 discards)

xargs: warning: options --max-args and --replace/-I/-i are mutually exclusive, ignoring previous --max-args value
Mutant test:mutation.ml:2931:65: Testing...
Mutant test:mutation.ml:2931:65: Killed!
Mutant test:bar: Testing...
Mutant test:bar: Killed!
Mutant test:mutation.ml:2941:67: Testing...
Mutant test:mutation.ml:2941:67: Killed!
Mutant test:foo: Testing...
Mutant test:foo: Killed!
cd plugin/; sh plugin.sh
MINIMIZER_DEBUG_EXTRA: coqc: /home/coq/.opam/4.13.1+flambda/bin/coqc
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/QuickChick/test/plugin
MINIMIZER_DEBUG_EXTRA: exec: /home/coq/.opam/4.13.1+flambda/bin/coqc.orig -Q /github/workspace/QuickChick/src QuickChick plugin.v 
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.e6pxykhT3J
MINIMIZER_DEBUG: files:  plugin.v
QuickChecking (arbitrary : G foo)
[baz; baz; bar 8 (bar 5 baz); bar 1 baz; baz; baz; baz; baz; baz; bar 1 baz; baz]
Time Elapsed: 0.002787s

QuickChecking a
[1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1]
Time Elapsed: 0.002562s

QuickChecking b
[1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1]
Time Elapsed: 0.002511s

QuickChecking (liftM Some a)
File "./plugin.v", line 51, characters 0-22:
Error: Conversion test raised an anomaly:
Anomaly "in Univ.repr: Universe plugin.51 undefined."
Please report at http://coq.inria.fr/bugs/.

make[1]: *** [Makefile:13: plugin.test] Error 1
make[1]: Leaving directory '/github/workspace/QuickChick/test'
make: *** [Makefile:68: tests] Error 2

📜 🔎 Minimization Log (truncated to last 8.0KiB; full 231KiB file on GitHub Actions Artifacts under bug.log)

ntrib/QuickChick QuickChick -Q /home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/SimpleIO SimpleIO -Q /home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/elpi elpi -Q /home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/mathcomp mathcomp -top plugin -o /tmp/bug_01.vo -dump-glob bug_01.glob bug_01.v
getting bug_01.glob (/github/workspace/cwd/bug_01.glob)
getting bug_01.glob (/github/workspace/cwd/bug_01.glob)
�[92m
Succeeded in normalizing Requires.�[0m

Now, I will attempt to split up [Require] statements...
getting /github/workspace/cwd/bug_01.v
NOTE: The file /github/workspace/cwd/bug_01.v is very new (1705996264, 0 seconds old), delaying until it's a bit older
getting /github/workspace/cwd/bug_01.glob
getting /github/workspace/cwd/bug_01.glob

No Requires to split.

In order to efficiently manipulate the file, I have to break it into statements.  I will attempt to do this by matching on periods.
�[92m
Splitting successful.�[0m

I will now attempt to remove any lines after the line which generates the error.

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...
�[92m
Splitting to definitions successful.�[0m

I will now attempt to remove goals ending in [Abort.]
�[92m
Aborted removal successful.�[0m

I will now attempt to remove unused Ltacs
�[92m
Ltac removal successful.�[0m

I will now attempt to remove unused definitions

Non-fatal error: Failed to remove definitions and preserve the error.  
The new error was:
QuickChecking (liftM Some a)
File "/tmp/tmpy5uixz89/plugin.v", line 55, characters 0-22:
Error: The reference QuickChick.Generators.sampleGen was not found
in the current environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused non-instance, non-canonical structure definitions

Non-fatal error: Failed to remove non-instance definitions and preserve the error.  
The new error was:
QuickChecking (liftM Some a)
File "/tmp/tmpsp0hqugn/plugin.v", line 72, characters 0-22:
Error: The reference QuickChick.Generators.sampleGen was not found
in the current environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused variables
�[92m
Variable removal successful.�[0m

I will now attempt to remove unused contexts
�[92m
Context removal successful.�[0m

I will now attempt to replace Qed Obligation with Admit Obligations
�[92m
Admitting Qed Obligations successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting Qed Obligations unsuccessful.
No successful changes.

I will now attempt to replace Qeds with Admitteds
�[92m
Admitting Qeds successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting Qeds unsuccessful.
No successful changes.

I will now attempt to replace Qeds with admit. Defined.
�[92m
Admitting Qeds successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting Qeds unsuccessful.
No successful changes.

I will now attempt to remove goals ending in [Abort.]
�[92m
Aborted removal successful.�[0m

I will now attempt to remove unused Ltacs
�[92m
Ltac removal successful.�[0m

I will now attempt to remove unused definitions

Non-fatal error: Failed to remove definitions and preserve the error.  
The new error was:
QuickChecking (liftM Some a)
File "/tmp/tmpy5uixz89/plugin.v", line 55, characters 0-22:
Error: The reference QuickChick.Generators.sampleGen was not found
in the current environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused non-instance, non-canonical structure definitions

Non-fatal error: Failed to remove non-instance definitions and preserve the error.  
The new error was:
QuickChecking (liftM Some a)
File "/tmp/tmpsp0hqugn/plugin.v", line 72, characters 0-22:
Error: The reference QuickChick.Generators.sampleGen was not found
in the current environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused variables
�[92m
Variable removal successful.�[0m

I will now attempt to remove unused contexts
�[92m
Context removal successful.�[0m

I will now attempt to admit [abstract ...]s
�[92m
Admitting [abstract ...] successful.�[0m
�[92m
Admitting [abstract ...] successful.�[0m
Admitting [abstract ...] unsuccessful.
Admitting [abstract ...] unsuccessful.

I will now attempt to remove goals ending in [Abort.]
�[92m
Aborted removal successful.�[0m

I will now attempt to remove unused Ltacs
�[92m
Ltac removal successful.�[0m

I will now attempt to remove unused definitions

Non-fatal error: Failed to remove definitions and preserve the error.  
The new error was:
QuickChecking (liftM Some a)
File "/tmp/tmpy5uixz89/plugin.v", line 55, characters 0-22:
Error: The reference QuickChick.Generators.sampleGen was not found
in the current environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused non-instance, non-canonical structure definitions

Non-fatal error: Failed to remove non-instance definitions and preserve the error.  
The new error was:
QuickChecking (liftM Some a)
File "/tmp/tmpsp0hqugn/plugin.v", line 72, characters 0-22:
Error: The reference QuickChick.Generators.sampleGen was not found
in the current environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused variables
�[92m
Variable removal successful.�[0m

I will now attempt to remove unused contexts
�[92m
Context removal successful.�[0m

I will now attempt to replace Obligation with Admit Obligations
�[92m
Admitting Obligations successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting Obligations unsuccessful.
No successful changes.

I will now attempt to admit lemmas with Admitted
�[92m
Admitting lemmas successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting lemmas unsuccessful.
No successful changes.

I will now attempt to admit definitions with Admitted
�[92m
Admitting definitions successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting definitions unsuccessful.
No successful changes.

I will now attempt to admit lemmas with admit. Defined
�[92m
Admitting lemmas successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting lemmas unsuccessful.
No successful changes.

I will now attempt to admit definitions with admit. Defined
�[92m
Admitting definitions successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting definitions unsuccessful.
No successful changes.

I will now attempt to export modules
Module exportation unsuccessful.

I will now attempt to split imports and exports
Import/Export splitting unsuccessful.

I will now attempt to split := definitions
One-line definition splitting unsuccessful.

I will now attempt to remove all lines, one at a time
Line removal unsuccessful.

I will now attempt to remove goals ending in [Abort.]
�[92m
Aborted removal successful.�[0m

I will now attempt to remove unused Ltacs
�[92m
Ltac removal successful.�[0m

I will now attempt to remove unused definitions

Non-fatal error: Failed to remove definitions and preserve the error.  
The new error was:
QuickChecking (liftM Some a)
File "/tmp/tmpy5uixz89/plugin.v", line 55, characters 0-22:
Error: The reference QuickChick.Generators.sampleGen was not found
in the current environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused non-instance, non-canonical structure definitions

Non-fatal error: Failed to remove non-instance definitions and preserve the error.  
The new error was:
QuickChecking (liftM Some a)
File "/tmp/tmpsp0hqugn/plugin.v", line 72, characters 0-22:
Error: The reference QuickChick.Generators.sampleGen was not found
in the current environment.


�[93mIntermediate code not saved.�[0m

I will now attempt to remove unused variables
�[92m
Variable removal successful.�[0m

I will now attempt to remove unused contexts
�[92m
Context removal successful.�[0m

I will now attempt to remove empty sections

No empty sections to remove.

Now, I will attempt to strip repeated newlines and trailing spaces from this file...

No strippable newlines or 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.

[JasonGross]

Looks like an issue in QuickChick, so closing for now