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 coq 8.10.1 Formal proof management system num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.09.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.09.1 Official release 4.09.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.3 A library manager for OCaml # opam file: opam-version: "2.0" maintainer: "Reynald Affeldt <reynald.affeldt@aist.go.jp>" homepage: "https://github.com/affeldt-aist/monae" dev-repo: "git+https://github.com/affeldt-aist/monae.git" bug-reports: "https://github.com/affeldt-aist/monae/issues" license: "LGPL-2.1-or-later" synopsis: "Monads and equational reasoning in Coq" description: """ This Coq library contains a hierarchy of monads with their laws used in several examples of monadic equational reasoning.""" build: [ [make "-j%{jobs}%"] [make "sect5"] [make "-C" "impredicative_set"] ] install: [make "install"] depends: [ "coq" { (>= "8.11" & < "8.13~") | (= "dev") } "coq-mathcomp-ssreflect" { (>= "1.11.0" & < "1.12~") } "coq-mathcomp-fingroup" { (>= "1.11.0" & < "1.12~") } "coq-mathcomp-algebra" { (>= "1.11.0" & < "1.12~") } "coq-mathcomp-solvable" { (>= "1.11.0" & < "1.12~") } "coq-mathcomp-field" { (>= "1.11.0" & < "1.12~") } "coq-mathcomp-analysis" { (= "0.3.4") } "coq-infotheo" { >= "0.2.1" } "coq-paramcoq" { >= "1.1.2" & < "1.2~" } ] tags: [ "keyword:monae" "keyword:effects" "keyword:probability" "keyword:nondeterminism" "logpath:monae" ] authors: [ "Reynald Affeldt" "David Nowak" "Takafumi Saikawa" "Jacques Garrigue" "Celestine Sauvage" "Kazunari Tanaka" ] url { http: "https://github.com/affeldt-aist/monae/archive/0.2.1.tar.gz" checksum: "sha512=64763dadb87bd136ea6594eb5e615ed56d7e4d51d169a2254b9a70c11d1871251fa79b7822df469ec1bdfa2ae1e1530dc93bccb6d0298463901902d7af7bfa0f" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-monae.0.2.1 coq.8.10.1
[NOTE] Package coq is already installed (current version is 8.10.1). The following dependencies couldn't be met: - coq-monae -> coq-mathcomp-analysis = 0.3.4 -> coq >= dev no matching version 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-monae.0.2.1
The following actions will be performed: - remove coq 8.10.1 <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> [WARNING] While removing coq.8.10.1: 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/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/vernac/vernacstate.cmx - lib/coq/vernac/vernacstate.cmi - lib/coq/vernac/vernacprop.cmx - lib/coq/vernac/vernacprop.cmi - lib/coq/vernac/vernacextend.cmx - lib/coq/vernac/vernacextend.cmi - lib/coq/vernac/vernacexpr.cmx - lib/coq/vernac/vernacexpr.cmi - lib/coq/vernac/vernacentries.cmx - lib/coq/vernac/vernacentries.cmi - lib/coq/vernac/vernac.cmxa - lib/coq/vernac/vernac.cma - lib/coq/vernac/vernac.a - lib/coq/vernac/topfmt.cmx - lib/coq/vernac/topfmt.cmi - lib/coq/vernac/search.cmx - lib/coq/vernac/search.cmi - lib/coq/vernac/record.cmx - lib/coq/vernac/record.cmi - lib/coq/vernac/pvernac.cmx - lib/coq/vernac/pvernac.cmi - lib/coq/vernac/proof_using.cmx - lib/coq/vernac/proof_using.cmi - lib/coq/vernac/ppvernac.cmx - lib/coq/vernac/ppvernac.cmi - lib/coq/vernac/obligations.cmx - lib/coq/vernac/obligations.cmi - lib/coq/vernac/mltop.cmx - lib/coq/vernac/mltop.cmi - lib/coq/vernac/metasyntax.cmx - lib/coq/vernac/metasyntax.cmi - lib/coq/vernac/locality.cmx - lib/coq/vernac/locality.cmi - lib/coq/vernac/lemmas.cmx - lib/coq/vernac/lemmas.cmi - lib/coq/vernac/indschemes.cmx - lib/coq/vernac/indschemes.cmi - lib/coq/vernac/himsg.cmx - lib/coq/vernac/himsg.cmi - lib/coq/vernac/g_vernac.cmx - lib/coq/vernac/g_vernac.cmi - lib/coq/vernac/g_proofs.cmx - lib/coq/vernac/g_proofs.cmi - lib/coq/vernac/explainErr.cmx - lib/coq/vernac/explainErr.cmi - lib/coq/vernac/egramml.cmx - lib/coq/vernac/egramml.cmi - lib/coq/vernac/egramcoq.cmx - lib/coq/vernac/egramcoq.cmi - lib/coq/vernac/declareDef.cmx - lib/coq/vernac/declareDef.cmi - lib/coq/vernac/comProgramFixpoint.cmx - lib/coq/vernac/comProgramFixpoint.cmi - lib/coq/vernac/comInductive.cmx - lib/coq/vernac/comInductive.cmi - lib/coq/vernac/comFixpoint.cmx - lib/coq/vernac/comFixpoint.cmi - lib/coq/vernac/comDefinition.cmx - lib/coq/vernac/comDefinition.cmi - lib/coq/vernac/comAssumption.cmx - lib/coq/vernac/comAssumption.cmi - lib/coq/vernac/classes.cmx - lib/coq/vernac/classes.cmi - lib/coq/vernac/class.cmx - lib/coq/vernac/class.cmi - lib/coq/vernac/auto_ind_decl.cmx - lib/coq/vernac/auto_ind_decl.cmi - lib/coq/vernac/attributes.cmx - lib/coq/vernac/attributes.cmi - lib/coq/vernac/assumptions.cmx - lib/coq/vernac/assumptions.cmi - lib/coq/toplevel/workerLoop.cmx - lib/coq/toplevel/workerLoop.cmi - lib/coq/toplevel/vernac.cmx - lib/coq/toplevel/vernac.cmi - lib/coq/toplevel/usage.cmx - lib/coq/toplevel/usage.cmi - lib/coq/toplevel/toplevel.cmxa - lib/coq/toplevel/toplevel.cma - lib/coq/toplevel/toplevel.a - lib/coq/toplevel/g_toplevel.cmx - lib/coq/toplevel/g_toplevel.cmi - lib/coq/toplevel/coqtop.cmx - lib/coq/toplevel/coqtop.cmi - lib/coq/toplevel/coqloop.cmx - lib/coq/toplevel/coqloop.cmi - lib/coq/toplevel/coqinit.cmx - lib/coq/toplevel/coqinit.cmi - lib/coq/toplevel/coqcargs.cmx - lib/coq/toplevel/coqcargs.cmi - lib/coq/toplevel/coqc.cmx - lib/coq/toplevel/coqc.cmi - lib/coq/toplevel/coqargs.cmx - lib/coq/toplevel/coqargs.cmi - lib/coq/toplevel/ccompile.cmx - lib/coq/toplevel/ccompile.cmi - lib/coq/topbin/coqtop_bin.cmx - lib/coq/topbin/coqtacticworker_bin.cmx - lib/coq/topbin/coqqueryworker_bin.cmx - lib/coq/topbin/coqproofworker_bin.cmx - lib/coq/topbin/coqc_bin.cmx - lib/coq/tools/make-one-time-file.py - lib/coq/tools/make-both-time-files.py - lib/coq/tools/make-both-single-timing-files.py - lib/coq/tools/coqdoc/coqdoc.sty - lib/coq/tools/coqdoc/coqdoc.css - lib/coq/tools/TimeFileMaker.py - lib/coq/tools/CoqMakefile.in - 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 [...] truncated cmx - lib/coq/interp/notation_term.cmi - lib/coq/interp/notation_ops.cmx - lib/coq/interp/notation_ops.cmi - lib/coq/interp/notation.cmx - lib/coq/interp/notation.cmi - lib/coq/interp/modintern.cmx - 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.cmx - lib/coq/interp/implicit_quantifiers.cmi - lib/coq/interp/impargs.cmx - lib/coq/interp/impargs.cmi - lib/coq/interp/genintern.cmx - lib/coq/interp/genintern.cmi - lib/coq/interp/dumpglob.cmx - lib/coq/interp/dumpglob.cmi - lib/coq/interp/discharge.cmx - lib/coq/interp/discharge.cmi - lib/coq/interp/declare.cmx - lib/coq/interp/declare.cmi - lib/coq/interp/constrintern.cmx - lib/coq/interp/constrintern.cmi - lib/coq/interp/constrextern.cmx - lib/coq/interp/constrextern.cmi - lib/coq/interp/constrexpr_ops.cmx - lib/coq/interp/constrexpr_ops.cmi - lib/coq/interp/constrexpr.cmx - lib/coq/interp/constrexpr.cmi - lib/coq/gramlib/.pack/gramlib__Ploc.cmx - lib/coq/gramlib/.pack/gramlib__Ploc.cmi - lib/coq/gramlib/.pack/gramlib__Plexing.cmx - lib/coq/gramlib/.pack/gramlib__Plexing.cmi - lib/coq/gramlib/.pack/gramlib__Grammar.cmx - lib/coq/gramlib/.pack/gramlib__Grammar.cmi - lib/coq/gramlib/.pack/gramlib__Gramext.cmx - lib/coq/gramlib/.pack/gramlib__Gramext.cmi - lib/coq/gramlib/.pack/gramlib.cmxa - lib/coq/gramlib/.pack/gramlib.cmx - lib/coq/gramlib/.pack/gramlib.cmi - lib/coq/gramlib/.pack/gramlib.cma - lib/coq/gramlib/.pack/gramlib.a - lib/coq/engine/univops.cmx - lib/coq/engine/univops.cmi - lib/coq/engine/univSubst.cmx - lib/coq/engine/univSubst.cmi - lib/coq/engine/univProblem.cmx - lib/coq/engine/univProblem.cmi - lib/coq/engine/univNames.cmx - lib/coq/engine/univNames.cmi - lib/coq/engine/univMinim.cmx - lib/coq/engine/univMinim.cmi - lib/coq/engine/univGen.cmx - lib/coq/engine/univGen.cmi - lib/coq/engine/uState.cmx - lib/coq/engine/uState.cmi - lib/coq/engine/termops.cmx - lib/coq/engine/termops.cmi - lib/coq/engine/proofview_monad.cmx - lib/coq/engine/proofview_monad.cmi - lib/coq/engine/proofview.cmx - lib/coq/engine/proofview.cmi - lib/coq/engine/nameops.cmx - lib/coq/engine/nameops.cmi - lib/coq/engine/namegen.cmx - lib/coq/engine/namegen.cmi - lib/coq/engine/logic_monad.cmx - lib/coq/engine/logic_monad.cmi - lib/coq/engine/ftactic.cmx - lib/coq/engine/ftactic.cmi - lib/coq/engine/evd.cmx - lib/coq/engine/evd.cmi - lib/coq/engine/evarutil.cmx - lib/coq/engine/evarutil.cmi - lib/coq/engine/evar_kinds.cmx - lib/coq/engine/evar_kinds.cmi - lib/coq/engine/engine.cmxa - lib/coq/engine/engine.cma - lib/coq/engine/engine.a - lib/coq/engine/eConstr.cmx - lib/coq/engine/eConstr.cmi - lib/coq/dllcoqrun.so - lib/coq/dev/top_printers.cmi - lib/coq/coqpp/coqpp_parse.cmi - lib/coq/coqpp/coqpp_ast.cmi - lib/coq/config/coq_config.cmx - lib/coq/config/coq_config.cmi - lib/coq/config/config.cmxa - lib/coq/config/config.cma - lib/coq/config/config.a - lib/coq/clib/unionfind.cmx - lib/coq/clib/unionfind.cmi - lib/coq/clib/unicodetable.cmx - lib/coq/clib/unicodetable.cmi - lib/coq/clib/unicode.cmx - lib/coq/clib/unicode.cmi - lib/coq/clib/trie.cmx - lib/coq/clib/trie.cmi - lib/coq/clib/terminal.cmx - lib/coq/clib/terminal.cmi - lib/coq/clib/store.cmx - lib/coq/clib/store.cmi - lib/coq/clib/segmenttree.cmx - lib/coq/clib/segmenttree.cmi - lib/coq/clib/range.cmx - lib/coq/clib/range.cmi - lib/coq/clib/predicate.cmx - lib/coq/clib/predicate.cmi - lib/coq/clib/orderedType.cmx - lib/coq/clib/orderedType.cmi - lib/coq/clib/option.cmx - lib/coq/clib/option.cmi - lib/coq/clib/monad.cmx - lib/coq/clib/monad.cmi - lib/coq/clib/minisys.cmx - lib/coq/clib/minisys.cmi - lib/coq/clib/int.cmx - lib/coq/clib/int.cmi - lib/coq/clib/iStream.cmx - lib/coq/clib/iStream.cmi - lib/coq/clib/heap.cmx - lib/coq/clib/heap.cmi - lib/coq/clib/hashset.cmx - lib/coq/clib/hashset.cmi - lib/coq/clib/hashcons.cmx - lib/coq/clib/hashcons.cmi - lib/coq/clib/hMap.cmx - lib/coq/clib/hMap.cmi - lib/coq/clib/exninfo.cmx - lib/coq/clib/exninfo.cmi - lib/coq/clib/dyn.cmx - lib/coq/clib/dyn.cmi - lib/coq/clib/diff2.cmx - lib/coq/clib/diff2.cmi - lib/coq/clib/clib.cmxa - lib/coq/clib/clib.cma - lib/coq/clib/clib.a - lib/coq/clib/cUnix.cmx - lib/coq/clib/cUnix.cmi - lib/coq/clib/cThread.cmx - lib/coq/clib/cThread.cmi - lib/coq/clib/cString.cmx - lib/coq/clib/cString.cmi - lib/coq/clib/cStack.cmx - lib/coq/clib/cStack.cmi - lib/coq/clib/cSig.cmi - lib/coq/clib/cSet.cmx - lib/coq/clib/cSet.cmi - lib/coq/clib/cObj.cmx - lib/coq/clib/cObj.cmi - lib/coq/clib/cMap.cmx - lib/coq/clib/cMap.cmi - lib/coq/clib/cList.cmx - lib/coq/clib/cList.cmi - lib/coq/clib/cEphemeron.cmx - lib/coq/clib/cEphemeron.cmi - lib/coq/clib/cArray.cmx - lib/coq/clib/cArray.cmi - lib/coq/clib/bigint.cmx - lib/coq/clib/bigint.cmi - lib/coq/clib/backtrace.cmx - lib/coq/clib/backtrace.cmi - lib/coq/META - bin/coqtop.opt - bin/coqtacticworker.opt - bin/coqtacticworker.byte - bin/coqqueryworker.opt - bin/coqqueryworker.byte - bin/coqproofworker.opt - bin/coqproofworker.byte - bin/coqpp - bin/coqidetop.opt - bin/coqidetop [NOTE] While removing coq.8.10.1: not removing non-empty directories: - share/texmf/tex/latex/misc - lib/coq/vernac - lib/coq/toplevel - lib/coq/topbin - 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/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/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/ssrmatching - lib/coq/plugins/setoid_ring - lib/coq/plugins/rtauto - lib/coq/plugins/omega - lib/coq/plugins/nsatz - lib/coq/plugins/micromega - lib/coq/plugins/ltac - lib/coq/plugins/funind - lib/coq/plugins/firstorder - lib/coq/plugins/extraction - lib/coq/plugins/derive - lib/coq/plugins/cc - lib/coq/plugins/btauto - lib/coq/parsing - lib/coq/library - lib/coq/kernel/byterun - lib/coq/interp - lib/coq/gramlib/.pack - lib/coq/engine - lib/coq/dev - lib/coq/coqpp - lib/coq/config - lib/coq/clib -> removed coq.8.10.1 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