# 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.16.1 Formal proof management system
dune 3.12.1 Fast, portable, and opinionated build system
ocaml 4.13.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.13.1 Official release 4.13.1
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.6 A library manager for OCaml
zarith 1.13 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.16.1Dry 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.16.1opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-vst-iris.2.11.1 coq.8.16.1# 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.16.1 Formal proof management system
coq-compcert 3.11 The CompCert C compiler (64 bit)
coq-flocq 4.1.3 A formalization of floating-point arithmetic for the Coq system
coq-iris 4.1.0 A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs
coq-menhirlib 20230608 A support library for verified Coq parsers produced by Menhir
coq-stdpp 1.9.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.12.1 Fast, portable, and opinionated build system
menhir 20230608 An LR(1) parser generator
menhirLib 20230608 Runtime support library for parsers generated by Menhir
menhirSdk 20230608 Compile-time library for auxiliary tools related to Menhir
ocaml 4.13.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.13.1 Official release 4.13.1
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.6 A library manager for OCaml
zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers
[NOTE] Package coq is already installed (current version is 8.16.1).
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.13.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.13.1/lib/coq/user-contrib/compcert
- ZLIST=platform
- BITSIZE=64
- ARCH=x86
- INSTALLDIR=/home/bench/.opam/ocaml-base-compiler.4.13.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.13.1/lib/coq/user-contrib/compcert
- ZLIST=platform
- BITSIZE=64
- ARCH=x86
- INSTALLDIR=/home/bench/.opam/ocaml-base-compiler.4.13.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 46, characters 12-37:
- Error: In environment
- n, P : nat
- Q, y : mpred
- Unable to unify "∀ a : ?A, ?M15012 a → ?M15013 a" with
- "approx (S n) Q = approx (S n) y".
-
- COQC concurrency/ghostsI.v
- File "./concurrency/ghostsI.v", line 4, characters 0-28:
- Error: Cannot find a physical path bound to logical path VST.veric.bi.
-
- COQC concurrency/invariants.v
- File "./concurrency/invariants.v", line 7, characters 0-39:
- Error: Cannot find a physical path bound to logical path
- VST.concurrency.ghostsI.
-
- COQC concurrency/fupd.v
- File "./concurrency/fupd.v", line 4, characters 0-84:
- Error: Cannot find a physical path bound to logical path
- invariants with prefix VST.concurrency.
-
- COQC atomics/general_atomics.v
- File "./atomics/general_atomics.v", line 3, characters 0-28:
- Error: Cannot find a physical path bound to logical path VST.veric.bi.
-
- COQC atomics/SC_atomics.v
- File "./atomics/SC_atomics.v", line 6, characters 0-36:
- Error: Cannot find a physical path bound to logical path
- VST.concurrency.fupd.
-
- COQC atomics/verif_lock_atomic.v
- File "./atomics/verif_lock_atomic.v", line 9, characters 0-38:
- Error: Cannot find a physical path bound to logical path
- 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 0-38:
- Error: Cannot find a physical path bound to logical path
- VST.atomics.SC_atomics.
-
- COQC progs64/verif_incr_atomic.v
- File "./progs64/verif_incr_atomic.v", line 2, characters 0-45:
- Error: Cannot find a physical path bound to logical path
- 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.10 | linux/x86_64 | ocaml-base-compiler.4.13.1 | file:///home/bench/run/opam-coq-archive/released
# path ~/.opam/ocaml-base-compiler.4.13.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-14826-d2c37b.env
# output-file ~/.opam/log/coq-vst-iris-14826-d2c37b.out
### output ###
# [...]
# COQC atomics/hashtable.v
# COQC atomics/verif_hashtable_atomic.v
# File "./atomics/verif_hashtable_atomic.v", line 3, characters 0-38:
# Error: Cannot find a physical path bound to logical path
# VST.atomics.SC_atomics.
#
# COQC progs64/verif_incr_atomic.v
# File "./progs64/verif_incr_atomic.v", line 2, characters 0-45:
# Error: Cannot find a physical path bound to logical path
# 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.16.1' failed.
No files were installed.
true