Set Polymorphic Inductive Cumulativity #136
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
|
I've fixed compatibility with Coq 8.9, let me look at quickcheck |
|
The issue with QuickChick seems to be a bug in Coq's legacy ( |
|
The issue with QuickCheck is coq/coq#17566. I'm not sure what we should do here, options I see are:
|
|
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? |
I'm not sure. I certainly don't understand the code well enough to write a patch. @SkySkimmer says:
Or alternatively if coq/coq#17565 is granted then users can just |
|
Or we can alter QuickChick to make it compatible with here. |
liyishuai
added a commit
to QuickChick/QuickChick
that referenced
this pull request
Jan 4, 2024
liyishuai
added a commit
to QuickChick/QuickChick
that referenced
this pull request
Jan 5, 2024
liyishuai
approved these changes
Jan 5, 2024
|
Fails QuickChick unit test on Coq dev: https://github.com/QuickChick/QuickChick/blob/235f6f2156b06239d10e971b7f229f18b73fb67c/test/plugin/plugin.v#L51
|
@JasonGross any idea regarding the new (Universe?) issue with QuickChick? |
|
Can we get coqbot to minimize it for us? Something like 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 |
I see on CI. What should I pass |
|
I might have changed the test suite in coq/opam#2897. Locating this problem on my side. |
|
@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) 🌟 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
|
I don't think so. @Lysxia any ideas? |
|
Slightly more minimal example. Removing 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). |
|
Reported upstream as QuickChick/QuickChick#352 |
|
I'm guessing the issue is that the |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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
DefaultOptionsor something with#[export] Set ...for all the options, that isImported by the relevant files?