This result is black-listed as it is considered as too hard to reproduce / to solve. If you find a way to fix this package, please make a pull-request to github.com/coq/opam-coq-archive. The list of black-listed packages is in black_list.rb.
# 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 8.15.0 Formal proof management system
dune 3.2.0 Fast, portable, and opinionated build system
ocaml 4.14.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.14.0 Official release 4.14.0
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
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 ]
install: [ make "install" "VFILES=structures.v" ]
depends: [
"coq-elpi" {>= "1.5.0" & < "1.6.0~"}
]
synopsis: "Hierarchy Builder"
description: """
High level commands to declare and evolve a hierarchy based on packed classes.
"""
url {
src: "https://github.com/math-comp/hierarchy-builder/archive/v0.10.0.tar.gz"
checksum: "sha256=170ad371db025ddf7750235ce9cad45755482930adb751739e1bc13b4c77f858"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-hierarchy-builder.0.10.0 coq.8.15.0[NOTE] Package coq is already installed (current version is 8.15.0).
The following dependencies couldn't be met:
- coq-hierarchy-builder -> coq-elpi < 1.6.0~ -> coq < 8.13~ -> ocaml < 4.12
base of this switch (use `--unlock-base' to force)
No solution found, exiting
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
opam remove -y coq; opam install -y --show-action --unlock-base coq-hierarchy-builder.0.10.0The following actions will be performed:
- remove coq 8.15.0
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[WARNING] While removing coq.8.15.0: not removing files that changed since:
- share/texmf/tex/latex/misc/coqdoc.sty
- man/man1/coqwc.1
- man/man1/coqtop.opt.1
- man/man1/coqtop.byte.1
- man/man1/coqtop.1
- man/man1/coqnative.1
- man/man1/coqdoc.1
- man/man1/coqdep.1
- man/man1/coqchk.1
- man/man1/coqc.1
- man/man1/coq_makefile.1
- man/man1/coq-tex.1
- lib/stublibs/dllcoqrun_stubs.so
- lib/coqide-server/protocol/xmlprotocol.mli
- lib/coqide-server/protocol/xmlprotocol.ml
- lib/coqide-server/protocol/xmlprotocol.cmx
- lib/coqide-server/protocol/xmlprotocol.cmti
- lib/coqide-server/protocol/xmlprotocol.cmt
- lib/coqide-server/protocol/xmlprotocol.cmi
- lib/coqide-server/protocol/xml_printer.mli
- lib/coqide-server/protocol/xml_printer.ml
- lib/coqide-server/protocol/xml_printer.cmx
- lib/coqide-server/protocol/xml_printer.cmti
- lib/coqide-server/protocol/xml_printer.cmt
- lib/coqide-server/protocol/xml_printer.cmi
- lib/coqide-server/protocol/xml_parser.mli
- lib/coqide-server/protocol/xml_parser.ml
- lib/coqide-server/protocol/xml_parser.cmx
- lib/coqide-server/protocol/xml_parser.cmti
- lib/coqide-server/protocol/xml_parser.cmt
- lib/coqide-server/protocol/xml_parser.cmi
- lib/coqide-server/protocol/xml_lexer.mli
- lib/coqide-server/protocol/xml_lexer.ml
- lib/coqide-server/protocol/xml_lexer.cmx
- lib/coqide-server/protocol/xml_lexer.cmti
- lib/coqide-server/protocol/xml_lexer.cmt
- lib/coqide-server/protocol/xml_lexer.cmi
- lib/coqide-server/protocol/serialize.mli
- lib/coqide-server/protocol/serialize.ml
- lib/coqide-server/protocol/serialize.cmx
- lib/coqide-server/protocol/serialize.cmti
- lib/coqide-server/protocol/serialize.cmt
- lib/coqide-server/protocol/serialize.cmi
- lib/coqide-server/protocol/richpp.mli
- lib/coqide-server/protocol/richpp.ml
- lib/coqide-server/protocol/richpp.cmx
- lib/coqide-server/protocol/richpp.cmti
- lib/coqide-server/protocol/richpp.cmt
- lib/coqide-server/protocol/richpp.cmi
- lib/coqide-server/protocol/protocol.cmxs
- lib/coqide-server/protocol/protocol.cmxa
- lib/coqide-server/protocol/protocol.cma
- lib/coqide-server/protocol/protocol.a
- lib/coqide-server/protocol/interface.ml
- lib/coqide-server/protocol/interface.cmx
- lib/coqide-server/protocol/interface.cmt
- lib/coqide-server/protocol/interface.cmi
- lib/coqide-server/opam
- lib/coqide-server/dune-package
- lib/coqide-server/core/document.mli
- lib/coqide-server/core/document.ml
- lib/coqide-server/core/document.cmx
- lib/coqide-server/core/document.cmti
- lib/coqide-server/core/document.cmt
- lib/coqide-server/core/document.cmi
- lib/coqide-server/core/core.cmxs
- lib/coqide-server/core/core.cmxa
- lib/coqide-server/core/core.cma
- lib/coqide-server/core/core.a
- lib/coqide-server/META
- lib/coq/user-contrib/Ltac2/String.vos
- lib/coq/user-contrib/Ltac2/String.vo
- lib/coq/user-contrib/Ltac2/String.v
- lib/coq/user-contrib/Ltac2/String.glob
- lib/coq/user-contrib/Ltac2/Std.vos
- lib/coq/user-contrib/Ltac2/Std.vo
- lib/coq/user-contrib/Ltac2/Std.v
- lib/coq/user-contrib/Ltac2/Std.glob
- lib/coq/user-contrib/Ltac2/Printf.vos
- lib/coq/user-contrib/Ltac2/Printf.vo
- lib/coq/user-contrib/Ltac2/Printf.v
- lib/coq/user-contrib/Ltac2/Printf.glob
- lib/coq/user-contrib/Ltac2/Pattern.vos
- lib/coq/user-contrib/Ltac2/Pattern.vo
- lib/coq/user-contrib/Ltac2/Pattern.v
- lib/coq/user-contrib/Ltac2/Pattern.glob
- lib/coq/user-contrib/Ltac2/Option.vos
- lib/coq/user-contrib/Ltac2/Option.vo
- lib/coq/user-contrib/Ltac2/Option.v
- lib/coq/user-contrib/Ltac2/Option.glob
- lib/coq/user-contrib/Ltac2/Notations.vos
- lib/coq/user-contrib/Ltac2/Notations.vo
- lib/coq/user-contrib/Ltac2/Notations.v
- lib/coq/user-contrib/Ltac2/Notations.glob
- lib/coq/user-contrib/Ltac2/Message.vos
- lib/coq/user-contrib/Ltac2/Message.vo
- lib/coq/user-contrib/Ltac2/Message.v
- lib/coq/user-contrib/Ltac2/Message.glob
- lib/coq/user-contrib/Ltac2/Ltac2.vos
- lib/coq/user-contrib/Ltac2/Ltac2.vo
- lib/coq/user-contrib/Ltac2/Ltac2.v
- lib/coq/user-contrib/Ltac2/Ltac2.glob
- lib/coq/user-contrib/Ltac2/Ltac1.vos
- lib/coq/user-contrib/Ltac2/Ltac1.vo
- lib/coq/user-contrib/Ltac2/Ltac1.v
- lib/coq/user-contrib/Ltac2/Ltac1.glob
- lib/coq/user-contrib/Ltac2/List.vos
- lib/coq/user-contrib/Ltac2/List.vo
- lib/coq/user-contrib/Ltac2/List.v
- lib/coq/user-contrib/Ltac2/List.glob
- lib/coq/user-contrib/Ltac2/Int.vos
- lib/coq/user-contrib/Ltac2/Int.vo
- lib/coq/user-contrib/Ltac2/Int.v
- lib/coq/user-contrib/Ltac2/Int.glob
- lib/coq/user-contrib/Ltac2/Init.vos
- lib/coq/user-contrib/Ltac2/Init.vo
- lib/coq/user-contrib/Ltac2/Init.v
- lib/coq/user-contrib/Ltac2/Init.glob
- lib/coq/user-contrib/Ltac2/Ind.vos
- lib/coq/user-contrib/Ltac2/Ind.vo
- lib/coq/user-contrib/Ltac2/Ind.v
- lib/coq/user-contrib/Ltac2/Ind.glob
- lib/coq/user-contrib/Ltac2/Ident.vos
- lib/coq/user-contrib/Ltac2/Ident.vo
- lib/coq/user-contrib/Ltac2/Ident.v
- lib/coq/user-contrib/Ltac2/Ident.glob
- lib/coq/user-contrib/Ltac2/Fresh.vos
- lib/coq/user-contrib/Ltac2/Fresh.vo
- lib/coq/user-contrib/Ltac2/Fresh.v
- lib/coq/user-contrib/Ltac2/Fresh.glob
- lib/coq/user-contrib/Ltac2/Env.vos
- lib/coq/user-contrib/Ltac2/Env.vo
- lib/coq/user-contrib/Ltac2/Env.v
- lib/coq/user-contrib/Ltac2/Env.glob
- lib/coq/user-contrib/Ltac2/Control.vos
- lib/coq/user-contrib/Ltac2/Control.vo
- lib/coq/user-contrib/Ltac2/Control.v
- lib/coq/user-contrib/Ltac2/Control.glob
- lib/coq/user-contrib/Ltac2/Constr.vos
- lib/coq/user-contrib/Ltac2/Constr.vo
- lib/coq/user-contrib/Ltac2/Constr.v
- lib/coq/user-contrib/Ltac2/Constr.glob
- lib/coq/user-contrib/Ltac2/Char.vos
- lib/coq/user-contrib/Ltac2/Char.vo
- lib/coq/user-contrib/Ltac2/Char.v
- lib/coq/user-contrib/Ltac2/Char.glob
- lib/coq/user-contrib/Ltac2/Bool.vos
- lib/coq/user-contrib/Ltac2/Bool.vo
- lib/coq/user-contrib/Ltac2/Bool.v
- lib/coq/user-contrib/Ltac2/Bool.glob
- lib/coq/user-contrib/Ltac2/Array.vos
- lib/coq/user-contrib/Ltac2/Array.vo
- lib/coq/user-contrib/Ltac2/Array.v
- lib/coq/user-contrib/Ltac2/Array.glob
- lib/coq/theories/ssrmatching/ssrmatching.vos
- lib/coq/theories/ssrmatching/ssrmatching.vo
- lib/coq/theories/ssrmatching/ssrmatching.v
- lib/coq/theories/ssrmatching/ssrmatching.glob
- lib/coq/theories/ssr/ssrunder.vos
- lib/coq/theories/ssr/ssrunder.vo
- lib/coq/theories/ssr/ssrunder.v
- lib/coq/theories/ssr/ssrunder.glob
- lib/coq/theories/ssr/ssrsetoid.vos
- lib/coq/theories/ssr/ssrsetoid.vo
- lib/coq/theories/ssr/ssrsetoid.v
- lib/coq/theories/ssr/ssrsetoid.glob
- lib/coq/theories/ssr/ssrfun.vos
- lib/coq/theories/ssr/ssrfun.vo
- lib/coq/theories/ssr/ssrfun.v
- lib/coq/theories/ssr/ssrfun.glob
- lib/coq/theories/ssr/ssreflect.vos
- lib/coq/theories/ssr/ssreflect.vo
- lib/coq/theories/ssr/ssreflect.v
- lib/coq/theories/ssr/ssreflect.glob
- lib/coq/theories/ssr/ssrclasses.vos
- lib/coq/theories/ssr/ssrclasses.vo
- lib/coq/theories/ssr/ssrclasses.v
- lib/coq/theories/ssr/ssrclasses.glob
- lib/coq/theories/ssr/ssrbool.vos
- lib/coq/theories/ssr/ssrbool.vo
- lib/coq/theories/ssr/ssrbool.v
- lib/coq/theories/ssr/ssrbool.glob
- lib/coq/theories/setoid_ring/ZArithRing.vos
- lib/coq/theories/setoid_ring/ZArithRing.vo
- lib/coq/theories/setoid_ring/ZArithRing.v
- lib/coq/theories/setoid_ring/ZArithRing.glob
- lib/coq/theories/setoid_ring/Rings_Z.vos
- lib/coq/theories/setoid_ring/Rings_Z.vo
- lib/coq/theories/setoid_ring/Rings_Z.v
- lib/coq/theories/setoid_ring/Rings_Z.glob
- lib/coq/theories/setoid_ring/Rings_R.vos
- lib/coq/theories/setoid_ring/Rings_R.vo
- lib/coq/theories/setoid_ring/Rings_R.v
- lib/coq/theories/setoid_ring/Ri
[...] truncated
cmx
- lib/coq-core/clib/heap.cmti
- lib/coq-core/clib/heap.cmt
- lib/coq-core/clib/heap.cmi
- lib/coq-core/clib/hashset.mli
- lib/coq-core/clib/hashset.ml
- lib/coq-core/clib/hashset.cmx
- lib/coq-core/clib/hashset.cmti
- lib/coq-core/clib/hashset.cmt
- lib/coq-core/clib/hashset.cmi
- lib/coq-core/clib/hashcons.mli
- lib/coq-core/clib/hashcons.ml
- lib/coq-core/clib/hashcons.cmx
- lib/coq-core/clib/hashcons.cmti
- lib/coq-core/clib/hashcons.cmt
- lib/coq-core/clib/hashcons.cmi
- lib/coq-core/clib/hMap.mli
- lib/coq-core/clib/hMap.ml
- lib/coq-core/clib/hMap.cmx
- lib/coq-core/clib/hMap.cmti
- lib/coq-core/clib/hMap.cmt
- lib/coq-core/clib/hMap.cmi
- lib/coq-core/clib/exninfo.mli
- lib/coq-core/clib/exninfo.ml
- lib/coq-core/clib/exninfo.cmx
- lib/coq-core/clib/exninfo.cmti
- lib/coq-core/clib/exninfo.cmt
- lib/coq-core/clib/exninfo.cmi
- lib/coq-core/clib/dyn.mli
- lib/coq-core/clib/dyn.ml
- lib/coq-core/clib/dyn.cmx
- lib/coq-core/clib/dyn.cmti
- lib/coq-core/clib/dyn.cmt
- lib/coq-core/clib/dyn.cmi
- lib/coq-core/clib/diff2.mli
- lib/coq-core/clib/diff2.ml
- lib/coq-core/clib/diff2.cmx
- lib/coq-core/clib/diff2.cmti
- lib/coq-core/clib/diff2.cmt
- lib/coq-core/clib/diff2.cmi
- lib/coq-core/clib/clib.cmxs
- lib/coq-core/clib/clib.cmxa
- lib/coq-core/clib/clib.cma
- lib/coq-core/clib/clib.a
- lib/coq-core/clib/cUnix.mli
- lib/coq-core/clib/cUnix.ml
- lib/coq-core/clib/cUnix.cmx
- lib/coq-core/clib/cUnix.cmti
- lib/coq-core/clib/cUnix.cmt
- lib/coq-core/clib/cUnix.cmi
- lib/coq-core/clib/cThread.mli
- lib/coq-core/clib/cThread.ml
- lib/coq-core/clib/cThread.cmx
- lib/coq-core/clib/cThread.cmti
- lib/coq-core/clib/cThread.cmt
- lib/coq-core/clib/cThread.cmi
- lib/coq-core/clib/cString.mli
- lib/coq-core/clib/cString.ml
- lib/coq-core/clib/cString.cmx
- lib/coq-core/clib/cString.cmti
- lib/coq-core/clib/cString.cmt
- lib/coq-core/clib/cString.cmi
- lib/coq-core/clib/cSig.mli
- lib/coq-core/clib/cSig.cmti
- lib/coq-core/clib/cSig.cmi
- lib/coq-core/clib/cSet.mli
- lib/coq-core/clib/cSet.ml
- lib/coq-core/clib/cSet.cmx
- lib/coq-core/clib/cSet.cmti
- lib/coq-core/clib/cSet.cmt
- lib/coq-core/clib/cSet.cmi
- lib/coq-core/clib/cObj.mli
- lib/coq-core/clib/cObj.ml
- lib/coq-core/clib/cObj.cmx
- lib/coq-core/clib/cObj.cmti
- lib/coq-core/clib/cObj.cmt
- lib/coq-core/clib/cObj.cmi
- lib/coq-core/clib/cMap.mli
- lib/coq-core/clib/cMap.ml
- lib/coq-core/clib/cMap.cmx
- lib/coq-core/clib/cMap.cmti
- lib/coq-core/clib/cMap.cmt
- lib/coq-core/clib/cMap.cmi
- lib/coq-core/clib/cList.mli
- lib/coq-core/clib/cList.ml
- lib/coq-core/clib/cList.cmx
- lib/coq-core/clib/cList.cmti
- lib/coq-core/clib/cList.cmt
- lib/coq-core/clib/cList.cmi
- lib/coq-core/clib/cEphemeron.mli
- lib/coq-core/clib/cEphemeron.ml
- lib/coq-core/clib/cEphemeron.cmx
- lib/coq-core/clib/cEphemeron.cmti
- lib/coq-core/clib/cEphemeron.cmt
- lib/coq-core/clib/cEphemeron.cmi
- lib/coq-core/clib/cArray.mli
- lib/coq-core/clib/cArray.ml
- lib/coq-core/clib/cArray.cmx
- lib/coq-core/clib/cArray.cmti
- lib/coq-core/clib/cArray.cmt
- lib/coq-core/clib/cArray.cmi
- lib/coq-core/boot/util.ml
- lib/coq-core/boot/path.ml
- lib/coq-core/boot/env.mli
- lib/coq-core/boot/env.ml
- lib/coq-core/boot/boot__Util.cmx
- lib/coq-core/boot/boot__Util.cmt
- lib/coq-core/boot/boot__Util.cmi
- lib/coq-core/boot/boot__Path.cmx
- lib/coq-core/boot/boot__Path.cmt
- lib/coq-core/boot/boot__Path.cmi
- lib/coq-core/boot/boot__Env.cmx
- lib/coq-core/boot/boot__Env.cmti
- lib/coq-core/boot/boot__Env.cmt
- lib/coq-core/boot/boot__Env.cmi
- lib/coq-core/boot/boot.ml
- lib/coq-core/boot/boot.cmxs
- lib/coq-core/boot/boot.cmxa
- lib/coq-core/boot/boot.cmx
- lib/coq-core/boot/boot.cmt
- lib/coq-core/boot/boot.cmi
- lib/coq-core/boot/boot.cma
- lib/coq-core/boot/boot.a
- lib/coq-core/META
- doc/coq/coqide-server/README.md
- doc/coq/coqide-server/LICENSE
- doc/coq/coq-core/README.md
- doc/coq/coq-core/LICENSE
- bin/votour
- bin/ocamllibdep
- bin/csdpcert
- bin/coqworkmgr
- bin/coqwc
- bin/coqtop.opt
- bin/coqtop.byte
- bin/coqtop
- bin/coqtacticworker.opt
- bin/coqqueryworker.opt
- bin/coqproofworker.opt
- bin/coqpp
- bin/coqnative
- bin/coqidetop.opt
- bin/coqidetop.byte
- bin/coqdoc
- bin/coqdep
- bin/coqchk
- bin/coqc.byte
- bin/coqc
- bin/coq_makefile
- bin/coq-tex
[NOTE] While removing coq.8.15.0: not removing non-empty directories:
- share/texmf/tex/latex/misc
- lib/coqide-server/protocol
- lib/coqide-server/core
- lib/coq/user-contrib/Ltac2
- lib/coq/theories/ssrmatching
- lib/coq/theories/setoid_ring
- lib/coq/theories/rtauto
- lib/coq/theories/omega
- lib/coq/theories/nsatz
- lib/coq/theories/micromega
- lib/coq/theories/funind
- lib/coq/theories/extraction
- lib/coq/theories/derive
- lib/coq/theories/btauto
- lib/coq/theories/ZArith
- lib/coq/theories/Wellfounded
- lib/coq/theories/Vectors
- lib/coq/theories/Unicode
- lib/coq/theories/Structures
- lib/coq/theories/Strings
- lib/coq/theories/Sorting
- lib/coq/theories/Sets
- lib/coq/theories/Setoids
- lib/coq/theories/Relations
- lib/coq/theories/Reals/Cauchy
- lib/coq/theories/Reals/Abstract
- lib/coq/theories/QArith
- lib/coq/theories/Program
- lib/coq/theories/PArith
- lib/coq/theories/Numbers/Natural/Peano
- lib/coq/theories/Numbers/Natural/Binary
- lib/coq/theories/Numbers/Natural/Abstract
- lib/coq/theories/Numbers/NatInt
- lib/coq/theories/Numbers/Integer/NatPairs
- lib/coq/theories/Numbers/Integer/Binary
- lib/coq/theories/Numbers/Integer/Abstract
- lib/coq/theories/Numbers/Cyclic/ZModulo
- lib/coq/theories/Numbers/Cyclic/Int63
- lib/coq/theories/Numbers/Cyclic/Int31
- lib/coq/theories/Numbers/Cyclic/Abstract
- lib/coq/theories/NArith
- lib/coq/theories/MSets
- lib/coq/theories/Logic
- lib/coq/theories/Lists
- lib/coq/theories/Init
- lib/coq/theories/Floats
- lib/coq/theories/FSets
- lib/coq/theories/Compat
- lib/coq/theories/Classes
- lib/coq/theories/Bool
- lib/coq/theories/Array
- lib/coq/theories/Arith
- lib/coq-core/vm
- lib/coq-core/vernac
- lib/coq-core/toplevel
- lib/coq-core/top_printers
- lib/coq-core/tools/coqdoc
- lib/coq-core/tactics
- lib/coq-core/sysinit
- lib/coq-core/stm
- lib/coq-core/proofs
- lib/coq-core/printing
- lib/coq-core/pretyping
- lib/coq-core/plugins/zify
- lib/coq-core/plugins/tutorial/p3
- lib/coq-core/plugins/tutorial/p2
- lib/coq-core/plugins/tutorial/p1
- lib/coq-core/plugins/tutorial/p0
- lib/coq-core/plugins/tauto
- lib/coq-core/plugins/ssrmatching
- lib/coq-core/plugins/ssreflect
- lib/coq-core/plugins/rtauto
- lib/coq-core/plugins/ring
- lib/coq-core/plugins/number_string_notation
- lib/coq-core/plugins/nsatz
- lib/coq-core/plugins/micromega
- lib/coq-core/plugins/ltac2
- lib/coq-core/plugins/funind
- lib/coq-core/plugins/firstorder
- lib/coq-core/plugins/extraction
- lib/coq-core/plugins/derive
- lib/coq-core/plugins/cc
- lib/coq-core/plugins/btauto
- lib/coq-core/parsing
- lib/coq-core/library
- lib/coq-core/kernel
- lib/coq-core/interp
- lib/coq-core/gramlib
- lib/coq-core/engine
- lib/coq-core/config
- lib/coq-core/clib
- lib/coq-core/boot
- doc/coq/coqide-server
- doc/coq/coq-core
-> removed coq.8.15.0
Done.
# Run eval $(opam env) to update the current shell environment
[ERROR] Sorry, resolution of the request timed out.
Try to specify a simpler request, use a different solver, or increase the allowed time by setting OPAMSOLVERTIMEOUT to a bigger value (currently, it is set to 600.0 seconds).
The middle of the output is truncated (maximum 20000 characters)
truetrueNo files were installed.
true