Set Polymorphic Inductive Cumulativity

JasonGross commented 1 year ago

This is required for Monad for use in metacoq, I believe, but I figured I would set the flag everywhere while I'm at it. Maybe CoqExtLib should have some file of DefaultOptions or something with #[export] Set ... for all the options, that is Imported by the relevant files?

[x] QuickChick/QuickChick#349
[x] coq/opam#2889

liyishuai commented 1 year ago

8.9: Maybe time to drop support, unless a quick fix is available.
8.11: Coqdoc problems usually disappear by rerunning the CI.
dev: ITree was broken long ago, non-blocking.
8.16, 8.17: Incompatibility with QuickChick should be resolved.

JasonGross commented 1 year ago

I've fixed compatibility with Coq 8.9, let me look at quickcheck

JasonGross commented 1 year ago

The issue with QuickChick seems to be a bug in Coq's legacy (apply) unification, I'm currently minimizing it.

JasonGross commented 1 year ago

The issue with QuickCheck is https://github.com/coq/coq/issues/17566. I'm not sure what we should do here, options I see are:

Remove Opaque ret
Fully instantiate the lemma being applyd
Use pose proof instead of apply
Give up on this PR?

gmalecha commented 1 year ago

I don't think we should give up on the PR. @JasonGross is one of the (relatively) few people that actually understands universes, so getting that insight in here to benefit everyone seems a good thing.

Will the Coq but be fixed?

JasonGross commented 1 year ago

Will the Coq bug be fixed?

I'm not sure. I certainly don't understand the code well enough to write a patch. @SkySkimmer says:

Old unification only understands inductive cumulativity in the syntactic equality fast path IIRC https://github.com/coq/coq/pull/14758

Or alternatively if https://github.com/coq/coq/issues/17565 is granted then users can just Set New Unification In Tactics or whatever the flag ends up being called. Or we can try to get rapply ... in .... Someday hopefully the old unification engine will be removed and replaced by the new one, but I'm not sure how far off that if.

liyishuai commented 1 year ago

Or we can alter QuickChick to make it compatible with here.

liyishuai commented 9 months ago

Fails QuickChick unit test on Coq dev: https://github.com/QuickChick/QuickChick/blob/235f6f2156b06239d10e971b7f229f18b73fb67c/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."

liyishuai commented 8 months ago

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.

JasonGross commented 8 months ago

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

JasonGross commented 8 months ago

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.

I see

  <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
  -> retrieved coq-quickchick.dev  (git+https://github.com/QuickChick/QuickChick#master)
  Error:  The installation of coq-quickchick failed at "make -j 3 tests".

  #=== ERROR while installing coq-quickchick.dev ================================#
  # context              2.1.5 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.4.13.1+options | https://coq.inria.fr/opam/extra-dev#2024-01-08 09:50
  # path                 ~/.opam/4.13.1+flambda/.opam-switch/build/coq-quickchick.dev
  # command              /usr/bin/make -j 3 tests
  # exit-code            2
  # env-file             ~/.opam/log/coq-quickchick-5176-be5acb.env
  # output-file          ~/.opam/log/coq-quickchick-5176-be5acb.out
  ### output ###
  # +++ 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:2917:65: Testing...
  # Mutant test:mutation.ml:2917:65: Killed!
  # Mutant test:bar: Testing...
  # Mutant test:bar: Killed!
  # Mutant test:mutation.ml:2927:67: Testing...
  # Mutant test:mutation.ml:2927:67: Killed!
  # Mutant test:foo: Testing...
  # Mutant test:foo: Killed!
  # make[1]: Leaving directory '/home/coq/.opam/4.13.1+flambda/.opam-switch/build/coq-quickchick.dev/test'
  # make: *** [Makefile:68: tests] Error 2

  <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
  +- The following actions failed
  | - install coq-quickchick dev
  +- 
  - No changes have been performed

on CI. What should I pass opam install to see the anomaly?

liyishuai commented 8 months ago

I might have changed the test suite in coq/opam#2897. Locating this problem on my side.

JasonGross commented 8 months ago

@liyishuai here's the minimized example. Any ideas for tracking down what's going on? Is QuickChick internally relying on some ext-lib structure not being cumulative?

@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)

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

```coq (* -*- 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). ```

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

```coq ```

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

```coq ```

:scroll: Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 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 ```

:scroll: :mag_right: 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.

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

liyishuai commented 8 months ago

Is QuickChick internally relying on some ext-lib structure not being cumulative?

I don't think so. @Lysxia any ideas?

JasonGross commented 8 months ago

Slightly more minimal example. Removing Cumulative makes it pass

Require Coq.Strings.String.
Module Export Monad.
Set Universe Polymorphism.
Cumulative 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
}.
Axiom liftM@{d c} : forall {m : Type@{d} -> Type@{c}} {M : Monad m} {T U : Type@{d}} (f : T -> U), m T -> m U.
End Monad.
Module Export QuickChick.
Module Export Show.
Import Coq.Strings.String.
Class Show (A : Type) : Type := { show : A -> string }.
#[global] Declare Instance showNat : Show nat.
#[global] Declare Instance showList {A : Type} `{_ : Show A} : Show (list A).
#[global] Declare Instance showOpt {A : Type} `{_ : Show A} : Show (option A).
End Show.
Module Export Generators.
Set Implicit Arguments.
Axiom G : Type -> Type.
#[global] Declare Instance MonadGen : Monad G.
Axiom sampleGen : forall (A : Type) (g : G A), list A.
End Generators.
End QuickChick.
Declare ML Module "coq-quickchick.plugin".
Definition a : G nat.
Admitted.
Sample (liftM Some a).

JasonGross commented 8 months ago

Reported upstream as https://github.com/QuickChick/QuickChick/issues/352

JasonGross commented 8 months ago

I'm guessing the issue is that the evd from interp_constr is being thrown away in let (c,_evd) = interp_constr env evd c in https://github.com/QuickChick/QuickChick/blob/235f6f2156b06239d10e971b7f229f18b73fb67c/plugin/quickChick.mlg.cppo#L298-L302

coq-community / coq-ext-lib

Set Polymorphic Inductive Cumulativity #136