# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-findutils 1 Virtual package relying on findutils conf-m4 1 Virtual package relying on m4 coq 8.10.0 Formal proof management system num 1.3 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.06.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.06.1 Official 4.06.1 release ocaml-config 1 OCaml Switch Configuration ocamlfind 1.8.1 A library manager for OCaml # opam file: opam-version: "2.0" authors: [ "Google Inc." "Massachusetts Institute of Technology" ] maintainer: "Jason Gross <jgross@mit.edu>" homepage: "https://github.com/mit-plv/rewriter" bug-reports: "https://github.com/mit-plv/rewriter/issues" license: "MIT" build: [ [make "-j%{jobs}%" "perf-Slow" "EXTERNAL_PERF_DEPENDENCIES=1" "TIMED=1"] ] install: [] depends: [ "coq" {>= "8.9~"} "conf-time" "coq-rewriter" ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" synopsis: "Performance Benchmark for Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting" url { src: "git+https://github.com/mit-plv/rewriter.git#master" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-rewriter-perf-Slow.dev coq.8.10.0
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 2h opam install -y --deps-only coq-rewriter-perf-Slow.dev coq.8.10.0
# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-findutils 1 Virtual package relying on findutils conf-m4 1 Virtual package relying on m4 coq 8.10.0 Formal proof management system num 1.3 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.06.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.06.1 Official 4.06.1 release ocaml-config 1 OCaml Switch Configuration ocamlfind 1.8.1 A library manager for OCaml The following actions will be performed: - install coq-rewriter dev - install conf-which 1 - install conf-time 1 ===== 3 to install ===== <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> [coq-rewriter.dev] synchronised from git+https://github.com/mit-plv/rewriter.git#master <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> -> installed conf-which.1 [ERROR] The compilation of conf-time failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build which time". -> installed coq-rewriter.dev #=== ERROR while compiling conf-time.1 ========================================# # context 2.0.5 | linux/x86_64 | ocaml-base-compiler.4.06.1 | https://opam.ocaml.org#a33e1dcf # path ~/.opam/ocaml-base-compiler.4.06.1/.opam-switch/build/conf-time.1 # command ~/.opam/opam-init/hooks/sandbox.sh build which time # exit-code 1 # env-file ~/.opam/log/conf-time-4233-b76d46.env # output-file ~/.opam/log/conf-time-4233-b76d46.out <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build conf-time 1 +- +- The following changes have been performed | - install conf-which 1 | - install coq-rewriter dev +- The packages you requested declare the following system dependencies. Please make sure they are installed before retrying: time # 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.06.1/.opam-switch/backup/state-20200821093442.export"
true
No files were installed.
true