# 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 dev Formal proof management system
dune 3.0.3 Fast, portable, and opinionated build system
ocaml 4.11.2 The OCaml compiler (virtual package)
ocaml-base-compiler 4.11.2 Official release 4.11.2
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.3 A library manager for OCaml
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "Enrico Tassi <enrico.tassi@inria.fr>"
authors: [ "Cyril Cohen" "Kazuhiko Sakaguchi" "Enrico Tassi" ]
license: "MIT"
homepage: "https://github.com/math-comp/hierarchy-builder"
bug-reports: "https://github.com/math-comp/hierarchy-builder/issues"
dev-repo: "git+https://github.com/math-comp/hierarchy-builder"
build: [ [ make "build"]
[ make "test-suite" ] {with-test}
]
install: [ make "install" ]
depends: [ "coq-elpi" { (>= "1.11.0" & < "1.14~") | = "dev" } ]
conflicts: [ "coq-hierarchy-builder-shim" ]
synopsis: "High level commands to declare and evolve a hierarchy based on packed classes"
description: """
Hierarchy Builder is a high level language to build hierarchies of algebraic structures and make these
hierarchies evolve without breaking user code. The key concepts are the ones of factory, builder
and abbreviation that let the hierarchy developer describe an actual interface for their library.
Behind that interface the developer can provide appropriate code to ensure retro compatibility.
"""
tags: [ "logpath:HB" ]
url {
src: "https://github.com/math-comp/hierarchy-builder/archive/v1.2.1.tar.gz"
checksum: "sha256=a515d4fea55c30a6346877edfa6f23447a19c6875feb889ec21bed062c004060"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-hierarchy-builder.1.2.1 coq.devDry 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-hierarchy-builder.1.2.1 coq.devopam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-hierarchy-builder.1.2.1 coq.dev# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base camlp5 7.14 Preprocessor-pretty-printer of OCaml conf-findutils 1 Virtual package relying on findutils conf-gmp 4 Virtual package relying on a GMP lib system installation conf-perl 2 Virtual package relying on perl coq dev Formal proof management system coq-elpi dev Elpi extension language for Coq cppo 1.6.8 Code preprocessor like cpp for OCaml dune 3.0.3 Fast, portable, and opinionated build system elpi 1.14.1 ELPI - Embeddable λProlog Interpreter ocaml 4.11.2 The OCaml compiler (virtual package) ocaml-base-compiler 4.11.2 Official release 4.11.2 ocaml-compiler-libs v0.12.4 OCaml compiler libraries repackaged ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.3 A library manager for OCaml ppx_derivers 1.2.1 Shared [@@deriving] plugin registry ppx_deriving 5.2.1 Type-driven code generation for OCaml ppxlib 0.25.0 Standard library for ppx rewriters re 1.10.3 RE is a regular expression library for OCaml result 1.5 Compatibility Result module seq base Compatibility package for OCaml's standard iterator type starting from 4.07. sexplib0 v0.15.0 Library containing the definition of S-expressions and some base converters stdlib-shims 0.3.0 Backport some of the new stdlib features to older compiler zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers [NOTE] Package coq is already installed (current version is dev). The following actions will be performed: - install coq-hierarchy-builder 1.2.1 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/1: [coq-hierarchy-builder.1.2.1: http] [coq-hierarchy-builder.1.2.1] downloaded from https://github.com/math-comp/hierarchy-builder/archive/v1.2.1.tar.gz Processing 1/1: <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/2: [coq-hierarchy-builder: make build] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "build" (CWD=/home/bench/.opam/ocaml-base-compiler.4.11.2/.opam-switch/build/coq-hierarchy-builder.1.2.1) - ocamlc unix.cma str.cma -g hb.ml -o coq.hb - /home/bench/.opam/ocaml-base-compiler.4.11.2/bin/coq_makefile -f _CoqProject -o Makefile.coq - make -f Makefile.coq - make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.11.2/.opam-switch/build/coq-hierarchy-builder.1.2.1' - COQDEP VFILES - *** Warning: in file structures.v, library elpi is required from root elpi and has not been found in the loadpath! - COQC structures.v - File "./structures.v", line 15, characters 0-30: - Error: Cannot find a physical path bound to logical path - elpi with prefix elpi. - - make[2]: *** [Makefile.coq:791: structures.vo] Error 1 - make[1]: *** [Makefile.coq:408: all] Error 2 - make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.11.2/.opam-switch/build/coq-hierarchy-builder.1.2.1' - make: *** [Makefile:97: this-build] Error 2 [ERROR] The compilation of coq-hierarchy-builder failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make build". #=== ERROR while compiling coq-hierarchy-builder.1.2.1 ========================# # context 2.0.7 | linux/x86_64 | ocaml-base-compiler.4.11.2 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.11.2/.opam-switch/build/coq-hierarchy-builder.1.2.1 # command ~/.opam/opam-init/hooks/sandbox.sh build make build # exit-code 2 # env-file ~/.opam/log/coq-hierarchy-builder-17353-335865.env # output-file ~/.opam/log/coq-hierarchy-builder-17353-335865.out ### output ### # [...] # make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.11.2/.opam-switch/build/coq-hierarchy-builder.1.2.1' # COQDEP VFILES # *** Warning: in file structures.v, library elpi is required from root elpi and has not been found in the loadpath! # COQC structures.v # File "./structures.v", line 15, characters 0-30: # Error: Cannot find a physical path bound to logical path # elpi with prefix elpi. # # make[2]: *** [Makefile.coq:791: structures.vo] Error 1 # make[1]: *** [Makefile.coq:408: all] Error 2 # make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.11.2/.opam-switch/build/coq-hierarchy-builder.1.2.1' # make: *** [Makefile:97: this-build] Error 2 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-hierarchy-builder 1.2.1 +- - No changes have been performed # Run eval $(opam env) to update the current shell environment 'opam install -y -v coq-hierarchy-builder.1.2.1 coq.dev' failed.
No files were installed.
true