# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-domains base base-nnp base Naked pointers prohibited in the OCaml heap base-threads base base-unix base conf-gmp 4 Virtual package relying on a GMP lib system installation coq 8.17.1 The Coq Proof Assistant coq-core 8.17.1 The Coq Proof Assistant -- Core Binaries and Tools coq-stdlib 8.17.1 The Coq Proof Assistant -- Standard Library coqide-server 8.17.1 The Coq Proof Assistant, XML protocol server dune 3.12.1 Fast, portable, and opinionated build system ocaml 5.1.1 The OCaml compiler (virtual package) ocaml-base-compiler 5.1.1 Official release 5.1.1 ocaml-config 3 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" maintainer: "palmskog@gmail.com" homepage: "https://github.com/coq-community/coq-dpdgraph" dev-repo: "git+https://github.com/coq-community/coq-dpdgraph.git" bug-reports: "https://github.com/coq-community/coq-dpdgraph/issues" license: "LGPL-2.1-only" synopsis: "Compute dependencies between Coq objects (definitions, theorems) and produce graphs" description: """ Coq plugin that extracts the dependencies between Coq objects, and produces files with dependency information. Includes tools to visualize dependency graphs and find unused definitions.""" build: [ ["./configure"] [make "-j%{jobs}%" "WARN_ERR="] ] install: [make "install" "BINDIR=%{bin}%"] depends: [ "ocaml" {>= "4.09.0"} "coq" {>= "8.16" & < "8.18~"} "ocamlgraph" ] tags: [ "category:Miscellaneous/Coq Extensions" "keyword:dependency graph" "keyword:dependency analysis" "logpath:dpdgraph" "date:2022-01-21" ] authors: [ "Anne Pacalet" "Yves Bertot" "Olivier Pons" ] url { src: "https://github.com/coq-community/coq-dpdgraph/releases/download/v1.0%2B8.16/coq-dpdgraph-1.0-8.16.tgz" checksum: "sha512=6ed4db949867b3a7761f9ed09213613fe32d04b5d13d15ffbad6fb2b1a24dd5ccebade61f6c288e95b578c355ccc6977b485c3630764703d09b6fc6d29a3a446" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-dpdgraph.1.0+8.16 coq.8.17.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-dpdgraph.1.0+8.16 coq.8.17.1
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-dpdgraph.1.0+8.16 coq.8.17.1
# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-domains base base-nnp base Naked pointers prohibited in the OCaml heap base-threads base base-unix base conf-gmp 4 Virtual package relying on a GMP lib system installation coq 8.17.1 The Coq Proof Assistant coq-core 8.17.1 The Coq Proof Assistant -- Core Binaries and Tools coq-stdlib 8.17.1 The Coq Proof Assistant -- Standard Library coqide-server 8.17.1 The Coq Proof Assistant, XML protocol server dune 3.12.1 Fast, portable, and opinionated build system ocaml 5.1.1 The OCaml compiler (virtual package) ocaml-base-compiler 5.1.1 Official release 5.1.1 ocaml-config 3 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 ocamlgraph 2.1.0 A generic graph library for OCaml stdlib-shims 0.3.0 Backport some of the new stdlib features to older compiler zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers [NOTE] Package coq is already installed (current version is 8.17.1). The following actions will be performed: - install coq-dpdgraph 1.0+8.16 <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/3: [coq-dpdgraph.1.0+8.16: http] Processing 1/3: -> retrieved coq-dpdgraph.1.0+8.16 (https://github.com/coq-community/coq-dpdgraph/releases/download/v1.0%2B8.16/coq-dpdgraph-1.0-8.16.tgz) Processing 2/3: [coq-dpdgraph: ./configure] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./configure" (CWD=/home/bench/.opam/ocaml-base-compiler.5.1.1/.opam-switch/build/coq-dpdgraph.1.0+8.16) - configure: coq-dpdgraph version 1.0-8.16 - configure: ~~~~~~~~~~~~~~~~~~~~ - configure: ~~ OCaml compilers - configure: ~~~~~~~~~~~~~~~~~~~~ - checking for ocamlc... ocamlc - checking ocamlc version... 5.1.1 - checking ocamlc -safe-string option... yes - checking ocaml library path... /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/ocaml - checking for ocamlopt... ocamlopt - checking ocamlopt version... ok - checking for ocamlc.opt... ocamlc.opt - checking ocamlc.opt version... ok - checking for ocamlopt.opt... ocamlopt.opt - checking ocamlc.opt version... ok - checking for ocamldep... ocamldep - checking for ocamllex... ocamllex - checking for ocamllex.opt... ocamllex.opt - checking for ocamlyacc... ocamlyacc - checking for ocamldoc... ocamldoc - checking for ocamldoc.opt... ocamldoc.opt - configure: ~~~~~~~~~~~~~~~ - configure: ~~ ocamlgraph - configure: ~~~~~~~~~~~~~~~ - checking for ocamlfind... ocamlfind - checking ocamlfind compatibility... yes - checking ocamlgraph package... /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/ocamlgraph - configure: ~~~~~~~~ - configure: ~~ Coq - configure: ~~~~~~~~ - checking for coqc... coqc - checking coq version... Fatal error: Not enough heap memory to reserve minor heaps - - checking for coq_makefile... coq_makefile - configure: ~~~~~~~~~~~~~~~~~~~~~~ - configure: ~~ creating Makefile - configure: ~~~~~~~~~~~~~~~~~~~~~~ - configure: creating ./config.status - config.status: creating Makefile Processing 2/3: [coq-dpdgraph: make] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" "WARN_ERR=" (CWD=/home/bench/.opam/ocaml-base-compiler.5.1.1/.opam-switch/build/coq-dpdgraph.1.0+8.16) - * build version.ml - * build dpd_parse.ml - ocamlyacc dpd_parse.mly - * build dpd_lex.ml - ocamllex.opt dpd_lex.mll - 29 states, 495 transitions, table size 2154 bytes - * build .depend - ocamldep version.ml dpd_compute.ml dpd_dot.ml dpd_parse.ml dpd_lex.ml dpd2dot.ml dpdusage.ml *.mli > .depend - * build Make_coq - coq_makefile -f Make -o Make_coq - * build version.cmi - ocamlc.opt -w +a -g -dtypes -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/ocamlgraph -c version.mli - * build dpd_compute.cmi - ocamlc.opt -w +a -g -dtypes -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/ocamlgraph -c dpd_compute.mli - * build dpd2dot.cmi - ocamlc.opt -w +a -g -dtypes -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/ocamlgraph -c dpd2dot.mli - * build dpdgraph.vo - * build version.cmo - make -f Make_coq dpdgraph.vo - ocamlc.opt -w +a -g -dtypes -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/ocamlgraph -c version.ml - make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.5.1.1/.opam-switch/build/coq-dpdgraph.1.0+8.16' - * build dpd_compute.cmo - ocamlc.opt -w +a -g -dtypes -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/ocamlgraph -c dpd_compute.ml - * build dpd_dot.cmi - ocamlc.opt -w +a -g -dtypes -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/ocamlgraph -c dpd_dot.mli - * build dpd_parse.cmi - ocamlc.opt -w +a -g -dtypes -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/ocamlgraph -c dpd_parse.mli - * build dpdusage.cmi - Fatal error: Not enough heap memory to reserve minor heaps - * build dpd_dot.cmo - ocamlc.opt -w +a -g -dtypes -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/ocamlgraph -c dpdusage.mli - ocamlc.opt -w +a -g -dtypes -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/ocamlgraph -c dpd_dot.ml - * build dpd_parse.cmo - ocamlc.opt -w +a -g -dtypes -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/ocamlgraph -c dpd_parse.ml - * build dpd_lex.cmi - ocamlc.opt -w +a -g -dtypes -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/ocamlgraph -c dpd_lex.mli - * build dpd_lex.cmo - ocamlc.opt -w +a -g -dtypes -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/ocamlgraph -c dpd_lex.ml - * build dpd2dot.cmo - ocamlc.opt -w +a -g -dtypes -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/ocamlgraph -c dpd2dot.ml - * build dpdusage.cmo - ocamlc.opt -w +a -g -dtypes -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/ocamlgraph -c dpdusage.ml - * build dpd2dot - ocamlc.opt -g -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/ocamlgraph -o dpd2dot graph.cma version.cmo dpd_compute.cmo dpd_dot.cmo dpd_parse.cmo dpd_lex.cmo dpd2dot.cmo - * build dpdusage - ocamlc.opt -g -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/ocamlgraph -o dpdusage graph.cma version.cmo dpd_compute.cmo dpd_dot.cmo dpd_parse.cmo dpd_lex.cmo dpdusage.cmo - Aborted (core dumped) - COQPP searchdepend.mlg - COQDEP VFILES - COQPP graphdepend.mlg - OCAMLLIBDEP dpdgraph.mllib - CAMLDEP graphdepend.ml - CAMLDEP searchdepend.ml - Fatal error: Not enough heap memory to reserve minor heaps - Aborted (core dumped) - CAMLOPT -c searchdepend.ml - CAMLOPT -c graphdepend.ml - CAMLOPT -a -o dpdgraph.cmxa - CAMLOPT -shared -o dpdgraph.cmxs - COQC dpdgraph.v - Fatal error: Not enough heap memory to reserve minor heaps - Aborted (core dumped) - make[1]: *** [Make_coq:830: dpdgraph.vo] Error 134 - make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.5.1.1/.opam-switch/build/coq-dpdgraph.1.0+8.16' - make: *** [Makefile:80: dpdgraph.vo] Error 2 [ERROR] The compilation of coq-dpdgraph.1.0+8.16 failed at "make -j4 WARN_ERR=". #=== ERROR while compiling coq-dpdgraph.1.0+8.16 ==============================# # context 2.1.5 | linux/x86_64 | ocaml-base-compiler.5.1.1 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.5.1.1/.opam-switch/build/coq-dpdgraph.1.0+8.16 # command ~/.opam/opam-init/hooks/sandbox.sh build make -j4 WARN_ERR= # exit-code 2 # env-file ~/.opam/log/coq-dpdgraph-26456-493912.env # output-file ~/.opam/log/coq-dpdgraph-26456-493912.out ### output ### # [...] # Fatal error: Not enough heap memory to reserve minor heaps # Aborted (core dumped) # CAMLOPT -c searchdepend.ml # CAMLOPT -c graphdepend.ml # CAMLOPT -a -o dpdgraph.cmxa # CAMLOPT -shared -o dpdgraph.cmxs # COQC dpdgraph.v # Fatal error: Not enough heap memory to reserve minor heaps # Aborted (core dumped) # make[1]: *** [Make_coq:830: dpdgraph.vo] Error 134 # make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.5.1.1/.opam-switch/build/coq-dpdgraph.1.0+8.16' # make: *** [Makefile:80: dpdgraph.vo] Error 2 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-dpdgraph 1.0+8.16 +- - No changes have been performed # Run eval $(opam env) to update the current shell environment 'opam install -y -v coq-dpdgraph.1.0+8.16 coq.8.17.1' failed.
No files were installed.
true