« Up

validsdp 1.0.0 Black list 🏴‍☠️

Context

# 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
camlp4              4.02+7       Camlp4 is a system for writing extensible parsers for programming languages
conf-findutils      1            Virtual package relying on findutils
conf-which          1            Virtual package relying on which
coq                 8.5.0~camlp4 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: [
  "É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" {< "9~"}
  "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"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-validsdp.1.0.0 coq.8.5.0~camlp4
Return code
5120
Output
[NOTE] Package coq is already installed (current version is 8.5.0~camlp4).
The following dependencies couldn't be met:
  - coq-validsdp -> coq >= 8.12 -> ocaml >= 4.05.0
      base of this switch (use `--unlock-base' to force)
  - coq-validsdp -> coq >= 8.12 -> coq-core -> ocaml >= 4.09.0
      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:

Command
opam remove -y coq; opam install -y --show-action --unlock-base coq-validsdp.1.0.0
Return code
15360
Output
The following actions will be performed:
  - remove coq 8.5.0~camlp4
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[WARNING] While removing coq.8.5.0~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.0~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.0~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)

Install dependencies

Command
true
Return code
0
Duration
0 s

Install 🚀

Command
true
Return code
0
Duration
0 s

Installation size

No files were installed.

Uninstall 🧹

Command
true
Return code
0
Missing removes
none
Wrong removes
none