Embedding does not work with Coq 8.11
jakobbotsch opened this issue · 24 comments
The embedding does not compile with Coq 8.11 (using the new MetaCoq package):
File "./embedding/theories/Misc.v", line 106, characters 23-36:
Error: The reference utils.rev_ind was not found in the current environment.
We should maybe discuss which versions of Coq we want to support for full ConCert, i.e.
do we want the embedding to support multiple versions of Coq or not. Pros are that it
makes working with the project easier for other people, but a con is that it takes some more
effort.
I tried to update it, but there were a bunch of refactoring changes to MetaCoq so seems like this will take some work. I will leave it to you @annenkov.
Thanks @jakobbotsch for the info! I'll try to fix it. The error you see is definitely due to changes in MetaCoq. You're right, we need to figure out which versions to support.
I think we should just update to 8.11 and stick to that. The refactoring changes will make it hard to support mulltiple versions without having multiple versions of ConCert, which is not worth it in terms of the benefits.
Yes, I agree. Let's stick to 8.11. Some issues with custom entries have been fixed in 8.11, so I probably can remove some hacks from the notations.
Hopefully this will also fix some weirdQuickChick issues that magically appeared on my fork when I merged the lastest commits from this upstream...
@mikkelmilo Note that the execution part of ConCert supports Coq 8.9, 8.10 and 8.11, so you can just use any of those. This issue is only for the embedding part which I don't think you are using.
@jakobbotsch yeah it should not be the embedding part which causes it, but it is essentially after the merge of this commit that QuickChick suddenly gives errors in the extracted code, so maybe... I'm looking into it, but I'm pretty clueless as to the reason at the moment.
@jakobbotsch which version of std++ you have used to compile with Coq 8.11? If I run opam install coq-stdpp, it tries to install coq-stdpp.1.2.1 and this version requires Coq < 8.11.
Ok, I ended up installing the dev version.
@jakobbotsch I think we should add coq-bignums to dependencies in the readme.
@spitters I just wanted a confirmation from @jakobbotsch that this is indeed the case, because I had some issues with installing packages today, so I am not sure that the problem wasn't caused by my setup.
@jakobbotsch I think we should add coq-bignums to dependencies in the readme.
I have already done so.
@jakobbotsch which version of std++ you have used to compile with Coq 8.11?
I just used opam install coq-stdpp, but I have the iris repo added to opam.
@jakobbotsch could you check the coq-stdpp version please (if you still have the setup)?
This is the result of my opam list:
# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
conf-m4 1 Virtual package relying on m4
coq 8.11.0 Formal proof management system
coq-bignums 8.11.0 Bignums, the Coq library of arbitrary large numbers
coq-equations 1.2.1+8.11 A function definition package for Coq
coq-metacoq 1.0~alpha2+8.11 A meta-programming framework for Coq
coq-metacoq-checker 1.0~alpha2+8.11 Specification of Coq's type theory and reference checker implementation
coq-metacoq-erasure 1.0~alpha2+8.11 Implementation and verification of an erasure procedure for Coq
coq-metacoq-pcuic 1.0~alpha2+8.11 A type system equivalent to Coq's and its metatheory
coq-metacoq-safechecker 1.0~alpha2+8.11 Implementation and verification of safe conversion and typechecking algorithms for Coq
coq-metacoq-template 1.0~alpha2+8.11 A quoting and unquoting library for Coq in Coq
coq-metacoq-translations 1.0~alpha2+8.11 Translations built on top of MetaCoq
coq-stdpp dev.2020-03-13.1.215f99da This project contains an extended "Standard Library" for Coq called coq-std++
num 1.3 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.07.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.07.1 Official release 4.07.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.8.1 A library manager for OCaml
Thanks, you also have a dev version. I think I should create an issue about stdpp for coq 8.11.
Note that our readme already says to add the Iris repo so the dev versions can be installed (although I guess that's probably not necessary for 1.2.1). I think we should just get rid of the version part from the readme (i.e. change opam install coq-stdpp.1.2.1 to opam install coq-stdpp).
I've created a coq.8.11 branch that compiles. We can merge it into master once we decide that it is fine with everyone.
Looks good, let me try to fix the CI image.
I think we should just update to 8.11 and stick to that. The refactoring changes will make it hard to support mulltiple versions without having multiple versions of ConCert, which is not worth it in terms of the benefits.
FYI QuickChick only supports up to 8.10. They have an open issue for 8.11 support, though. So if we want my tests to be merged we either have to wait for the QC maintainers to close this issue, or support 8.10 ourselves (the 8.9.1 version currently doesn't work on my fork because of a bug with stdpp and QC).
I tested out the 8.11 branch, but with coq 8.10 installed and it works fine on my end.
So, our coq.8.11 branch works fine with QuikChick under Coq 8.10, right @mikkelmilo? If so, maybe we should merge coq.8.11 into master then and use it (since it seems compatible with both 8.10 and 8.11)
Yes, seems like a good solution. There's also a good chance QC will get 8.11 support before my work is ready to be merged.
The branch is already there, and it looks like they'll push to opam soon.