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.2 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.5 A library manager for OCaml # opam file: opam-version: "2.0" maintainer: "Enrico Tassi <enrico.tassi@inria.fr>" authors: [ "Enrico Tassi" ] license: "LGPL-2.1-or-later" homepage: "https://github.com/LPCIC/coq-elpi" bug-reports: "https://github.com/LPCIC/coq-elpi/issues" dev-repo: "git+https://github.com/LPCIC/coq-elpi" build: [ make "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ] install: [ make "install" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ] depends: [ "elpi" {>= "1.11.2" & < "1.12.0~"} "coq" {>= "8.11" & < "8.12~"} ] tags: [ "logpath:elpi" ] synopsis: "Elpi extension language for Coq" description: """ Coq-elpi provides a Coq plugin that embeds ELPI. It also provides a way to embed Coq's terms into λProlog using the Higher-Order Abstract Syntax approach and a way to read terms back. In addition to that it exports to ELPI a set of Coq's primitives, e.g. printing a message, accessing the environment of theorems and data types, defining a new constant and so on. For convenience it also provides a quotation and anti-quotation for Coq's syntax in λProlog. E.g. `{{nat}}` is expanded to the type name of natural numbers, or `{{A -> B}}` to the representation of a product by unfolding the `->` notation. Finally it provides a way to define new vernacular commands and new tactics.""" url { src: "https://github.com/LPCIC/coq-elpi/archive/v1.4.0.tar.gz" checksum: "sha256=13c2034209f728451707b79937f25d800ea87f3be1c80886f9c21b8bf8f3f7c9" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-elpi.1.4.0 coq.8.10.2
[NOTE] Package coq is already installed (current version is 8.10.2). The following dependencies couldn't be met: - coq-elpi -> coq >= 8.11 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-elpi.1.4.0
The following actions will be performed: - remove coq 8.10.2 <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> [WARNING] While removing coq.8.10.2: 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.2: 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.2 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