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-ocamlbuild base OCamlbuild binary and libraries distributed with the OCaml compiler base-threads base base-unix base camlp5 7.14 Preprocessor-pretty-printer of OCaml conf-findutils 1 Virtual package relying on findutils conf-perl 2 Virtual package relying on perl coq 8.4.5 Formal proof management system. num 0 The Num library for arbitrary-precision integer and rational arithmetic ocaml 4.02.3 The OCaml compiler (virtual package) ocaml-base-compiler 4.02.3 Official 4.02.3 release ocaml-config 1 OCaml Switch Configuration ocamlbuild 0 Build system distributed with the OCaml compiler since OCaml 3.10.0 # 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.9~"} "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.0.tar.gz" checksum: "sha512=f54224caafc490f01896ff1fa1e6e9c71ff91ca5bf04fe00f4761dbd9e32758628f6be045b56f4a466574c05ae98edaf41931a1851ae59b8ab0686d83bb28036" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-chick-blog.1.0.0 coq.8.4.5
[NOTE] Package coq is already installed (current version is 8.4.5). The following dependencies couldn't be met: - coq-chick-blog -> ocaml >= 4.03 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-chick-blog.1.0.0
The following actions will be performed: - remove coq 8.4.5 <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> [WARNING] While removing coq.8.4.5: not removing files that changed since: - share/emacs/site-lisp/coqdoc.sty - share/emacs/site-lisp/coq.el - share/emacs/site-lisp/coq-syntax.el - share/emacs/site-lisp/coq-inferior.el - share/emacs/site-lisp/coq-font-lock.el - share/emacs/site-lisp/coq-db.el - share/coq/coq.png - 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/toplevel/whelp.cmi - lib/coq/toplevel/vernacinterp.cmi - lib/coq/toplevel/vernacexpr.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.cmi - lib/coq/toplevel/toplevel.cma - lib/coq/toplevel/toplevel.a - lib/coq/toplevel/search.cmi - lib/coq/toplevel/record.cmi - lib/coq/toplevel/mltop.cmi - lib/coq/toplevel/metasyntax.cmi - lib/coq/toplevel/libtypes.cmi - lib/coq/toplevel/lemmas.cmi - lib/coq/toplevel/interface.cmi - lib/coq/toplevel/indschemes.cmi - lib/coq/toplevel/ind_tables.cmi - lib/coq/toplevel/ide_slave.cmi - lib/coq/toplevel/ide_intf.cmi - lib/coq/toplevel/himsg.cmi - lib/coq/toplevel/discharge.cmi - lib/coq/toplevel/coqtop.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/backtrack.cmi - lib/coq/toplevel/autoinstance.cmi - lib/coq/toplevel/auto_ind_decl.cmi - lib/coq/tools/coqdoc/coqdoc.sty - lib/coq/tools/coqdoc/coqdoc.css - lib/coq/theories/ZArith/auxiliary.vo - lib/coq/theories/ZArith/Zwf.vo - lib/coq/theories/ZArith/Zsqrt_compat.vo - lib/coq/theories/ZArith/Zquot.vo - lib/coq/theories/ZArith/Zpower.vo - lib/coq/theories/ZArith/Zpow_facts.vo - lib/coq/theories/ZArith/Zpow_def.vo - lib/coq/theories/ZArith/Zpow_alt.vo - lib/coq/theories/ZArith/Zorder.vo - lib/coq/theories/ZArith/Znumtheory.vo - lib/coq/theories/ZArith/Znat.vo - lib/coq/theories/ZArith/Zmisc.vo - lib/coq/theories/ZArith/Zminmax.vo - lib/coq/theories/ZArith/Zmin.vo - lib/coq/theories/ZArith/Zmax.vo - lib/coq/theories/ZArith/Zlogarithm.vo - lib/coq/theories/ZArith/Zhints.vo - lib/coq/theories/ZArith/Zgcd_alt.vo - lib/coq/theories/ZArith/Zeven.vo - lib/coq/theories/ZArith/Zeuclid.vo - lib/coq/theories/ZArith/Zdiv.vo - lib/coq/theories/ZArith/Zdigits.vo - lib/coq/theories/ZArith/Zcomplements.vo - lib/coq/theories/ZArith/Zcompare.vo - lib/coq/theories/ZArith/Zbool.vo - lib/coq/theories/ZArith/Zabs.vo - lib/coq/theories/ZArith/ZOdiv_def.vo - lib/coq/theories/ZArith/ZOdiv.vo - lib/coq/theories/ZArith/ZArith_dec.vo - lib/coq/theories/ZArith/ZArith_base.vo - lib/coq/theories/ZArith/ZArith.vo - lib/coq/theories/ZArith/Wf_Z.vo - lib/coq/theories/ZArith/Int.vo - lib/coq/theories/ZArith/BinIntDef.vo - lib/coq/theories/ZArith/BinInt.vo - lib/coq/theories/Wellfounded/Wellfounded.vo - lib/coq/theories/Wellfounded/Well_Ordering.vo - lib/coq/theories/Wellfounded/Union.vo - lib/coq/theories/Wellfounded/Transitive_Closure.vo - lib/coq/theories/Wellfounded/Lexicographic_Product.vo - lib/coq/theories/Wellfounded/Lexicographic_Exponentiation.vo - lib/coq/theories/Wellfounded/Inverse_Image.vo - lib/coq/theories/Wellfounded/Inclusion.vo - lib/coq/theories/Wellfounded/Disjoint_Union.vo - lib/coq/theories/Vectors/VectorSpec.vo - lib/coq/theories/Vectors/VectorDef.vo - lib/coq/theories/Vectors/Vector.vo - lib/coq/theories/Vectors/Fin.vo - lib/coq/theories/Unicode/Utf8_core.vo - lib/coq/theories/Unicode/Utf8.vo - lib/coq/theories/Structures/OrdersTac.vo - lib/coq/theories/Structures/OrdersLists.vo - lib/coq/theories/Structures/OrdersFacts.vo - lib/coq/theories/Structures/OrdersEx.vo - lib/coq/theories/Structures/OrdersAlt.vo - lib/coq/theories/Structures/Orders.vo - lib/coq/theories/Structures/OrderedTypeEx.vo - lib/coq/theories/Structures/OrderedTypeAlt.vo - lib/coq/theories/Structures/OrderedType.vo - lib/coq/theories/Structures/GenericMinMax.vo - lib/coq/theories/Structures/EqualitiesFacts.vo - lib/coq/theories/Structures/Equalities.vo - lib/coq/theories/Structures/DecidableTypeEx.vo - lib/coq/theories/Structures/DecidableType.vo - lib/coq/theories/Strings/String.vo - lib/coq/theories/Strings/Ascii.vo - lib/coq/theories/Sorting/Sorting.vo - lib/coq/theories/Sorting/Sorted.vo - lib/coq/theories/Sorting/Permutation.vo - lib/coq/theories/Sorting/PermutSetoid.vo - lib/coq/theories/Sorting/PermutEq.vo - lib/coq/theories/Sorting/Mergesort.vo - lib/coq/theories/Sorting/Heap.vo - lib/coq/theories/Sets/Uniset.vo - lib/coq/theories/Sets/Relations_3_facts.vo - lib/coq/theories/Sets/Relations_3.vo - lib/coq/theories/Sets/Relations_2_facts.vo - lib/coq/theories/Sets/Relations_2.vo - lib/coq/theories/Sets/Relations_1_facts.vo - lib/coq/theories/Sets/Relations_1.vo - lib/coq/theories/Sets/Powerset_facts.vo - lib/coq/theories/Sets/Powerset_Classical_facts.vo - lib/coq/theories/Sets/Powerset.vo - lib/coq/theories/Sets/Permut.vo - lib/coq/theories/Sets/Partial_Order.vo - lib/coq/theories/Sets/Multiset.vo - lib/coq/theories/Sets/Integers.vo - lib/coq/theories/Sets/Infinite_sets.vo - lib/coq/theories/Sets/Image.vo - lib/coq/theories/Sets/Finite_sets_facts.vo - lib/coq/theories/Sets/Finite_sets.vo - lib/coq/theories/Sets/Ensembles.vo - lib/coq/theories/Sets/Cpo.vo - lib/coq/theories/Sets/Constructive_sets.vo - lib/coq/theories/Sets/Classical_sets.vo - lib/coq/theories/Setoids/Setoid.vo - lib/coq/theories/Relations/Relations.vo - lib/coq/theories/Relations/Relation_Operators.vo - lib/coq/theories/Relations/Relation_Definitions.vo - lib/coq/theories/Relations/Operators_Properties.vo - lib/coq/theories/Reals/Sqrt_reg.vo - lib/coq/theories/Reals/SplitRmult.vo - lib/coq/theories/Reals/SplitAbsolu.vo - lib/coq/theories/Reals/SeqSeries.vo - lib/coq/theories/Reals/SeqProp.vo - lib/coq/theories/Reals/Rtrigo_reg.vo - lib/coq/theories/Reals/Rtrigo_fun.vo - lib/coq/theories/Reals/Rtrigo_def.vo - lib/coq/theories/Reals/Rtrigo_calc.vo - lib/coq/theories/Reals/Rtrigo_alt.vo - lib/coq/theories/Reals/Rtrigo1.vo - lib/coq/theories/Reals/Rtrigo.vo - lib/coq/theories/Reals/Rtopology.vo - lib/coq/theories/Reals/Rsqrt_def.vo - lib/coq/theories/Reals/Rsigma.vo - lib/coq/theories/Reals/Rseries.vo - lib/coq/theories/Reals/Rprod.vo - lib/coq/theories/Reals/Rpower.vo - lib/coq/theories/Reals/Rpow_def.vo - lib/coq/theories/Reals/Rminmax.vo - lib/coq/theories/Reals/Rlogic.vo - lib/coq/theories/Reals/Rlimit.vo - lib/coq/theories/Reals/RiemannInt_SF.vo - lib/coq/theories/Reals/RiemannInt.vo - lib/coq/theories/Reals/Rgeom.vo - lib/coq/theories/Reals/Rfunctions.vo - lib/coq/theories/Reals/Reals.vo - lib/coq/theories/Reals/Rderiv.vo - lib/coq/theories/Reals/Rdefinitions.vo - lib/coq/theories/Reals/Rcomplete.vo - lib/coq/theories/Reals/Rbasic_fun.vo - lib/coq/theories/Reals/Rbase.vo - lib/coq/theories/Reals/Raxioms.vo - lib/coq/theories/Reals/Ratan.vo - lib/coq/theories/Reals/Ranalysis_reg.vo - lib/coq/theories/Reals/Ranalysis5.vo - lib/coq/theories/Reals/Ranalysis4.vo - lib/coq/theories/Reals/Ranalysis3.vo - lib/coq/theories/Reals/Ranalysis2.vo - lib/coq/theories/Reals/Ranalysis1.vo - lib/coq/theories/Reals/Ranalysis.vo - lib/coq/theories/Reals/R_sqrt.vo - lib/coq/theories/Reals/R_sqr.vo - lib/coq/theories/Reals/R_Ifp.vo - lib/coq/theories/Reals/ROrderedType.vo - lib/coq/theories/Reals/RList.vo [...] truncated t.vo - lib/coq/plugins/extraction/ExtrOcamlIntConv.vo - lib/coq/plugins/extraction/ExtrOcamlBigIntConv.vo - lib/coq/plugins/extraction/ExtrOcamlBasic.vo - lib/coq/plugins/decl_mode/ppdecl_proof.cmi - lib/coq/plugins/decl_mode/g_decl_mode.cmi - lib/coq/plugins/decl_mode/decl_proof_instr.cmi - lib/coq/plugins/decl_mode/decl_mode_plugin_mod.cmi - lib/coq/plugins/decl_mode/decl_mode_plugin.cmxs - lib/coq/plugins/decl_mode/decl_mode_plugin.cma - lib/coq/plugins/decl_mode/decl_mode.cmi - lib/coq/plugins/decl_mode/decl_interp.cmi - lib/coq/plugins/decl_mode/decl_expr.cmi - lib/coq/plugins/cc/g_congruence.cmi - lib/coq/plugins/cc/cctac.cmi - lib/coq/plugins/cc/ccproof.cmi - lib/coq/plugins/cc/ccalgo.cmi - lib/coq/plugins/cc/cc_plugin_mod.cmi - lib/coq/plugins/cc/cc_plugin.cmxs - lib/coq/plugins/cc/cc_plugin.cma - lib/coq/parsing/tok.cmi - lib/coq/parsing/tactic_printer.cmi - lib/coq/parsing/q_util.cmi - lib/coq/parsing/printmod.cmi - lib/coq/parsing/printer.cmi - lib/coq/parsing/prettyp.cmi - lib/coq/parsing/ppvernac.cmi - lib/coq/parsing/pptactic.cmi - lib/coq/parsing/ppconstr.cmi - lib/coq/parsing/pcoq.cmi - lib/coq/parsing/parsing.cmxa - lib/coq/parsing/parsing.cma - lib/coq/parsing/parsing.a - lib/coq/parsing/lexer.cmi - lib/coq/parsing/highparsing.cmxa - lib/coq/parsing/highparsing.cma - lib/coq/parsing/highparsing.a - lib/coq/parsing/grammar.cma - lib/coq/parsing/g_xml.cmi - lib/coq/parsing/g_vernac.cmi - lib/coq/parsing/g_tactic.cmi - lib/coq/parsing/g_proofs.cmi - lib/coq/parsing/g_prim.cmi - lib/coq/parsing/g_ltac.cmi - lib/coq/parsing/g_constr.cmi - lib/coq/parsing/extrawit.cmi - lib/coq/parsing/extend.cmi - lib/coq/parsing/egrammar.cmi - lib/coq/library/summary.cmi - lib/coq/library/states.cmi - lib/coq/library/nametab.cmi - lib/coq/library/nameops.cmi - lib/coq/library/library.cmxa - 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/impargs.cmi - lib/coq/library/heads.cmi - lib/coq/library/goptionstyp.cmi - lib/coq/library/goptions.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/library/decl_kinds.cmi - lib/coq/library/assumptions.cmi - lib/coq/libcoqrun.a - lib/coq/lib/xml_utils.cmi - lib/coq/lib/xml_parser.cmi - lib/coq/lib/xml_lexer.cmi - lib/coq/lib/util.cmi - lib/coq/lib/unionfind.cmi - lib/coq/lib/unicodetable.cmi - lib/coq/lib/tries.cmi - lib/coq/lib/system.cmi - lib/coq/lib/store.cmi - lib/coq/lib/segmenttree.cmi - lib/coq/lib/rtree.cmi - lib/coq/lib/profile.cmi - lib/coq/lib/predicate.cmi - lib/coq/lib/pp_control.cmi - lib/coq/lib/pp.cmi - lib/coq/lib/option.cmi - lib/coq/lib/lib.cmxa - lib/coq/lib/lib.cma - lib/coq/lib/lib.a - lib/coq/lib/heap.cmi - lib/coq/lib/hashtbl_alt.cmi - lib/coq/lib/hashcons.cmi - lib/coq/lib/gmapl.cmi - lib/coq/lib/gmap.cmi - lib/coq/lib/fset.cmi - lib/coq/lib/fmap.cmi - lib/coq/lib/flags.cmi - lib/coq/lib/explore.cmi - lib/coq/lib/errors.cmi - lib/coq/lib/envars.cmi - lib/coq/lib/dyn.cmi - lib/coq/lib/dnet.cmi - lib/coq/lib/compat.cmi - lib/coq/lib/bigint.cmi - lib/coq/kernel/vm.cmi - lib/coq/kernel/vconv.cmi - lib/coq/kernel/univ.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/sign.cmi - lib/coq/kernel/safe_typing.cmi - lib/coq/kernel/retroknowledge.cmi - lib/coq/kernel/reduction.cmi - lib/coq/kernel/pre_env.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/esubst.cmi - lib/coq/kernel/environ.cmi - lib/coq/kernel/entries.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/closure.cmi - lib/coq/kernel/cemitcodes.cmi - lib/coq/kernel/cbytegen.cmi - lib/coq/kernel/cbytecodes.cmi - lib/coq/interp/topconstr.cmi - lib/coq/interp/syntax_def.cmi - lib/coq/interp/smartlocate.cmi - lib/coq/interp/reserve.cmi - lib/coq/interp/ppextend.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/genarg.cmi - lib/coq/interp/dumpglob.cmi - lib/coq/interp/coqlib.cmi - lib/coq/interp/constrintern.cmi - lib/coq/interp/constrextern.cmi - lib/coq/dllcoqrun.so - lib/coq/config/coqide-gtk2rc - lib/coq/config/coq_config.o - lib/coq/config/coq_config.cmx - lib/coq/config/coq_config.cmo - lib/coq/config/coq_config.cmi - doc/FAQ-CoqIde - bin/coqtop.opt - bin/coqtop.byte - bin/coqchk.opt [NOTE] While removing coq.8.4.5: not removing non-empty directories: - share/emacs/site-lisp - share/coq - 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/Classes - lib/coq/theories/Bool - lib/coq/theories/Arith - lib/coq/tactics - lib/coq/states - lib/coq/proofs - lib/coq/pretyping - lib/coq/plugins/xml - lib/coq/plugins/syntax - lib/coq/plugins/subtac - lib/coq/plugins/setoid_ring - lib/coq/plugins/rtauto - lib/coq/plugins/romega - lib/coq/plugins/ring - 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/field - lib/coq/plugins/extraction - lib/coq/plugins/decl_mode - lib/coq/plugins/cc - lib/coq/parsing - lib/coq/library - lib/coq/kernel - lib/coq/interp - lib/coq/config -> removed coq.8.4.5 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