ยซ Up

dpdgraph 1.0+8.17 Error ๐Ÿ”ฅ

Context

# 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.17" & < "8.18~"}
  "ocamlgraph" 
]
tags: [
  "category:Miscellaneous/Coq Extensions"
  "keyword:dependency graph"
  "keyword:dependency analysis"
  "logpath:dpdgraph"
  "date:2023-03-23"
]
authors: [
  "Anne Pacalet"
  "Yves Bertot"
  "Olivier Pons"
]
url {
  src: "https://github.com/coq-community/coq-dpdgraph/releases/download/v1.0%2B8.17/coq-dpdgraph-1.0-8.17.tgz"
  checksum: "sha512=a649d4e77ed8cc66c9ccaa6f8e84ee8600cbf2b24e01a2b90c43739516e988180075be6e5b6557ad1840632966c5c46233ebce067f9eb46e4c25b3291fc0c7bd"
}

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-dpdgraph.1.0+8.17 coq.8.17.1
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-dpdgraph.1.0+8.17 coq.8.17.1
Return code
0
Duration
1 m 0 s

Install ๐Ÿš€

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-dpdgraph.1.0+8.17 coq.8.17.1
Return code
7936
Duration
2 m 0 s
Output
# 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.17
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/3: [coq-dpdgraph.1.0+8.17: http]
Processing  1/3:
-> retrieved coq-dpdgraph.1.0+8.17  (https://github.com/coq-community/coq-dpdgraph/releases/download/v1.0%2B8.17/coq-dpdgraph-1.0-8.17.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.17)
- configure: coq-dpdgraph version 1.0-8.17
- 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.17)
-    * 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
-    * build version.cmi
- coq_makefile -f Make -o Make_coq
- 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.17'
-    * 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
- Fatal error: Not enough heap memory to reserve minor heaps
-    * build dpdusage.cmi
- ocamlc.opt -w +a  -g -dtypes -I /home/bench/.opam/ocaml-base-compiler.5.1.1/lib/ocamlgraph -c dpdusage.mli
-    * build dpd_dot.cmo
- 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)
- COQDEP VFILES
- COQPP searchdepend.mlg
- 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.17'
- make: *** [Makefile:80: dpdgraph.vo] Error 2
[ERROR] The compilation of coq-dpdgraph.1.0+8.17 failed at "make -j4 WARN_ERR=".
#=== ERROR while compiling coq-dpdgraph.1.0+8.17 ==============================#
# 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.17
# command              ~/.opam/opam-init/hooks/sandbox.sh build make -j4 WARN_ERR=
# exit-code            2
# env-file             ~/.opam/log/coq-dpdgraph-20877-8c7c23.env
# output-file          ~/.opam/log/coq-dpdgraph-20877-8c7c23.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.17'
# make: *** [Makefile:80: dpdgraph.vo] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-dpdgraph 1.0+8.17
+- 
- No changes have been performed
# Run eval $(opam env) to update the current shell environment
'opam install -y -v coq-dpdgraph.1.0+8.17 coq.8.17.1' failed.

Installation size

No files were installed.

Uninstall ๐Ÿงน

Command
true
Return code
0
Missing removes
none
Wrong removes
none