« Up

mtac2 dev Error with dependencies 🚒

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                   dev         The Coq Proof Assistant
coq-core              dev         The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib            dev         The Coq Proof Assistant -- Standard Library
coqide-server         dev         The Coq Proof Assistant, XML protocol server
dune                  3.12.2      Fast, portable, and opinionated build system
ocaml                 5.0.0       The OCaml compiler (virtual package)
ocaml-base-compiler   5.0.0       Official release 5.0.0
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: "beta.ziliani@gmail.com"
homepage: "https://github.com/Mtac2/Mtac2"
dev-repo: "git+https://github.com/Mtac2/Mtac2.git"
bug-reports: "https://github.com/Mtac2/Mtac2/issues"
authors: ["Beta Ziliani <beta.ziliani@gmail.com>" "Jan-Oliver Kaiser <janno@mpi-sws.org>" "Robbert Krebbers <mail@robbertkrebbers.nl>" "Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr>" "Derek Dreyer <dreyer@mpi-sws.org>"]
license: "MIT"
build: [
  ["coq_makefile" "-f" "_CoqProject" "-o" "Makefile"]
  [make "-j%{jobs}%"]
]
install: [
  [make "install"]
]
depends: [
  "ocaml"
  "coq" {>= "8.13" | = "dev"}
  "coq-unicoq" {>= "1.5" | = "dev"}
]
synopsis: "Mtac2: Typed Tactics for Coq"
tags: [
  "logpath:Mtac2"
]
url {
  src: "git+https://github.com/Mtac2/Mtac2.git#master"
}

Lint

Command: true
Return code: 0

Dry install 🏜️

Dry install with the current Coq version:

Command: opam install -y --show-action coq-mtac2.dev coq.dev
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-mtac2.dev coq.dev

Return code

7936

Duration

1 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                   dev         The Coq Proof Assistant
coq-core              dev         The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib            dev         The Coq Proof Assistant -- Standard Library
coqide-server         dev         The Coq Proof Assistant, XML protocol server
dune                  3.12.2      Fast, portable, and opinionated build system
ocaml                 5.0.0       The OCaml compiler (virtual package)
ocaml-base-compiler   5.0.0       Official release 5.0.0
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
The following actions will be performed:
  - install coq-unicoq dev
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> retrieved coq-unicoq.dev  (git+https://github.com/unicoq/unicoq.git#master)
[ERROR] The compilation of coq-unicoq.dev failed at "make -j4".
#=== ERROR while compiling coq-unicoq.dev =====================================#
# context              2.1.5 | linux/x86_64 | ocaml-base-compiler.5.0.0 | file:///home/bench/run/opam-coq-archive/extra-dev
# path                 ~/.opam/ocaml-base-compiler.5.0.0/.opam-switch/build/coq-unicoq.dev
# command              ~/.opam/opam-init/hooks/sandbox.sh build make -j4
# exit-code            2
# env-file             ~/.opam/log/coq-unicoq-4325-d173f0.env
# output-file          ~/.opam/log/coq-unicoq-4325-d173f0.out
### output ###
# 1239 |     | Proj (c1, _, t1), Proj (c2, _, t2) when Names.Projection.repr_equal c1 c2 ->
# [...]
# Alert deprecated: Names.Projection.repr_equal
# Use an explicit projection of Repr
# CAMLOPT -c -for-pack Unicoq src/unitactics.ml
# CAMLOPT -pack -o src/unicoq.cmx
# CAMLOPT -a -o src/unicoq.cmxa
# CAMLOPT -shared -o src/unicoq.cmxs
# COQC theories/Unicoq.v
# Fatal error: Not enough heap memory to reserve minor heaps
# Aborted (core dumped)
# make[1]: *** [Makefile:847: theories/Unicoq.vo] Error 134
# make: *** [Makefile:417: all] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-unicoq dev
+- 
- No changes have been performed
# Run eval $(opam env) to update the current shell environment

Install 🚀

Command: true
Return code: 0
Duration: 0 s

Installation size

No files were installed.

Uninstall 🧹

Command: true
Return code: 0
Missing removes: none
Wrong removes: none