-
Notifications
You must be signed in to change notification settings - Fork 79
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
MetaCoq is incompatible with QuickChick (universe inconsistency) #580
Comments
You can probably minimize this with the bug minimizer |
This kind of universe inconsistency is usually due to a template-polymorphic inductive type being partially applied somewhere. Those are not easy to find though. |
Does coqbot watch this repo?
|
I guess not. Trying at coq-community/run-coq-bug-minimizer#2 (comment) |
Can metacoq do a release so that the opam package is compatible with 8.14.0? |
We're working on it |
This is also the incompatibility with Iris that we run into at Bedrock with @gmalecha and others; we thought it might relate to https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80 but I don't have strong evidence it's related. In our case, we just found out that we can skip importing Minimized example against
Some partial minimizations appear in https://gist.github.com/Blaisorblade/aae837cb9b39e7693d3f2037960b0f80, but dunno if it's helpful. |
On the latest commit of the
|
@gmalecha suggested dropping Other users can try replacing requires of From MetaCoq.Template Require Import
utils.MCUtils (* Utility functions *)
monad_utils (* Monadic notations *)
uGraph (* The graph of universes *)
BasicAst (* The basic AST structures *)
Ast (* The term AST *)
AstUtils (* Utilities on the AST *)
Induction (* Induction *)
LiftSubst (* Lifting and substitution for terms *)
UnivSubst (* Substitution of universe instances *)
(* Typing *) (* Typing judgment *)
TemplateMonad (* The TemplateMonad *)
Loader (* The plugin *). |
I assume the partial application in QuickChick is from coq-ext-lib.
There might be more list monads in there. |
If indeed this is the issue, the solution is to eta-expand |
FWIW:
|
This is done to avoid universe inconsistencies related to: MetaCoq/metacoq#580.
With the following:
I get the error:
Strangely, pasting the line
From QuickChick Require Import Sets.
on top of file https://github.com/MetaCoq/metacoq/blob/coq-8.13/template-coq/theories/TermEquality.v raises the error:Tested with Coq 8.13.2, QuickChick 1.5.0 and MetaCoq 1.0~beta2+8.13 from opam
This is related to smtcoq/sniper#4 and QuickChick/QuickChick#232.
The text was updated successfully, but these errors were encountered: