# 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.15.1 Formal proof management system
dune 3.4.1 Fast, portable, and opinionated build system
ocaml 4.09.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.1 Official release 4.09.1
ocaml-config 1 OCaml Switch Configuration
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"
authors: "Xavier Leroy <xavier.leroy@inria.fr>"
maintainer: "Michael Soegtrop"
homepage: "http://compcert.inria.fr/"
dev-repo: "git+https://github.com/AbsInt/CompCert.git"
bug-reports: "https://github.com/AbsInt/CompCert/issues"
license: "INRIA Non-Commercial License Agreement"
build: [
["./configure"
"amd64-linux" {os = "linux" & arch = "x86_64"}
"amd64-macosx" {os = "macos" & arch = "x86_64"}
"arm64-linux" {os = "linux" & (arch = "arm64" | arch = "aarch64")}
"arm64-macosx" {os = "macos" & (arch = "arm64" | arch = "aarch64")}
"amd64-cygwin" {os = "cygwin"}
# This is for building a MinGW CompCert with cygwin host and cygwin target
"amd64-cygwin" {os = "win32" & os-distribution = "cygwinports"}
# This is for building a 64 bit CompCert on 32 bit MinGW with cygwin build host
"-toolprefix" {os = "win32" & os-distribution = "cygwinports" & arch = "i686"}
"x86_64-pc-cygwin-" {os = "win32" & os-distribution = "cygwinports" & arch = "i686"}
"-prefix" "%{prefix}%"
"-install-coqdev"
"-clightgen"
"-use-external-Flocq"
"-use-external-MenhirLib"
"-coqdevdir" "%{lib}%/coq/user-contrib/compcert"
"-ignore-coq-version"]
[make "-j%{jobs}%" {ocaml:version >= "4.06"}]
]
install: [
[make "install"]
]
depends: [
"coq" {>= "8.9.0" & < "8.17~"}
"menhir" {>= "20190626" }
"ocaml" {>= "4.05.0"}
"coq-flocq" {>= "4.1.0" & < "5~"}
"coq-menhirlib" {>= "20190626"}
]
synopsis: "The CompCert C compiler (64 bit)"
tags: [
"category:Computer Science/Semantics and Compilation/Compilation"
"category:Computer Science/Semantics and Compilation/Semantics"
"keyword:C"
"keyword:compiler"
"logpath:compcert"
"date:2022-06-27"
]
url {
src: "https://github.com/AbsInt/CompCert/archive/v3.11.tar.gz"
checksum: "sha512=02240113c7ad9155b76a99ea73c454a70cffa9efbaf92bbb70bc6d4901a2b1f36082713ea64b315b15384bca6a11459e6d2313701156bd16bdf2ad1ec10d67aa"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-compcert.3.11 coq.8.15.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-compcert.3.11 coq.8.15.1opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-compcert.3.11 coq.8.15.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.15.1 Formal proof management system coq-flocq 4.1.0 A formalization of floating-point arithmetic for the Coq system coq-menhirlib 20220210 A support library for verified Coq parsers produced by Menhir dune 3.4.1 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.09.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.09.1 Official release 4.09.1 ocaml-config 1 OCaml Switch Configuration 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.15.1). The following actions will be performed: - install coq-compcert 3.11 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/1: [coq-compcert.3.11: http] [coq-compcert.3.11] downloaded from https://github.com/AbsInt/CompCert/archive/v3.11.tar.gz Processing 1/1: <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/2: [coq-compcert: ./configure amd64-linux] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./configure" "amd64-linux" "-prefix" "/home/bench/.opam/ocaml-base-compiler.4.09.1" "-install-coqdev" "-clightgen" "-use-external-Flocq" "-use-external-MenhirLib" "-coqdevdir" "/home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/compcert" "-ignore-coq-version" (CWD=/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-compcert.3.11) - Testing assembler support for CFI directives... yes - Testing linker support for '-no-pie' / '-nopie' option... yes, '-no-pie' - Testing Coq... version 8.15.1 -- good! - Testing OCaml... version 4.09.1 -- good! - Testing OCaml native-code compiler... yes - Testing OCaml .opt compilers... yes - Testing Menhir... version 20220210 -- good! - Testing GNU make... version 4.2.1 (command 'make') -- good! - - CompCert configuration: - Target architecture........... x86 - Hardware model................ 64 - Application binary interface.. standard - Endianness.................... little - OS and development env........ linux - C compiler.................... gcc -m64 - C preprocessor................ gcc -std=c99 -m64 -U__GNUC__ -U__SIZEOF_INT128__ -E - Assembler..................... gcc -m64 -c - Assembler supports CFI........ true - Assembler for runtime lib..... gcc -m64 -c - Linker........................ gcc -m64 -no-pie - Archiver...................... ar rcs - Math library.................. -lm - Build command to use.......... make - Menhir API library............ /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/menhirLib - The Flocq library............. external - The MenhirLib library......... external - Binaries installed in......... /home/bench/.opam/ocaml-base-compiler.4.09.1/bin - Runtime library provided...... true - Library files installed in.... /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/compcert - Man pages installed in........ /home/bench/.opam/ocaml-base-compiler.4.09.1/share/man - Standard headers provided..... true - Standard headers installed in. /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/compcert/include - Coq development installed in.. /home/bench/.opam/ocaml-base-compiler.4.09.1/lib/coq/user-contrib/compcert Processing 1/2: [coq-compcert: make] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-compcert.3.11) - make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-compcert.3.11' - ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml - menhir --coq --coq-no-version-check cparser/Parser.vy - Preprocessing x86/ConstpropOp.vp - Preprocessing x86/SelectOp.vp - Preprocessing x86/SelectLong.vp - Preprocessing backend/SelectDiv.vp - Preprocessing backend/SplitLong.vp - Analyzing Coq dependencies - make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-compcert.3.11' - make proof - make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-compcert.3.11' - COQC lib/Axioms.v - COQC lib/Coqlib.v - COQC x86_64/Archi.v - COQC lib/IEEE754_extra.v - COQC driver/Compopts.v - COQC cparser/Cabs.v - COQC lib/Wfsimpl.v - COQC cparser/Parser.v - COQC lib/Intv.v - COQC lib/Maps.v - COQC lib/Zbits.v - COQC lib/Iteration.v - COQC lib/Parmov.v - COQC lib/UnionFind.v - COQC lib/Postorder.v - COQC lib/FSetAVLplus.v - COQC lib/IntvSets.v - COQC lib/Decidableplus.v - COQC lib/BoolEqual.v - COQC common/Errors.v - COQC lib/Integers.v - COQC lib/Lattice.v - COQC common/Unityping.v - COQC lib/Ordered.v - COQC lib/Floats.v - COQC lib/Heaps.v - COQC common/AST.v - COQC common/Linking.v - COQC common/Values.v - COQC cfrontend/Ctypes.v - COQC common/Memdata.v - COQC common/Switch.v - COQC backend/Registers.v - COQC export/Ctypesdefs.v - COQC common/Memtype.v - COQC common/Builtins0.v - COQC common/Memory.v - COQC x86/Builtins1.v - COQC common/Builtins.v - COQC common/Globalenvs.v - COQC cfrontend/Cop.v - COQC common/Events.v - COQC cfrontend/Csyntax.v - COQC cfrontend/Initializers.v - COQC export/Csyntaxdefs.v - COQC backend/Kildall.v - COQC common/Smallstep.v - COQC common/Separation.v - COQC x86/Op.v - COQC common/Behaviors.v - COQC backend/Cminor.v - COQC cfrontend/Csem.v - COQC cfrontend/Clight.v - COQC common/Determinism.v - COQC cfrontend/Ctyping.v - COQC cfrontend/Cstrategy.v - COQC cfrontend/Initializersproof.v - COQC cfrontend/SimplExpr.v - COQC cfrontend/ClightBigstep.v - COQC cfrontend/Csharpminor.v - COQC export/Clightdefs.v - COQC backend/Cminortyping.v - COQC cfrontend/SimplExprspec.v - COQC cfrontend/Cminorgen.v - COQC cfrontend/Cexec.v - COQC cfrontend/Cminorgenproof.v - COQC cfrontend/SimplExprproof.v - COQC backend/CminorSel.v - COQC x86/Machregs.v - COQC backend/RTL.v - COQC x86/SelectOp.v - COQC backend/Locations.v - COQC backend/RTLgen.v - COQC backend/Inlining.v - COQC backend/Renumber.v - COQC backend/Liveness.v - COQC backend/ValueDomain.v - COQC backend/CSEdomain.v - COQC backend/Unusedglob.v - COQC backend/RTLgenspec.v - COQC x86/Conventions1.v - COQC backend/Inliningspec.v - COQC backend/Renumberproof.v - Error: System error: "No space left on device" - - make[1]: *** [Makefile:259: backend/Renumberproof.vo] Error 1 - make[1]: *** Waiting for unfinished jobs.... - make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-compcert.3.11' - make: *** [Makefile:190: all] Error 2 [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.11 ==================================# # context 2.0.6 | linux/x86_64 | ocaml-base-compiler.4.09.1 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-compcert.3.11 # command ~/.opam/opam-init/hooks/sandbox.sh build make -j4 # exit-code 2 # env-file ~/.opam/log/coq-compcert-27231-2dea01.env # output-file ~/.opam/log/coq-compcert-27231-2dea01.out ### output ### # [...] # COQC backend/CSEdomain.v # COQC backend/Unusedglob.v # COQC backend/RTLgenspec.v # COQC x86/Conventions1.v # COQC backend/Inliningspec.v # COQC backend/Renumberproof.v # Error: System error: "No space left on device" # # make[1]: *** [Makefile:259: backend/Renumberproof.vo] Error 1 # make[1]: *** Waiting for unfinished jobs.... # make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-compcert.3.11' # make: *** [Makefile:190: all] Error 2 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-compcert 3.11 +- - No changes have been performed # Run eval $(opam env) to update the current shell environment 'opam install -y -v coq-compcert.3.11 coq.8.15.1' failed.
No files were installed.
true