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.16.0 Formal proof management system dune 3.6.2 Fast, portable, and opinionated build system ocaml 4.10.2 The OCaml compiler (virtual package) ocaml-base-compiler 4.10.2 Official release 4.10.2 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.5 A library manager for OCaml zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers # opam file: opam-version: "2.0" maintainer: "Reynald Affeldt <reynald.affeldt@aist.go.jp>" homepage: "https://github.com/math-comp/analysis" dev-repo: "git+https://github.com/math-comp/analysis.git" bug-reports: "https://github.com/math-comp/analysis/issues" license: "CECILL-C" synopsis: "An analysis library for mathematical components" description: """ This repository contains an experimental library for real analysis for the Coq proof-assistant and using the Mathematical Components library.""" build: [make "-j%{jobs}%" ] install: [make "install"] depends: [ "coq" { (>= "8.11" & < "8.14~") | (= "dev") } "coq-mathcomp-ssreflect" { (>= "1.12.0" & < "1.13~") | (= "dev") } "coq-mathcomp-fingroup" { (>= "1.12.0" & < "1.13~") | (= "dev") } "coq-mathcomp-algebra" { (>= "1.12.0" & < "1.13~") | (= "dev") } "coq-mathcomp-solvable" { (>= "1.12.0" & < "1.13~") | (= "dev") } "coq-mathcomp-field" { (>= "1.12.0" & < "1.13~") | (= "dev") } "coq-mathcomp-finmap" { (>= "1.5.1" & < "1.6~") | (= "dev") } "coq-mathcomp-bigenough" { (>= "1.0.0") } "coq-hierarchy-builder" { >= "0.10.0" | (= "dev") } ] tags: [ "keyword:analysis" "keyword:topology" "keyword:real numbers" "date:2021-06-12" "logpath:mathcomp.analysis" ] authors: [ "Reynald Affeldt" "Cyril Cohen" "Marie Kerjean" "Assia Mahboubi" "Damien Rouhling" "Pierre Roux" "Kazuhiko Sakaguchi" "Pierre-Yves Strub" "Laurent Théry" ] url { http: "https://github.com/math-comp/analysis/archive/0.3.9.tar.gz" checksum: "sha512=150e3f485f21d4b0a8978c36c39e8dcec1a2dc791a3f0aa7a9e89e2d8b438503dcb649301fa4291d7acbbda08cf495181066efd0d1f1d79fd39ae1a24835c948" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-mathcomp-analysis.0.3.9 coq.8.16.0
[NOTE] Package coq is already installed (current version is 8.16.0). The following dependencies couldn't be met: - coq-mathcomp-analysis -> coq (< 8.14~ & = dev) -> ocaml < 4.10 base of this switch (use `--unlock-base' to force) Your request can't be satisfied: - No available version of coq satisfies the constraints 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-mathcomp-analysis.0.3.9
The following actions will be performed: - remove coq 8.16.0 <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> [WARNING] While removing coq.8.16.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 /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/usage.mli - lib/coq-core/boot/usage.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__Usage.cmx - lib/coq-core/boot/boot__Usage.cmti - lib/coq-core/boot/boot__Usage.cmt - lib/coq-core/boot/boot__Usage.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.16.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.16.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)
true
true
No files were installed.
true