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-num base Num library distributed with the OCaml compiler base-threads base base-unix base camlp4 4.04+1 Camlp4 is a system for writing extensible parsers for programming languages conf-findutils 1 Virtual package relying on findutils coq 8.5.2~camlp4 Formal proof management system num 0 The Num library for arbitrary-precision integer and rational arithmetic ocaml 4.04.2 The OCaml compiler (virtual package) ocaml-base-compiler 4.04.2 Official 4.04.2 release ocaml-config 1 OCaml Switch Configuration ocamlbuild 0.14.2 OCamlbuild is a build system with builtin rules to easily build most OCaml projects # opam file: opam-version: "2.0" maintainer: "dev@clarus.me" homepage: "https://github.com/clarus/coq-chick-blog" dev-repo: "git+https://github.com/clarus/coq-chick-blog.git" bug-reports: "https://github.com/clarus/coq-chick-blog/issues" authors: ["Guillaume Claret"] license: "MIT" build: [ ["./configure.sh"] [make "-j%{jobs}%"] [make "-C" "extraction" "-j%{jobs}%"] ] depends: [ "cohttp-lwt-unix" "coq-error-handlers" "coq-function-ninjas" "coq-list-string" "coq-moment" "coq" {< "8.15~"} "lwt" "ocaml" {>= "4.03"} "ocamlfind" {build} ] tags: [ "date:2019-11-26" "keyword:blog" "keyword:effects" "keyword:extraction" ] synopsis: "A blog engine written and proven in Coq" url { src: "https://github.com/clarus/coq-chick-blog/archive/1.0.1.tar.gz" checksum: "sha512=1327eba89ee0b0a21559e624bc478763e5f431f3e9fc6ba272ac3f60a64ac4a921287f4c773eba86cc8ea101fe14601350bfe4063a4870355e215bd6a2e5ce5d" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-chick-blog.1.0.1 coq.8.5.2~camlp4
[NOTE] Package coq is already installed (current version is 8.5.2~camlp4). [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).
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-chick-blog.1.0.1
The following actions will be performed: - remove coq 8.5.2~camlp4 <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> [WARNING] While removing coq.8.5.2~camlp4: not removing files that changed since: - share/emacs/site-lisp/gallina.el - share/emacs/site-lisp/gallina-syntax.el - share/emacs/site-lisp/gallina-db.el - share/emacs/site-lisp/coqdoc.sty - share/emacs/site-lisp/coq-inferior.el - share/emacs/site-lisp/coq-font-lock.el - man/man1/gallina.1 - man/man1/coqwc.1 - man/man1/coqtop.opt.1 - man/man1/coqtop.byte.1 - man/man1/coqtop.1 - man/man1/coqmktop.1 - man/man1/coqide.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/coq/toploop/tacworkertop.cmxs - lib/coq/toploop/tacworkertop.cma - lib/coq/toploop/queryworkertop.cmxs - lib/coq/toploop/queryworkertop.cma - lib/coq/toploop/proofworkertop.cmxs - lib/coq/toploop/proofworkertop.cma - lib/coq/toploop/coqidetop.cmxs - lib/coq/toploop/coqidetop.cma - lib/coq/toplevel/vernacinterp.cmi - lib/coq/toplevel/vernacentries.cmi - lib/coq/toplevel/vernac.cmi - lib/coq/toplevel/usage.cmi - lib/coq/toplevel/toplevel.cmxa - lib/coq/toplevel/toplevel.cma - lib/coq/toplevel/toplevel.a - lib/coq/toplevel/search.cmi - lib/coq/toplevel/record.cmi - lib/coq/toplevel/obligations.cmi - lib/coq/toplevel/mltop.cmi - lib/coq/toplevel/metasyntax.cmi - lib/coq/toplevel/locality.cmi - lib/coq/toplevel/indschemes.cmi - lib/coq/toplevel/ind_tables.cmi - lib/coq/toplevel/himsg.cmi - lib/coq/toplevel/g_obligations.cmi - lib/coq/toplevel/discharge.cmi - lib/coq/toplevel/coqtop.cmi - lib/coq/toplevel/coqloop.cmi - lib/coq/toplevel/coqinit.cmi - lib/coq/toplevel/command.cmi - lib/coq/toplevel/classes.cmi - lib/coq/toplevel/class.cmi - lib/coq/toplevel/cerrors.cmi - lib/coq/toplevel/auto_ind_decl.cmi - lib/coq/toplevel/assumptions.cmi - lib/coq/tools/coqdoc/coqdoc.sty - lib/coq/tools/coqdoc/coqdoc.css - lib/coq/tools/compat5.cmo - lib/coq/theories/ZArith/auxiliary.vo - lib/coq/theories/ZArith/auxiliary.v - lib/coq/theories/ZArith/auxiliary.glob - lib/coq/theories/ZArith/Zwf.vo - lib/coq/theories/ZArith/Zwf.v - lib/coq/theories/ZArith/Zwf.glob - lib/coq/theories/ZArith/Zsqrt_compat.vo - lib/coq/theories/ZArith/Zsqrt_compat.v - lib/coq/theories/ZArith/Zsqrt_compat.glob - lib/coq/theories/ZArith/Zquot.vo - lib/coq/theories/ZArith/Zquot.v - lib/coq/theories/ZArith/Zquot.glob - lib/coq/theories/ZArith/Zpower.vo - lib/coq/theories/ZArith/Zpower.v - lib/coq/theories/ZArith/Zpower.glob - lib/coq/theories/ZArith/Zpow_facts.vo - lib/coq/theories/ZArith/Zpow_facts.v - lib/coq/theories/ZArith/Zpow_facts.glob - lib/coq/theories/ZArith/Zpow_def.vo - lib/coq/theories/ZArith/Zpow_def.v - lib/coq/theories/ZArith/Zpow_def.glob - lib/coq/theories/ZArith/Zpow_alt.vo - lib/coq/theories/ZArith/Zpow_alt.v - lib/coq/theories/ZArith/Zpow_alt.glob - lib/coq/theories/ZArith/Zorder.vo - lib/coq/theories/ZArith/Zorder.v - lib/coq/theories/ZArith/Zorder.glob - lib/coq/theories/ZArith/Znumtheory.vo - lib/coq/theories/ZArith/Znumtheory.v - lib/coq/theories/ZArith/Znumtheory.glob - lib/coq/theories/ZArith/Znat.vo - lib/coq/theories/ZArith/Znat.v - lib/coq/theories/ZArith/Znat.glob - lib/coq/theories/ZArith/Zmisc.vo - lib/coq/theories/ZArith/Zmisc.v - lib/coq/theories/ZArith/Zmisc.glob - lib/coq/theories/ZArith/Zminmax.vo - lib/coq/theories/ZArith/Zminmax.v - lib/coq/theories/ZArith/Zminmax.glob - lib/coq/theories/ZArith/Zmin.vo - lib/coq/theories/ZArith/Zmin.v - lib/coq/theories/ZArith/Zmin.glob - lib/coq/theories/ZArith/Zmax.vo - lib/coq/theories/ZArith/Zmax.v - lib/coq/theories/ZArith/Zmax.glob - lib/coq/theories/ZArith/Zlogarithm.vo - lib/coq/theories/ZArith/Zlogarithm.v - lib/coq/theories/ZArith/Zlogarithm.glob - lib/coq/theories/ZArith/Zhints.vo - lib/coq/theories/ZArith/Zhints.v - lib/coq/theories/ZArith/Zhints.glob - lib/coq/theories/ZArith/Zgcd_alt.vo - lib/coq/theories/ZArith/Zgcd_alt.v - lib/coq/theories/ZArith/Zgcd_alt.glob - lib/coq/theories/ZArith/Zeven.vo - lib/coq/theories/ZArith/Zeven.v - lib/coq/theories/ZArith/Zeven.glob - lib/coq/theories/ZArith/Zeuclid.vo - lib/coq/theories/ZArith/Zeuclid.v - lib/coq/theories/ZArith/Zeuclid.glob - lib/coq/theories/ZArith/Zdiv.vo - lib/coq/theories/ZArith/Zdiv.v - lib/coq/theories/ZArith/Zdiv.glob - lib/coq/theories/ZArith/Zdigits.vo - lib/coq/theories/ZArith/Zdigits.v - lib/coq/theories/ZArith/Zdigits.glob - lib/coq/theories/ZArith/Zcomplements.vo - lib/coq/theories/ZArith/Zcomplements.v - lib/coq/theories/ZArith/Zcomplements.glob - lib/coq/theories/ZArith/Zcompare.vo - lib/coq/theories/ZArith/Zcompare.v - lib/coq/theories/ZArith/Zcompare.glob - lib/coq/theories/ZArith/Zbool.vo - lib/coq/theories/ZArith/Zbool.v - lib/coq/theories/ZArith/Zbool.glob - lib/coq/theories/ZArith/Zabs.vo - lib/coq/theories/ZArith/Zabs.v - lib/coq/theories/ZArith/Zabs.glob - lib/coq/theories/ZArith/ZArith_dec.vo - lib/coq/theories/ZArith/ZArith_dec.v - lib/coq/theories/ZArith/ZArith_dec.glob - lib/coq/theories/ZArith/ZArith_base.vo - lib/coq/theories/ZArith/ZArith_base.v - lib/coq/theories/ZArith/ZArith_base.glob - lib/coq/theories/ZArith/ZArith.vo - lib/coq/theories/ZArith/ZArith.v - lib/coq/theories/ZArith/ZArith.glob - lib/coq/theories/ZArith/Wf_Z.vo - lib/coq/theories/ZArith/Wf_Z.v - lib/coq/theories/ZArith/Wf_Z.glob - lib/coq/theories/ZArith/Int.vo - lib/coq/theories/ZArith/Int.v - lib/coq/theories/ZArith/Int.glob - lib/coq/theories/ZArith/BinIntDef.vo - lib/coq/theories/ZArith/BinIntDef.v - lib/coq/theories/ZArith/BinIntDef.glob - lib/coq/theories/ZArith/BinInt.vo - lib/coq/theories/ZArith/BinInt.v - lib/coq/theories/ZArith/BinInt.glob - lib/coq/theories/Wellfounded/Wellfounded.vo - lib/coq/theories/Wellfounded/Wellfounded.v - lib/coq/theories/Wellfounded/Wellfounded.glob - lib/coq/theories/Wellfounded/Well_Ordering.vo - lib/coq/theories/Wellfounded/Well_Ordering.v - lib/coq/theories/Wellfounded/Well_Ordering.glob - lib/coq/theories/Wellfounded/Union.vo - lib/coq/theories/Wellfounded/Union.v - lib/coq/theories/Wellfounded/Union.glob - lib/coq/theories/Wellfounded/Transitive_Closure.vo - lib/coq/theories/Wellfounded/Transitive_Closure.v - lib/coq/theories/Wellfounded/Transitive_Closure.glob - lib/coq/theories/Wellfounded/Lexicographic_Product.vo - lib/coq/theories/Wellfounded/Lexicographic_Product.v - lib/coq/theories/Wellfounded/Lexicographic_Product.glob - lib/coq/theories/Wellfounded/Lexicographic_Exponentiation.vo - lib/coq/theories/Wellfounded/Lexicographic_Exponentiation.v - lib/coq/theories/Wellfounded/Lexicographic_Exponentiation.glob - lib/coq/theories/Wellfounded/Inverse_Image.vo - lib/coq/theories/Wellfounded/Inverse_Image.v - lib/coq/theories/Wellfounded/Inverse_Image.glob - lib/coq/theories/Wellfounded/Inclusion.vo - lib/coq/theories/Wellfounded/Inclusion.v - lib/coq/theories/Wellfounded/Inclusion.glob - lib/coq/theories/Wellfounded/Disjoint_Union.vo - lib/coq/theories/Wellfounded/Disjoint_Union.v - lib/coq/theories/Wellfounded/Disjoint_Union.glob - lib/coq/theories/Vectors/VectorSpec.vo - lib/coq/theories/Vectors/VectorSpec.v - lib/coq/theories/Vectors/VectorSpec.glob - lib/coq/theories/Vectors/VectorEq.vo - lib/coq/theories/Vectors/VectorEq.v - lib/coq/theories/Vectors/VectorEq.glob - lib/coq/theories/Vectors/VectorDef.vo - lib/coq/theories/Vectors/VectorDef.v - lib/coq/theories/Vectors/VectorDef.glob - lib/coq/theories/Vectors/Vector.vo - lib/coq/theories/Vectors/Vector.v - lib/coq/theories/Vectors/Vector.glob - lib/coq/theories/Vectors/Fin.vo - lib/coq/theories/Vectors/Fin.v - lib/coq/theories/Vectors/Fin.glob - lib/coq/t [...] truncated a - lib/coq/library/library.cmi - lib/coq/library/library.cma - lib/coq/library/library.a - lib/coq/library/libobject.cmi - lib/coq/library/libnames.cmi - lib/coq/library/lib.cmi - lib/coq/library/kindops.cmi - lib/coq/library/keys.cmi - lib/coq/library/impargs.cmi - lib/coq/library/heads.cmi - lib/coq/library/goptions.cmi - lib/coq/library/globnames.cmi - lib/coq/library/global.cmi - lib/coq/library/dischargedhypsmap.cmi - lib/coq/library/decls.cmi - lib/coq/library/declaremods.cmi - lib/coq/library/declare.cmi - lib/coq/libcoqrun.a - lib/coq/lib/xml_printer.cmi - lib/coq/lib/xml_parser.cmi - lib/coq/lib/xml_lexer.cmi - lib/coq/lib/xml_datatype.cmi - lib/coq/lib/util.cmi - lib/coq/lib/unionfind.cmi - lib/coq/lib/unicodetable.cmi - lib/coq/lib/unicode.cmi - lib/coq/lib/trie.cmi - lib/coq/lib/terminal.cmi - lib/coq/lib/system.cmi - lib/coq/lib/store.cmi - lib/coq/lib/stateid.cmi - lib/coq/lib/spawn.cmi - lib/coq/lib/serialize.cmi - lib/coq/lib/segmenttree.cmi - lib/coq/lib/rtree.cmi - lib/coq/lib/richpp.cmi - lib/coq/lib/remoteCounter.cmi - lib/coq/lib/profile.cmi - lib/coq/lib/predicate.cmi - lib/coq/lib/ppstyle.cmi - lib/coq/lib/pp_control.cmi - lib/coq/lib/pp.cmi - lib/coq/lib/option.cmi - lib/coq/lib/monad.cmi - lib/coq/lib/loc.cmi - lib/coq/lib/lib.cmxa - lib/coq/lib/lib.cma - lib/coq/lib/lib.a - lib/coq/lib/int.cmi - lib/coq/lib/iStream.cmi - lib/coq/lib/hook.cmi - lib/coq/lib/heap.cmi - lib/coq/lib/hashset.cmi - lib/coq/lib/hashcons.cmi - lib/coq/lib/hMap.cmi - lib/coq/lib/genarg.cmi - lib/coq/lib/future.cmi - lib/coq/lib/flags.cmi - lib/coq/lib/feedback.cmi - lib/coq/lib/explore.cmi - lib/coq/lib/exninfo.cmi - lib/coq/lib/errors.cmi - lib/coq/lib/envars.cmi - lib/coq/lib/dyn.cmi - lib/coq/lib/deque.cmi - lib/coq/lib/control.cmi - lib/coq/lib/clib.cmxa - lib/coq/lib/clib.cma - lib/coq/lib/clib.a - lib/coq/lib/canary.cmi - lib/coq/lib/cUnix.cmi - lib/coq/lib/cThread.cmi - lib/coq/lib/cString.cmi - lib/coq/lib/cStack.cmi - lib/coq/lib/cSig.cmi - lib/coq/lib/cSet.cmi - lib/coq/lib/cObj.cmi - lib/coq/lib/cMap.cmi - lib/coq/lib/cList.cmi - lib/coq/lib/cEphemeron.cmi - lib/coq/lib/cArray.cmi - lib/coq/lib/bigint.cmi - lib/coq/lib/backtrace.cmi - lib/coq/lib/aux_file.cmi - lib/coq/kernel/vm.cmi - lib/coq/kernel/vconv.cmi - lib/coq/kernel/vars.cmi - lib/coq/kernel/univ.cmi - lib/coq/kernel/uint31.cmi - lib/coq/kernel/typeops.cmi - lib/coq/kernel/type_errors.cmi - lib/coq/kernel/term_typing.cmi - lib/coq/kernel/term.cmi - lib/coq/kernel/subtyping.cmi - lib/coq/kernel/sorts.cmi - lib/coq/kernel/safe_typing.cmi - lib/coq/kernel/retroknowledge.cmi - lib/coq/kernel/reduction.cmi - lib/coq/kernel/primitives.cmi - lib/coq/kernel/pre_env.cmi - lib/coq/kernel/opaqueproof.cmi - lib/coq/kernel/nativevalues.cmi - lib/coq/kernel/nativelibrary.cmi - lib/coq/kernel/nativelib.cmi - lib/coq/kernel/nativelambda.cmi - lib/coq/kernel/nativeinstr.cmi - lib/coq/kernel/nativeconv.cmi - lib/coq/kernel/nativecode.cmi - lib/coq/kernel/names.cmi - lib/coq/kernel/modops.cmi - lib/coq/kernel/mod_typing.cmi - lib/coq/kernel/mod_subst.cmi - lib/coq/kernel/kernel.cmxa - lib/coq/kernel/kernel.cma - lib/coq/kernel/kernel.a - lib/coq/kernel/inductive.cmi - lib/coq/kernel/indtypes.cmi - lib/coq/kernel/fast_typeops.cmi - lib/coq/kernel/evar.cmi - lib/coq/kernel/esubst.cmi - lib/coq/kernel/environ.cmi - lib/coq/kernel/entries.cmi - lib/coq/kernel/declareops.cmi - lib/coq/kernel/declarations.cmi - lib/coq/kernel/csymtable.cmi - lib/coq/kernel/copcodes.cmi - lib/coq/kernel/cooking.cmi - lib/coq/kernel/conv_oracle.cmi - lib/coq/kernel/context.cmi - lib/coq/kernel/constr.cmi - lib/coq/kernel/closure.cmi - lib/coq/kernel/cemitcodes.cmi - lib/coq/kernel/cbytegen.cmi - lib/coq/kernel/cbytecodes.cmi - lib/coq/intf/vernacexpr.cmi - lib/coq/intf/tacexpr.cmi - lib/coq/intf/pattern.cmi - lib/coq/intf/notation_term.cmi - lib/coq/intf/misctypes.cmi - lib/coq/intf/locus.cmi - lib/coq/intf/glob_term.cmi - lib/coq/intf/genredexpr.cmi - lib/coq/intf/extend.cmi - lib/coq/intf/evar_kinds.cmi - lib/coq/intf/decl_kinds.cmi - lib/coq/intf/constrexpr.cmi - lib/coq/interp/topconstr.cmi - lib/coq/interp/syntax_def.cmi - lib/coq/interp/stdarg.cmi - lib/coq/interp/smartlocate.cmi - lib/coq/interp/reserve.cmi - lib/coq/interp/ppextend.cmi - lib/coq/interp/notation_ops.cmi - lib/coq/interp/notation.cmi - lib/coq/interp/modintern.cmi - lib/coq/interp/interp.cmxa - lib/coq/interp/interp.cma - lib/coq/interp/interp.a - lib/coq/interp/implicit_quantifiers.cmi - lib/coq/interp/genintern.cmi - lib/coq/interp/dumpglob.cmi - lib/coq/interp/coqlib.cmi - lib/coq/interp/constrintern.cmi - lib/coq/interp/constrextern.cmi - lib/coq/interp/constrexpr_ops.cmi - lib/coq/interp/constrarg.cmi - lib/coq/grammar/q_util.cmi - lib/coq/grammar/grammar.cma - lib/coq/dllcoqrun.so - lib/coq/config/coq_config.cmi - bin/coqtop.byte [NOTE] While removing coq.8.5.2~camlp4: not removing non-empty directories: - share/emacs/site-lisp - lib/coq/toploop - lib/coq/toplevel - lib/coq/tools/coqdoc - 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 - lib/coq/theories/QArith - lib/coq/theories/Program - lib/coq/theories/PArith - lib/coq/theories/Numbers/Rational/SpecViaQ - lib/coq/theories/Numbers/Rational/BigQ - lib/coq/theories/Numbers/Natural/SpecViaZ - lib/coq/theories/Numbers/Natural/Peano - lib/coq/theories/Numbers/Natural/Binary - lib/coq/theories/Numbers/Natural/BigN - lib/coq/theories/Numbers/Natural/Abstract - lib/coq/theories/Numbers/NatInt - lib/coq/theories/Numbers/Integer/SpecViaZ - lib/coq/theories/Numbers/Integer/NatPairs - lib/coq/theories/Numbers/Integer/Binary - lib/coq/theories/Numbers/Integer/BigZ - lib/coq/theories/Numbers/Integer/Abstract - lib/coq/theories/Numbers/Cyclic/ZModulo - lib/coq/theories/Numbers/Cyclic/Int31 - lib/coq/theories/Numbers/Cyclic/DoubleCyclic - 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/FSets - lib/coq/theories/Compat - lib/coq/theories/Classes - lib/coq/theories/Bool - lib/coq/theories/Arith - lib/coq/tactics - lib/coq/stm - lib/coq/proofs - lib/coq/printing - lib/coq/pretyping - lib/coq/plugins/syntax - lib/coq/plugins/setoid_ring - lib/coq/plugins/rtauto - lib/coq/plugins/romega - lib/coq/plugins/quote - lib/coq/plugins/omega - lib/coq/plugins/nsatz - lib/coq/plugins/micromega - lib/coq/plugins/funind - lib/coq/plugins/fourier - lib/coq/plugins/firstorder - lib/coq/plugins/extraction - lib/coq/plugins/derive - lib/coq/plugins/decl_mode - lib/coq/plugins/cc - lib/coq/plugins/btauto - lib/coq/parsing - lib/coq/library - lib/coq/kernel - lib/coq/intf - lib/coq/interp - lib/coq/grammar - lib/coq/config -> removed coq.8.5.2~camlp4 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