(2021-10-27 02:59:51 UTC)
# 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 3 Virtual package relying on a GMP lib system installation coq dev Formal proof management system dune 2.9.1 Fast, portable, and opinionated build system ocaml 4.12.0 The OCaml compiler (virtual package) ocaml-base-compiler 4.12.0 Official release 4.12.0 ocaml-config 2 OCaml Switch Configuration ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled ocamlfind 1.9.1 A library manager for OCaml zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers # opam file: opam-version: "2.0" authors: ["Andrew W. Appel" "Lennart Beringer" "Sandrine Blazy" "Qinxiang Cao" "Santiago Cuellar" "Robert Dockins" "Josiah Dodds" "Nick Giannarakis" "Samuel Gruetter" "Aquinas Hobor" "Jean-Marie Madiot" ] 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 "IGNORECOQVERSION=true" "-j%{jobs}%" "msl" "sepcomp" "veric" "floyd"] ] run-test: [make "IGNORECOQVERSION=true" "-j%{jobs}%" "progs" "sha-hmac" "mailbox" "VSUpile"] install: [ ["mkdir" "-p" "%{lib}%/coq/user-contrib/VST"] ["cp" "-r" "msl" "%{lib}%/coq/user-contrib/VST/"] ["cp" "-r" "veric" "%{lib}%/coq/user-contrib/VST/"] ["cp" "-r" "floyd" "%{lib}%/coq/user-contrib/VST/"] ["cp" "-r" "sepcomp" "%{lib}%/coq/user-contrib/VST/"] ] remove: [ ["rm" "-fr" "%{lib}%/coq/user-contrib/VST"] ] depends: [ "ocaml" "coq" {>= "8.11.0"} "coq-compcert" {>= "3.7~"} ] synopsis: "Verified Software Toolchain" description: "The software toolchain includes static analyzers to check assertions about your program; optimizing compilers to translate your program to machine language; operating systems and libraries to supply context for your program. The Verified Software Toolchain project assures with machine-checked proofs that the assertions claimed at the top of the toolchain really hold in the machine-language program, running in the operating-system context." flags: light-uninstall url { src: "git+https://github.com/PrincetonUniversity/VST.git#master" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-vst.dev coq.dev
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
true
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-vst.dev coq.dev
# 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 3 Virtual package relying on a GMP lib system installation coq dev Formal proof management system dune 2.9.1 Fast, portable, and opinionated build system ocaml 4.12.0 The OCaml compiler (virtual package) ocaml-base-compiler 4.12.0 Official release 4.12.0 ocaml-config 2 OCaml Switch Configuration ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled ocamlfind 1.9.1 A library manager for OCaml zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers The following actions will be performed: - install menhirSdk dev - install coq-flocq dev - install menhirLib dev - install coq-menhirlib dev - install menhir dev - install coq-compcert dev ===== 6 to install ===== <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> [coq-flocq.dev] synchronised from git+https://gitlab.inria.fr/flocq/flocq.git#master [coq-compcert.dev] synchronised from git+https://github.com/AbsInt/CompCert.git [coq-menhirlib.dev] synchronised from git+https://gitlab.inria.fr/fpottier/menhir.git#master [menhir.dev] synchronised from git+https://gitlab.inria.fr/fpottier/menhir.git#master [menhirSdk.dev] synchronised from git+https://gitlab.inria.fr/fpottier/menhir.git#master [menhirLib.dev] synchronised from git+https://gitlab.inria.fr/fpottier/menhir.git#master <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> -> installed menhirSdk.dev -> installed coq-menhirlib.dev -> installed menhirLib.dev -> installed menhir.dev -> installed coq-flocq.dev [ERROR] The compilation of coq-compcert failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j4". #=== ERROR while compiling coq-compcert.dev ===================================# # context 2.0.8 | linux/x86_64 | ocaml-base-compiler.4.12.0 | file:///home/bench/run/opam-coq-archive/extra-dev # path ~/.opam/ocaml-base-compiler.4.12.0/.opam-switch/build/coq-compcert.dev # command ~/.opam/opam-init/hooks/sandbox.sh build make -j4 # exit-code 2 # env-file ~/.opam/log/coq-compcert-28140-40fffe.env # output-file ~/.opam/log/coq-compcert-28140-40fffe.out ### output ### # [...] # COQC lib/Coqlib.v # COQC x86_64/Archi.v # COQC lib/IEEE754_extra.v # COQC driver/Compopts.v # COQC cparser/Cabs.v # File "./lib/IEEE754_extra.v", line 35, characters 21-22: # Error: The reference Z was not found in the current environment. # # make[1]: *** [Makefile:262: lib/IEEE754_extra.vo] Error 1 # make[1]: *** Waiting for unfinished jobs.... # make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.12.0/.opam-switch/build/coq-compcert.dev' # make: *** [Makefile:191: all] Error 2 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-compcert dev +- +- The following changes have been performed | - install coq-flocq dev | - install coq-menhirlib dev | - install menhir dev | - install menhirLib dev | - install menhirSdk dev +- # Run eval $(opam env) to update the current shell environment The former state can be restored with: opam switch import "/home/bench/.opam/ocaml-base-compiler.4.12.0/.opam-switch/backup/state-20211026045746.export"
true
No files were installed.
true