This result is black-listed as it is considered as too hard to reproduce / to solve. If you find a way to fix this package, please make a pull-request to github.com/coq/opam-coq-archive. The list of black-listed packages is in black_list.rb.
# 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.14 Preprocessor-pretty-printer of OCaml conf-findutils 1 Virtual package relying on findutils conf-perl 2 Virtual package relying on perl coq 8.7.1+1 Formal proof management system num 0 The Num library for arbitrary-precision integer and rational arithmetic ocaml 4.03.0 The OCaml compiler (virtual package) ocaml-base-compiler 4.03.0 Official 4.03.0 release ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.6 A library manager for OCaml # 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 "-j" "COMPCERT=%{lib}%/coq/user-contrib/compcert" "version.vo" "msl" "veric" "floyd"] ] install: [ ["mkdir" "%{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.7.0"} "coq-compcert" {= "3.3.0"} ] 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: "https://github.com/PrincetonUniversity/VST/archive/v2.2.tar.gz" checksum: "md5=deb1d112fa078c380ed93f0f7e929481" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-vst.2.2 coq.8.7.1+1
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.2.2 coq.8.7.1+1
# 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.14 Preprocessor-pretty-printer of OCaml conf-findutils 1 Virtual package relying on findutils conf-perl 2 Virtual package relying on perl coq 8.7.1+1 Formal proof management system num 0 The Num library for arbitrary-precision integer and rational arithmetic ocaml 4.03.0 The OCaml compiler (virtual package) ocaml-base-compiler 4.03.0 Official 4.03.0 release ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.6 A library manager for OCaml The following actions will be performed: - install ocamlbuild 0.14.2 - install menhir 20180528 - install coq-compcert 3.3.0 ===== 3 to install ===== <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> [menhir.20180528] downloaded from cache at https://opam.ocaml.org/cache [ocamlbuild.0.14.2] downloaded from cache at https://opam.ocaml.org/cache [coq-compcert.3.3.0] downloaded from https://github.com/AbsInt/CompCert/archive/v3.3.tar.gz <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> -> installed ocamlbuild.0.14.2 -> installed menhir.20180528 [ERROR] The compilation of coq-compcert failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j4". #=== ERROR while compiling coq-compcert.3.3.0 =================================# # context 2.0.5 | linux/x86_64 | ocaml-base-compiler.4.03.0 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.03.0/.opam-switch/build/coq-compcert.3.3.0 # command ~/.opam/opam-init/hooks/sandbox.sh build make -j4 # exit-code 2 # env-file ~/.opam/log/coq-compcert-26936-2f17b7.env # output-file ~/.opam/log/coq-compcert-26936-2f17b7.out ### output ### # [...] # OCAMLC extraction/RTL.mli # OCAMLC extraction/Cop.mli # OCAMLC debug/Debug.mli # File "debug/Debug.mli", line 1: # Error: Corrupted compiled interface # lib/Camlcoq.cmi # make[2]: *** [Makefile.extr:116: debug/Debug.cmi] Error 2 # make[2]: *** Waiting for unfinished jobs.... # make[2]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.03.0/.opam-switch/build/coq-compcert.3.3.0' # make[1]: *** [Makefile:164: ccomp] Error 2 # make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.03.0/.opam-switch/build/coq-compcert.3.3.0' # make: *** [Makefile:139: all] Error 2 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-compcert 3.3.0 +- +- The following changes have been performed | - install menhir 20180528 | - install ocamlbuild 0.14.2 +- # 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.03.0/.opam-switch/backup/state-20231016110641.export"
true
No files were installed.
true