search

coq / opam

Archive for all Coq related OPAM packages organized in various repositories
https://coq.inria.fr/opam/www/
GNU Lesser General Public License v2.1
127 stars 166 forks source link

coq-vst Flocq version conflict #1511

Closed vzaliva closed 3 years ago

vzaliva commented 3 years ago

coq-vst package version 2.6 depends on both coq-compcert and coq-flocq packages. However coq-compcert includes its own copy of Flocq library which I think leads to the following error:

$ coqtop
Welcome to Coq 8.11.2 (December 2020)

Coq < From compcert Require Export Coqlib Integers Floats AST Ctypes Cop Clight.
Toplevel input, characters 0-74:
> From compcert Require Export Coqlib Integers Floats AST Ctypes Cop Clight.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error:
Compiled library compcert.lib.Integers (in file /home/lord/.opam/asn1/lib/coq/user-contrib/compcert/lib/Integers.vo) makes inconsistent assumptions over library Flocq.Core.Zaux
Zimmi48 commented 3 years ago

My understanding is that you should favor the platform versions of these libraries to have everything work smoothly together. I'm not sure they exist for 8.11 though (you will need to look by yourself). Otherwise, a very scripted way of installing them together is documented for 8.12 at https://github.com/coq/platform/tree/v8.12 and for 8.13 at https://github.com/coq/platform/tree/v8.13.

cc @MSoegtropIMC

MSoegtropIMC commented 3 years ago

@vzaliva : VST 2.6 depends on Compcert version 3.7~coq-platform or a variant of it. This variant does not include Flocq, but uses the opam supplied Flocq. I don't understand how you can install via opam VST 2.6 and CompCert 3.7 such that CompCert has its own Flocq. Can you please send a copy of opam list?

vzaliva commented 3 years ago 
$ 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-g++        1.0            Virtual package relying on the g++ compiler (for C++)
conf-m4         1              Virtual package relying on m4
coq             8.11.2         Formal proof management system
coq-compcert    dev            The CompCert C compiler.
coq-ext-lib     dev            a library of Coq definitions, theorems, and tactics
coq-flocq       3.3.1          A formalization of floating-point arithmetic for the C
coq-menhirlib   20201201       A support library for verified Coq parsers produced by
coq-struct-tact dev            Coq library of "structural tactics" and utility lemmas
dune            2.7.1          Fast, portable, and opinionated build system
menhir          20201201       An LR(1) parser generator
menhirLib       20201201       Runtime support library for parsers generated by Menhi
menhirSdk       20201201       Compile-time library for auxiliary tools related to Me
num             1.4            The legacy Num library for arbitrary-precision integer
ocaml           4.11.1         The OCaml compiler (virtual package)
ocaml-config    1              OCaml Switch Configuration
ocaml-variants  4.11.1+flambda Official release 4.11.1, with flambda activated
ocamlfind       1.8.1          A library manager for OCaml

I might added some confusion because of dev repository I have added.

MSoegtropIMC commented 3 years ago

OK, so you didn't install VST via opam. You should. Then opam will tell you that you need a different variant of the compcert package, namely coq-compcert.3.7~coq-platform. VST 2.6 either works with an opam supplied CompCert and Flocq or with the CompCert and Flocq delivered with VST but not with an external CompCert with integrated Flocq.

palmskog commented 3 years ago

One specific problem here is likely that the dev version of the CompCert package is incompatible with many parts of the released ecosystem. In fact, this dev package hasn't been updated since March 2020 (i.e., well before coq-vst.2.6) and seemingly uses the bundled Flocq, so intuitively all sorts of issues could be present.

MSoegtropIMC commented 3 years ago

I see, so someone needs to maintain the dev versions as well. Luckily most of the platform patches found its way into CompCert master, so that only a few configure flags are needed rather than a lot of patches.

I plan to point the master branch of the coq platform to the coq dev repo in the near future. Such issues should be found and fixed this way.

vzaliva commented 3 years ago

released opam repo now OK wrt. this issue.