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
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.9.1 Formal proof management system
num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.06.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.06.1 Official 4.06.1 release
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.5 A library manager for OCaml
# opam file:
opam-version: "2.0"
maintainer: [
"Érik Martin-Dorel <erik.martin-dorel@irit.fr>"
"Pierre Roux <pierre.roux@onera.fr>"
]
homepage: "https://sourcesup.renater.fr/validsdp/"
dev-repo: "git+https://github.com/validsdp/validsdp.git"
bug-reports: "https://github.com/validsdp/validsdp/issues"
license: "LGPL-2.1-or-later"
build: [
["sh" "-c" "./configure"]
[make "-j%{jobs}%"]
]
run-test: [make "-j%{jobs}%" "test"]
install: [make "install"]
depends: [
"ocaml"
"coq" {>= "8.12" & < "8.16~"}
"coq-bignums"
"coq-flocq" {>= "3.3.0"}
"coq-interval" {>= "4.0.0" & < "5~"}
"coq-mathcomp-field" {>= "1.12" & < "1.15~"}
"coq-mathcomp-analysis" {>= "0.3.4" & < "0.4~"}
"coq-libvalidsdp" {= "1.0.0"}
"coq-mathcomp-multinomials" {>= "1.2"}
"coq-coqeal" {>= "1.1.0"}
"coq-paramcoq" {>= "1.1.0"}
"osdp" {>= "1.0"}
"ocamlfind" {build}
"conf-autoconf" {build & dev}
]
synopsis: "ValidSDP"
description: """
ValidSDP is a library for the Coq formal proof assistant. It provides
reflexive tactics to prove multivariate inequalities involving
real-valued variables and rational constants, using SDP solvers as
untrusted back-ends and verified checkers based on libValidSDP.
Once installed, you can import the following modules:
From Coq Require Import Reals.
From ValidSDP Require Import validsdp.
"""
tags: [
"keyword:libValidSDP"
"keyword:ValidSDP"
"keyword:floating-point arithmetic"
"keyword:Cholesky decomposition"
"category:Miscellaneous/Coq Extensions"
"logpath:ValidSDP"
]
authors: [
"Érik Martin-Dorel <erik.martin-dorel@irit.fr>"
"Pierre Roux <pierre.roux@onera.fr>"
]
url {
src: "https://github.com/validsdp/validsdp/releases/download/v1.0.0/validsdp-1.0.0.tar.gz"
checksum: "sha512=94d872eb3ef308cc7c344f3c39e60d5bc265b05bc6c50b2399475e1ac4e105b330b1d63cf4193a04388b7a173f142e246bb6b6c46092fe9c221ed85b1d6b7c3f"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-validsdp.1.0.0 coq.8.9.1[NOTE] Package coq is already installed (current version is 8.9.1).
The following dependencies couldn't be met:
- coq-validsdp -> coq-libvalidsdp = 1.0.0 -> coq >= 8.12 -> ocaml >= 4.09.0
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-validsdp.1.0.0The following actions will be performed:
- remove coq 8.9.1
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[WARNING] While removing coq.8.9.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/vernacinterp.cmx
- lib/coq/vernac/vernacinterp.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/misctypes.cmx
- lib/coq/vernac/misctypes.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/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/coqargs.cmx
- lib/coq/toplevel/coqargs.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/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
- 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
[...] truncated
oq/kernel/byterun/dllcoqrun.so
- lib/coq/interp/syntax_def.cmx
- lib/coq/interp/syntax_def.cmi
- lib/coq/interp/stdarg.cmx
- lib/coq/interp/stdarg.cmi
- lib/coq/interp/smartlocate.cmx
- lib/coq/interp/smartlocate.cmi
- lib/coq/interp/reserve.cmx
- lib/coq/interp/reserve.cmi
- lib/coq/interp/redops.cmx
- lib/coq/interp/redops.cmi
- lib/coq/interp/notation_term.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/genredexpr.cmx
- lib/coq/interp/genredexpr.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/grammar/q_util.cmi
- lib/coq/grammar/grammar.cma
- lib/coq/engine/univops.cmx
- lib/coq/engine/univops.cmi
- lib/coq/engine/universes.cmx
- lib/coq/engine/universes.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/dev/checker_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/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.9.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/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/romega
- lib/coq/plugins/quote
- 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/grammar
- lib/coq/engine
- lib/coq/dev
- lib/coq/coqpp
- lib/coq/config
- lib/coq/clib
-> removed coq.8.9.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)
truetrueNo files were installed.
true