# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq 8.14.0 Formal proof management system
dune 3.6.2 Fast, portable, and opinionated build system
ocaml 4.12.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.12.1 Official release 4.12.1
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.5 A library manager for OCaml
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
synopsis: "Verified Software Toolchain with Iris"
description: "VST with support for Iris tactics, definitions, and notation. Especially useful for reasoning about fine-grained concurrent programs and logical atomicity."
authors: [
"William Mansky"
"Shengyi Wang"
]
maintainer: "VST team"
homepage: "http://vst.cs.princeton.edu/"
dev-repo: "git+https://github.com/PrincetonUniversity/VST.git"
bug-reports: "https://github.com/PrincetonUniversity/VST/issues"
license: "https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE"
build: [
[make "-j%{jobs}%" "build-iris" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=64"]
]
install: [
[make "install-iris" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=64"]
]
run-test: [
[make "-j%{jobs}%" "atomics" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=64"]
]
depends: [
"coq-vst" { = version }
"coq-iris" {>= "4.0.0"}
]
tags: [
"category:Computer Science/Semantics and Compilation/Semantics"
"keyword:C"
"logpath:VST"
"date:2023-01-24"
]
url {
src: "https://github.com/PrincetonUniversity/VST/archive/refs/tags/v2.11.1.tar.gz"
checksum: "sha512=9d66a1a0f428199110d89a8b4e90d50ad9b6448c92b5ad0859a1bcae9bf1153ea016b5af1ab9f4dc441b5af307968445f4b134cdb80593a6e9a974be94cc5730"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-vst-iris.2.11.1 coq.8.14.0Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-vst-iris.2.11.1 coq.8.14.0opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-vst-iris.2.11.1 coq.8.14.0# 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-gmp 4 Virtual package relying on a GMP lib system installation
coq 8.14.0 Formal proof management system
coq-compcert 3.11 The CompCert C compiler (64 bit)
coq-flocq 4.1.0 A formalization of floating-point arithmetic for the Coq system
coq-iris 4.0.0 A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs
coq-menhirlib 20220210 A support library for verified Coq parsers produced by Menhir
coq-stdpp 1.8.0 An extended "Standard Library" for Coq
coq-vst 2.11.1 Verified Software Toolchain
coq-vst-zlist 2.11 A list library indexed by Z type, with a powerful automatic solver
dune 3.6.2 Fast, portable, and opinionated build system
menhir 20220210 An LR(1) parser generator
menhirLib 20220210 Runtime support library for parsers generated by Menhir
menhirSdk 20220210 Compile-time library for auxiliary tools related to Menhir
ocaml 4.12.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.12.1 Official release 4.12.1
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.5 A library manager for OCaml
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
[NOTE] Package coq is already installed (current version is 8.14.0).
The following actions will be performed:
- install coq-vst-iris 2.11.1
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[coq-vst-iris.2.11.1] found in cache
Processing 1/1:
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/2: [coq-vst-iris: make build-iris]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" "build-iris" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=64" (CWD=/home/bench/.opam/ocaml-base-compiler.4.12.1/.opam-switch/build/coq-vst-iris.2.11.1)
- ===== CONFIGURATION SUMMARY =====
- COMPCERT=platform
- COMPCERT_SRC_DIR=__NONE__
- COMPCERT_INST_DIR=/home/bench/.opam/ocaml-base-compiler.4.12.1/lib/coq/user-contrib/compcert
- ZLIST=platform
- BITSIZE=64
- ARCH=x86
- INSTALLDIR=/home/bench/.opam/ocaml-base-compiler.4.12.1/lib/coq/user-contrib/VST
- ===== DERIVED CONFIGURATION =====
- COMPCERT_INFO_PATH_REF=compcert
- COMPCERT_EXPLICIT_PATH=false
- COMPCERT_BUILD_FROM_SRC=false
- COMPCERT_NEW=false
- COQFLAGS= -Q msl VST.msl -Q sepcomp VST.sepcomp -Q veric VST.veric -Q floyd VST.floyd -Q progs64 VST.progs64 -Q concurrency VST.concurrency -Q atomics VST.atomics -Q wand_demo wand_demo -Q sha sha -Q hmacfcf hmacfcf -Q tweetnacl20140427 tweetnacl20140427 -Q hmacdrbg hmacdrbg -Q aes aes -Q mailbox mailbox
- COMPCERT_R_FLAGS=
- =================================
- coqdep ... >.depend
- # DEPENDENCIES DEFAULT
- coqdep -vos -Q msl VST.msl -Q sepcomp VST.sepcomp -Q veric VST.veric -Q floyd VST.floyd -Q progs64 VST.progs64 -Q concurrency VST.concurrency -Q atomics VST.atomics -Q wand_demo wand_demo -Q sha sha -Q hmacfcf hmacfcf -Q tweetnacl20140427 tweetnacl20140427 -Q hmacdrbg hmacdrbg -Q aes aes -Q mailbox mailbox 2>&1 >.depend `find msl sepcomp veric floyd progs64 concurrency atomics wand_demo sha hmacfcf tweetnacl20140427 hmacdrbg aes mailbox -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true
- wc .depend
- 2478 22868 623634 .depend
- ===== CONFIGURATION SUMMARY =====
- COMPCERT=platform
- COMPCERT_SRC_DIR=__NONE__
- COMPCERT_INST_DIR=/home/bench/.opam/ocaml-base-compiler.4.12.1/lib/coq/user-contrib/compcert
- ZLIST=platform
- BITSIZE=64
- ARCH=x86
- INSTALLDIR=/home/bench/.opam/ocaml-base-compiler.4.12.1/lib/coq/user-contrib/VST
- ===== DERIVED CONFIGURATION =====
- COMPCERT_INFO_PATH_REF=compcert
- COMPCERT_EXPLICIT_PATH=false
- COMPCERT_BUILD_FROM_SRC=false
- COMPCERT_NEW=false
- COQFLAGS= -Q msl VST.msl -Q sepcomp VST.sepcomp -Q veric VST.veric -Q floyd VST.floyd -Q progs64 VST.progs64 -Q concurrency VST.concurrency -Q atomics VST.atomics -Q wand_demo wand_demo -Q sha sha -Q hmacfcf hmacfcf -Q tweetnacl20140427 tweetnacl20140427 -Q hmacdrbg hmacdrbg -Q aes aes -Q mailbox mailbox
- COMPCERT_R_FLAGS=
- =================================
- echo -Q msl VST.msl -Q sepcomp VST.sepcomp -Q veric VST.veric -Q floyd VST.floyd -Q progs64 VST.progs64 -Q concurrency VST.concurrency -Q atomics VST.atomics -Q wand_demo wand_demo -Q sha sha -Q hmacfcf hmacfcf -Q tweetnacl20140427 tweetnacl20140427 -Q hmacdrbg hmacdrbg -Q aes aes -Q mailbox mailbox > _CoqProject
- util/coqflags > _CoqProject-export
- coqc -Q msl VST.msl -Q sepcomp VST.sepcomp -Q veric VST.veric -Q floyd VST.floyd -Q progs64 VST.progs64 -Q concurrency VST.concurrency -Q atomics VST.atomics -Q wand_demo wand_demo -Q sha sha -Q hmacfcf hmacfcf -Q tweetnacl20140427 tweetnacl20140427 -Q hmacdrbg hmacdrbg -Q aes aes -Q mailbox mailbox progs64/incr.v
- for f in atomics/SC_atomics.c veric/bi.v concurrency/ghostsI.v concurrency/invariants.v concurrency/fupd.v atomics/general_atomics.v atomics/SC_atomics.v atomics/verif_lock_atomic.v atomics/hashtable_atomic.v atomics/hashtable.v atomics/verif_hashtable_atomic.v progs64/verif_incr_atomic.v; do if [ "${f##*.}" = "v" ]; then echo COQC $f; coqc -Q msl VST.msl -Q sepcomp VST.sepcomp -Q veric VST.veric -Q floyd VST.floyd -Q progs64 VST.progs64 -Q concurrency VST.concurrency -Q atomics VST.atomics -Q wand_demo wand_demo -Q sha sha -Q hmacfcf hmacfcf -Q tweetnacl20140427 tweetnacl20140427 -Q hmacdrbg hmacdrbg -Q aes aes -Q mailbox mailbox $f; fi; done
- COQC veric/bi.v
- File "./veric/bi.v", line 18, characters 0-61:
- Warning: Notation "|==> _" was already defined with a different format.
- [notation-incompatible-format,parsing]
- File "./veric/bi.v", line 18, characters 0-61:
- Warning: Notation "|={ _ , _ }=> _" was already defined with a different
- format. [notation-incompatible-format,parsing]
- File "./veric/bi.v", line 18, characters 0-61:
- Warning: Notation "|={ _ }=> _" was already defined with a different format.
- [notation-incompatible-format,parsing]
- COQC concurrency/ghostsI.v
- File "./concurrency/ghostsI.v", line 287, characters 0-61:
- Error:
- Unable to satisfy the following constraints:
- In environment:
- K : Type
- EqDecision0 : EqDecision K
- H : Countable K
- A : Ghost
- ord : G → G → Prop
- A_order : PCM_order ord
-
- ?P : "Ghost"
-
- ?H : "(∀ A0 : Type, Lookup ?K A0 (?M A0))%type"
- [K EqDecision0 H A ord A_order] [] |- ?M G == let
- (G, valid, Join_G, _, _,
- _) :=
- ?X130@{
- __:=K; __:=EqDecision0;
- __:=H; __:=A; __:=ord;
- __:=A_order} in
- G
- [K EqDecision0 H A ord A_order] [y] |- ?M G == let
- (G, valid, Join_G, _, _,
- _) :=
- ?X130@{
- __:=K; __:=EqDecision0;
- __:=H; __:=A; __:=ord;
- __:=A_order} in
- G
-
- COQC concurrency/invariants.v
- File "./concurrency/invariants.v", line 7, characters 15-38:
- Error: Unable to locate library VST.concurrency.ghostsI.
-
- COQC concurrency/fupd.v
- File "./concurrency/fupd.v", line 4, characters 51-61:
- Error: Unable to locate library invariants with prefix VST.concurrency.
-
- COQC atomics/general_atomics.v
- File "./atomics/general_atomics.v", line 4, characters 51-61:
- Error: Unable to locate library invariants with prefix VST.concurrency.
-
- COQC atomics/SC_atomics.v
- File "./atomics/SC_atomics.v", line 6, characters 15-35:
- Error: Unable to locate library VST.concurrency.fupd.
-
- COQC atomics/verif_lock_atomic.v
- File "./atomics/verif_lock_atomic.v", line 9, characters 15-37:
- Error: Unable to locate library VST.atomics.SC_atomics.
-
- COQC atomics/hashtable_atomic.v
- COQC atomics/hashtable.v
- COQC atomics/verif_hashtable_atomic.v
- File "./atomics/verif_hashtable_atomic.v", line 3, characters 15-37:
- Error: Unable to locate library VST.atomics.SC_atomics.
-
- COQC progs64/verif_incr_atomic.v
- File "./progs64/verif_incr_atomic.v", line 2, characters 15-44:
- Error: Unable to locate library VST.atomics.verif_lock_atomic.
-
- make: *** [Makefile:796: build-iris] Error 1
[ERROR] The compilation of coq-vst-iris failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j4 build-iris IGNORECOQVERSION=true ZLIST=platform BITSIZE=64".
#=== ERROR while compiling coq-vst-iris.2.11.1 ================================#
# context 2.0.8 | linux/x86_64 | ocaml-base-compiler.4.12.1 | file:///home/bench/run/opam-coq-archive/released
# path ~/.opam/ocaml-base-compiler.4.12.1/.opam-switch/build/coq-vst-iris.2.11.1
# command ~/.opam/opam-init/hooks/sandbox.sh build make -j4 build-iris IGNORECOQVERSION=true ZLIST=platform BITSIZE=64
# exit-code 2
# env-file ~/.opam/log/coq-vst-iris-31778-d2c37b.env
# output-file ~/.opam/log/coq-vst-iris-31778-d2c37b.out
### output ###
# Error: Unable to locate library VST.atomics.SC_atomics.
# [...]
# COQC atomics/hashtable_atomic.v
# COQC atomics/hashtable.v
# COQC atomics/verif_hashtable_atomic.v
# File "./atomics/verif_hashtable_atomic.v", line 3, characters 15-37:
# Error: Unable to locate library VST.atomics.SC_atomics.
#
# COQC progs64/verif_incr_atomic.v
# File "./progs64/verif_incr_atomic.v", line 2, characters 15-44:
# Error: Unable to locate library VST.atomics.verif_lock_atomic.
#
# make: *** [Makefile:796: build-iris] Error 1
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-vst-iris 2.11.1
+-
- No changes have been performed
# Run eval $(opam env) to update the current shell environment
'opam install -y -v coq-vst-iris.2.11.1 coq.8.14.0' failed.
No files were installed.
true