Please update vst to 2.4 version

[p3rsik]

The latest version of vst here is 2.2 which requires compcert.3.3 and coq.8.8.0. The latest stable version in dev-repo is vst.2.4, requiring compcert.3.5 and coq.8.9.1. Could you please update opam package for vst.

@PrincetonUniversity

[vzaliva]

It indeed requires Coq-8.8.

$ opam install coq-vst                                                              
The following dependencies couldn't be met:
  - coq-vst → coq-compcert = 3.3.0 → coq < 8.8.1
      not available because the package is pinned to version 8.9.1

[p3rsik]

I also tried to install coq-vst.dev version and it failed with this error:

[ERROR] The compilation of coq-vst failed at "/home/p3rsik/.opam/opam-init/hooks/sandbox.sh build make IGNORECOQVERSION=true -j3
COMPCERT=/home/p3rsik/.opam/default/lib/coq/user-contrib/compcert floyd progs".

#=== ERROR while compiling coq-vst.dev ========================================#
# context 2.0.4 | linux/x86_64 | ocaml-system.4.05.0 | https://coq.inria.fr/opam/extra-dev
#2019-10-16 10:50
# path ~/.opam/default/.opam-switch/build/coq-vst.dev
# command ~/.opam/opam-init/hooks/sandbox.sh build make IGNORECOQVERSION=true -j3 COMPCERT=/home/p3rsik/.opam/default/lib/coq/user-contrib/compcert floyd progs
# exit-code 2
# env-file ~/.opam/log/coq-vst-10871-74316f.env
# output-file ~/.opam/log/coq-vst-10871-74316f.out
### output ###
# [...]
# COQC msl/functors.v
# COQC msl/sig_isomorphism.v
# COQC veric/val_lemmas.v
# COQC floyd/sublist.v
# COQC veric/coqlib4.v
# File "./veric/val_lemmas.v", line 156, characters 8-27:
# Error: The reference Zbits.Ztestbit_succ was not found in the current
# environment.
#
# Makefile:423: recipe for target 'veric/val_lemmas.vo' failed
# make: *** [veric/val_lemmas.vo] Error 1
# make: *** Waiting for unfinished jobs...

This is opam list after the installation fail:

$ opam list
# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-num base Num library distributed with the OCaml compiler
base-threads base
base-unix base
camlp5 7.10 Preprocessor-pretty-printer of OCaml
conf-m4 1 Virtual package relying on m4
coq 8.9.1 pinned to version 8.9.1
coq-compcert 3.5 The CompCert C compiler
menhir 20181113 An LR(1) parser generator
num 0 The Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.05.0 The OCaml compiler (virtual package)
ocaml-config 1 OCaml Switch Configuration
ocaml-system 4.05.0 The OCaml compiler (system version, from outside of opam)
ocamlbuild 0.14.0 OCamlbuild is a build system with builtin rules to easily build most OCaml projects.
ocamlfind 1.8.1 A library manager for OCaml

[vzaliva]

Now CompCert 8.6 is available in OPAM opening a way to upgrade VST

[palmskog]

@MSoegtropIMC any update on the enhanced/modified VST and CompCert packages? Even if they are not fully ready yet, feel free to open a PR (e.g., a draft PR) in the Coq OPAM archive and I'd be happy to help out with refining the packages.

[MSoegtropIMC]

I have something working for VST 2.4 and 2.5 (not 2.3) and also the patched compcert variants delivered with Coq 8.10 and 8.11. But it doesn't allow to choose the specific compcert platform. Should I upload this as is already?

[palmskog]

I think those working packages would already be a big improvement on the situation now (no recent VST at all). We can always look into the platform configuration issue after we have the fixed platform stuff working.

[MSoegtropIMC]

OK, I will upload it as is then - it might be Wednesday, though.

[liyishuai]

What's the status of this issue?

[MSoegtropIMC]

Should come soon. The new version by default uses a platform supplied CompCert and Flocq, which had a few dependencies in opam and also required a rewrite of the VST makefile. I am almost there.