ยซ Up

infotheo 0.3.6 Black list ๐Ÿดโ€โ˜ ๏ธ

Context

# Packages matching: installed
# Name                # Installed # Synopsis
base-bigarray         base
base-threads          base
base-unix             base
conf-findutils        1           Virtual package relying on findutils
conf-gmp              4           Virtual package relying on a GMP lib system installation
coq                   8.16.0      Formal proof management system
dune                  3.13.0      Fast, portable, and opinionated build system
ocaml                 4.13.1      The OCaml compiler (virtual package)
ocaml-base-compiler   4.13.1      Official release 4.13.1
ocaml-config          2           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled
ocamlfind             1.9.6       A library manager for OCaml
zarith                1.13        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "Reynald Affeldt <reynald.affeldt@aist.go.jp>"
homepage: "https://github.com/affeldt-aist/infotheo"
dev-repo: "git+https://github.com/affeldt-aist/infotheo.git"
bug-reports: "https://github.com/affeldt-aist/infotheo/issues"
license: "LGPL-2.1-or-later"
synopsis: "Discrete probabilities and information theory for Coq"
description: """
Infotheo is a Coq library for reasoning about discrete probabilities,
information theory, and linear error-correcting codes."""
build: [
  [make "-j%{jobs}%" ]
  [make "-C" "extraction" "tests"] {with-test}
]
install: [make "install"]
depends: [
  "coq" { (>= "8.13" & < "8.16~") | (= "dev") }
  "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.15~") | (= "dev") }
  "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
  "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
  "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
  "coq-mathcomp-field" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
  "coq-mathcomp-analysis" { (>= "0.3.11") & (< "0.4~")}
]
tags: [
  "keyword:information theory"
  "keyword:probability"
  "keyword:error-correcting codes"
  "keyword:convexity"
  "logpath:infotheo"
  "date:2022-02-14"
]
authors: [
  "Reynald Affeldt, AIST"
  "Manabu Hagiwara, Chiba U. (previously AIST)"
  "Jonas Senizergues, ENS Cachan (internship at AIST)"
  "Jacques Garrigue, Nagoya U."
  "Kazuhiko Sakaguchi, Tsukuba U."
  "Taku Asai, Nagoya U. (M2)"
  "Takafumi Saikawa, Nagoya U."
  "Naruomi Obata, Titech (M2)"
]
url {
  http: "https://github.com/affeldt-aist/infotheo/archive/0.3.6.tar.gz"
  checksum: "sha512=0d6f4105056921186eed87fd6d1de3ce9da4c812d3e5bb5f1e1580ae450802552371ee316993c4c3fa07bbb9ce4b6c8de7aed294b22861abfaeec5a38511549d"
}

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-infotheo.0.3.6 coq.8.16.0
Return code
5120
Output
[NOTE] Package coq is already installed (current version is 8.16.0).
The following dependencies couldn't be met:
  - coq-infotheo -> coq (< 8.16~ & = dev) -> ocaml < 4.12
      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:

Command
opam remove -y coq; opam install -y --show-action --unlock-base coq-infotheo.0.3.6
Return code
15360
Output
The following actions will be performed:
  - remove coq 8.16.0
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[WARNING] While removing coq.8.16.0: 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/coqnative.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/stublibs/dllcoqrun_stubs.so
            - lib/coqide-server/protocol/xmlprotocol.mli
            - lib/coqide-server/protocol/xmlprotocol.ml
            - lib/coqide-server/protocol/xmlprotocol.cmx
            - lib/coqide-server/protocol/xmlprotocol.cmti
            - lib/coqide-server/protocol/xmlprotocol.cmt
            - lib/coqide-server/protocol/xmlprotocol.cmi
            - lib/coqide-server/protocol/xml_printer.mli
            - lib/coqide-server/protocol/xml_printer.ml
            - lib/coqide-server/protocol/xml_printer.cmx
            - lib/coqide-server/protocol/xml_printer.cmti
            - lib/coqide-server/protocol/xml_printer.cmt
            - lib/coqide-server/protocol/xml_printer.cmi
            - lib/coqide-server/protocol/xml_parser.mli
            - lib/coqide-server/protocol/xml_parser.ml
            - lib/coqide-server/protocol/xml_parser.cmx
            - lib/coqide-server/protocol/xml_parser.cmti
            - lib/coqide-server/protocol/xml_parser.cmt
            - lib/coqide-server/protocol/xml_parser.cmi
            - lib/coqide-server/protocol/xml_lexer.mli
            - lib/coqide-server/protocol/xml_lexer.ml
            - lib/coqide-server/protocol/xml_lexer.cmx
            - lib/coqide-server/protocol/xml_lexer.cmti
            - lib/coqide-server/protocol/xml_lexer.cmt
            - lib/coqide-server/protocol/xml_lexer.cmi
            - lib/coqide-server/protocol/serialize.mli
            - lib/coqide-server/protocol/serialize.ml
            - lib/coqide-server/protocol/serialize.cmx
            - lib/coqide-server/protocol/serialize.cmti
            - lib/coqide-server/protocol/serialize.cmt
            - lib/coqide-server/protocol/serialize.cmi
            - lib/coqide-server/protocol/richpp.mli
            - lib/coqide-server/protocol/richpp.ml
            - lib/coqide-server/protocol/richpp.cmx
            - lib/coqide-server/protocol/richpp.cmti
            - lib/coqide-server/protocol/richpp.cmt
            - lib/coqide-server/protocol/richpp.cmi
            - lib/coqide-server/protocol/protocol.cmxs
            - lib/coqide-server/protocol/protocol.cmxa
            - lib/coqide-server/protocol/protocol.cma
            - lib/coqide-server/protocol/protocol.a
            - lib/coqide-server/protocol/interface.ml
            - lib/coqide-server/protocol/interface.cmx
            - lib/coqide-server/protocol/interface.cmt
            - lib/coqide-server/protocol/interface.cmi
            - lib/coqide-server/opam
            - lib/coqide-server/dune-package
            - lib/coqide-server/core/document.mli
            - lib/coqide-server/core/document.ml
            - lib/coqide-server/core/document.cmx
            - lib/coqide-server/core/document.cmti
            - lib/coqide-server/core/document.cmt
            - lib/coqide-server/core/document.cmi
            - lib/coqide-server/core/core.cmxs
            - lib/coqide-server/core/core.cmxa
            - lib/coqide-server/core/core.cma
            - lib/coqide-server/core/core.a
            - lib/coqide-server/META
            - lib/coq/user-contrib/Ltac2/String.vos
            - lib/coq/user-contrib/Ltac2/String.vo
            - lib/coq/user-contrib/Ltac2/String.v
            - lib/coq/user-contrib/Ltac2/String.glob
            - lib/coq/user-contrib/Ltac2/Std.vos
            - lib/coq/user-contrib/Ltac2/Std.vo
            - lib/coq/user-contrib/Ltac2/Std.v
            - lib/coq/user-contrib/Ltac2/Std.glob
            - lib/coq/user-contrib/Ltac2/Printf.vos
            - lib/coq/user-contrib/Ltac2/Printf.vo
            - lib/coq/user-contrib/Ltac2/Printf.v
            - lib/coq/user-contrib/Ltac2/Printf.glob
            - lib/coq/user-contrib/Ltac2/Pattern.vos
            - lib/coq/user-contrib/Ltac2/Pattern.vo
            - lib/coq/user-contrib/Ltac2/Pattern.v
            - lib/coq/user-contrib/Ltac2/Pattern.glob
            - lib/coq/user-contrib/Ltac2/Option.vos
            - lib/coq/user-contrib/Ltac2/Option.vo
            - lib/coq/user-contrib/Ltac2/Option.v
            - lib/coq/user-contrib/Ltac2/Option.glob
            - lib/coq/user-contrib/Ltac2/Notations.vos
            - lib/coq/user-contrib/Ltac2/Notations.vo
            - lib/coq/user-contrib/Ltac2/Notations.v
            - lib/coq/user-contrib/Ltac2/Notations.glob
            - lib/coq/user-contrib/Ltac2/Message.vos
            - lib/coq/user-contrib/Ltac2/Message.vo
            - lib/coq/user-contrib/Ltac2/Message.v
            - lib/coq/user-contrib/Ltac2/Message.glob
            - lib/coq/user-contrib/Ltac2/Ltac2.vos
            - lib/coq/user-contrib/Ltac2/Ltac2.vo
            - lib/coq/user-contrib/Ltac2/Ltac2.v
            - lib/coq/user-contrib/Ltac2/Ltac2.glob
            - lib/coq/user-contrib/Ltac2/Ltac1.vos
            - lib/coq/user-contrib/Ltac2/Ltac1.vo
            - lib/coq/user-contrib/Ltac2/Ltac1.v
            - lib/coq/user-contrib/Ltac2/Ltac1.glob
            - lib/coq/user-contrib/Ltac2/List.vos
            - lib/coq/user-contrib/Ltac2/List.vo
            - lib/coq/user-contrib/Ltac2/List.v
            - lib/coq/user-contrib/Ltac2/List.glob
            - lib/coq/user-contrib/Ltac2/Int.vos
            - lib/coq/user-contrib/Ltac2/Int.vo
            - lib/coq/user-contrib/Ltac2/Int.v
            - lib/coq/user-contrib/Ltac2/Int.glob
            - lib/coq/user-contrib/Ltac2/Init.vos
            - lib/coq/user-contrib/Ltac2/Init.vo
            - lib/coq/user-contrib/Ltac2/Init.v
            - lib/coq/user-contrib/Ltac2/Init.glob
            - lib/coq/user-contrib/Ltac2/Ind.vos
            - lib/coq/user-contrib/Ltac2/Ind.vo
            - lib/coq/user-contrib/Ltac2/Ind.v
            - lib/coq/user-contrib/Ltac2/Ind.glob
            - lib/coq/user-contrib/Ltac2/Ident.vos
            - lib/coq/user-contrib/Ltac2/Ident.vo
            - lib/coq/user-contrib/Ltac2/Ident.v
            - lib/coq/user-contrib/Ltac2/Ident.glob
            - lib/coq/user-contrib/Ltac2/Fresh.vos
            - lib/coq/user-contrib/Ltac2/Fresh.vo
            - lib/coq/user-contrib/Ltac2/Fresh.v
            - lib/coq/user-contrib/Ltac2/Fresh.glob
            - lib/coq/user-contrib/Ltac2/Env.vos
            - lib/coq/user-contrib/Ltac2/Env.vo
            - lib/coq/user-contrib/Ltac2/Env.v
            - lib/coq/user-contrib/Ltac2/Env.glob
            - lib/coq/user-contrib/Ltac2/Control.vos
            - lib/coq/user-contrib/Ltac2/Control.vo
            - lib/coq/user-contrib/Ltac2/Control.v
            - lib/coq/user-contrib/Ltac2/Control.glob
            - lib/coq/user-contrib/Ltac2/Constr.vos
            - lib/coq/user-contrib/Ltac2/Constr.vo
            - lib/coq/user-contrib/Ltac2/Constr.v
            - lib/coq/user-contrib/Ltac2/Constr.glob
            - lib/coq/user-contrib/Ltac2/Char.vos
            - lib/coq/user-contrib/Ltac2/Char.vo
            - lib/coq/user-contrib/Ltac2/Char.v
            - lib/coq/user-contrib/Ltac2/Char.glob
            - lib/coq/user-contrib/Ltac2/Bool.vos
            - lib/coq/user-contrib/Ltac2/Bool.vo
            - lib/coq/user-contrib/Ltac2/Bool.v
            - lib/coq/user-contrib/Ltac2/Bool.glob
            - lib/coq/user-contrib/Ltac2/Array.vos
            - lib/coq/user-contrib/Ltac2/Array.vo
            - lib/coq/user-contrib/Ltac2/Array.v
            - lib/coq/user-contrib/Ltac2/Array.glob
            - lib/coq/theories/ssrmatching/ssrmatching.vos
            - lib/coq/theories/ssrmatching/ssrmatching.vo
            - lib/coq/theories/ssrmatching/ssrmatching.v
            - lib/coq/theories/ssrmatching/ssrmatching.glob
            - lib/coq/theories/ssr/ssrunder.vos
            - lib/coq/theories/ssr/ssrunder.vo
            - lib/coq/theories/ssr/ssrunder.v
            - lib/coq/theories/ssr/ssrunder.glob
            - lib/coq/theories/ssr/ssrsetoid.vos
            - lib/coq/theories/ssr/ssrsetoid.vo
            - lib/coq/theories/ssr/ssrsetoid.v
            - lib/coq/theories/ssr/ssrsetoid.glob
            - lib/coq/theories/ssr/ssrfun.vos
            - lib/coq/theories/ssr/ssrfun.vo
            - lib/coq/theories/ssr/ssrfun.v
            - lib/coq/theories/ssr/ssrfun.glob
            - lib/coq/theories/ssr/ssreflect.vos
            - lib/coq/theories/ssr/ssreflect.vo
            - lib/coq/theories/ssr/ssreflect.v
            - lib/coq/theories/ssr/ssreflect.glob
            - lib/coq/theories/ssr/ssrclasses.vos
            - lib/coq/theories/ssr/ssrclasses.vo
            - lib/coq/theories/ssr/ssrclasses.v
            - lib/coq/theories/ssr/ssrclasses.glob
            - lib/coq/theories/ssr/ssrbool.vos
            - lib/coq/theories/ssr/ssrbool.vo
            - lib/coq/theories/ssr/ssrbool.v
            - lib/coq/theories/ssr/ssrbool.glob
            - lib/coq/theories/setoid_ring/ZArithRing.vos
            - lib/coq/theories/setoid_ring/ZArithRing.vo
            - lib/coq/theories/setoid_ring/ZArithRing.v
            - lib/coq/theories/setoid_ring/ZArithRing.glob
            - lib/coq/theories/setoid_ring/Rings_Z.vos
            - lib/coq/theories/setoid_ring/Rings_Z.vo
            - lib/coq/theories/setoid_ring/Rings_Z.v
            - lib/coq/theories/setoid_ring/Rings_Z.glob
            - lib/coq/theories/setoid_ring/Rings_R.vos
            - lib/coq/theories/setoid_ring/Rings_R.vo
            - lib/coq/theories/setoid_ring/Rings_R.v
            - lib/coq/theories/setoid_ring/Ri
[...] truncated
/coq-core/clib/hashset.cmti
            - lib/coq-core/clib/hashset.cmt
            - lib/coq-core/clib/hashset.cmi
            - lib/coq-core/clib/hashcons.mli
            - lib/coq-core/clib/hashcons.ml
            - lib/coq-core/clib/hashcons.cmx
            - lib/coq-core/clib/hashcons.cmti
            - lib/coq-core/clib/hashcons.cmt
            - lib/coq-core/clib/hashcons.cmi
            - lib/coq-core/clib/hMap.mli
            - lib/coq-core/clib/hMap.ml
            - lib/coq-core/clib/hMap.cmx
            - lib/coq-core/clib/hMap.cmti
            - lib/coq-core/clib/hMap.cmt
            - lib/coq-core/clib/hMap.cmi
            - lib/coq-core/clib/exninfo.mli
            - lib/coq-core/clib/exninfo.ml
            - lib/coq-core/clib/exninfo.cmx
            - lib/coq-core/clib/exninfo.cmti
            - lib/coq-core/clib/exninfo.cmt
            - lib/coq-core/clib/exninfo.cmi
            - lib/coq-core/clib/dyn.mli
            - lib/coq-core/clib/dyn.ml
            - lib/coq-core/clib/dyn.cmx
            - lib/coq-core/clib/dyn.cmti
            - lib/coq-core/clib/dyn.cmt
            - lib/coq-core/clib/dyn.cmi
            - lib/coq-core/clib/diff2.mli
            - lib/coq-core/clib/diff2.ml
            - lib/coq-core/clib/diff2.cmx
            - lib/coq-core/clib/diff2.cmti
            - lib/coq-core/clib/diff2.cmt
            - lib/coq-core/clib/diff2.cmi
            - lib/coq-core/clib/clib.cmxs
            - lib/coq-core/clib/clib.cmxa
            - lib/coq-core/clib/clib.cma
            - lib/coq-core/clib/clib.a
            - lib/coq-core/clib/cUnix.mli
            - lib/coq-core/clib/cUnix.ml
            - lib/coq-core/clib/cUnix.cmx
            - lib/coq-core/clib/cUnix.cmti
            - lib/coq-core/clib/cUnix.cmt
            - lib/coq-core/clib/cUnix.cmi
            - lib/coq-core/clib/cThread.mli
            - lib/coq-core/clib/cThread.ml
            - lib/coq-core/clib/cThread.cmx
            - lib/coq-core/clib/cThread.cmti
            - lib/coq-core/clib/cThread.cmt
            - lib/coq-core/clib/cThread.cmi
            - lib/coq-core/clib/cString.mli
            - lib/coq-core/clib/cString.ml
            - lib/coq-core/clib/cString.cmx
            - lib/coq-core/clib/cString.cmti
            - lib/coq-core/clib/cString.cmt
            - lib/coq-core/clib/cString.cmi
            - lib/coq-core/clib/cSig.mli
            - lib/coq-core/clib/cSig.cmti
            - lib/coq-core/clib/cSig.cmi
            - lib/coq-core/clib/cSet.mli
            - lib/coq-core/clib/cSet.ml
            - lib/coq-core/clib/cSet.cmx
            - lib/coq-core/clib/cSet.cmti
            - lib/coq-core/clib/cSet.cmt
            - lib/coq-core/clib/cSet.cmi
            - lib/coq-core/clib/cObj.mli
            - lib/coq-core/clib/cObj.ml
            - lib/coq-core/clib/cObj.cmx
            - lib/coq-core/clib/cObj.cmti
            - lib/coq-core/clib/cObj.cmt
            - lib/coq-core/clib/cObj.cmi
            - lib/coq-core/clib/cMap.mli
            - lib/coq-core/clib/cMap.ml
            - lib/coq-core/clib/cMap.cmx
            - lib/coq-core/clib/cMap.cmti
            - lib/coq-core/clib/cMap.cmt
            - lib/coq-core/clib/cMap.cmi
            - lib/coq-core/clib/cList.mli
            - lib/coq-core/clib/cList.ml
            - lib/coq-core/clib/cList.cmx
            - lib/coq-core/clib/cList.cmti
            - lib/coq-core/clib/cList.cmt
            - lib/coq-core/clib/cList.cmi
            - lib/coq-core/clib/cEphemeron.mli
            - lib/coq-core/clib/cEphemeron.ml
            - lib/coq-core/clib/cEphemeron.cmx
            - lib/coq-core/clib/cEphemeron.cmti
            - lib/coq-core/clib/cEphemeron.cmt
            - lib/coq-core/clib/cEphemeron.cmi
            - lib/coq-core/clib/cArray.mli
            - lib/coq-core/clib/cArray.ml
            - lib/coq-core/clib/cArray.cmx
            - lib/coq-core/clib/cArray.cmti
            - lib/coq-core/clib/cArray.cmt
            - lib/coq-core/clib/cArray.cmi
            - lib/coq-core/boot/util.ml
            - lib/coq-core/boot/usage.mli
            - lib/coq-core/boot/usage.ml
            - lib/coq-core/boot/path.ml
            - lib/coq-core/boot/env.mli
            - lib/coq-core/boot/env.ml
            - lib/coq-core/boot/boot__Util.cmx
            - lib/coq-core/boot/boot__Util.cmt
            - lib/coq-core/boot/boot__Util.cmi
            - lib/coq-core/boot/boot__Usage.cmx
            - lib/coq-core/boot/boot__Usage.cmti
            - lib/coq-core/boot/boot__Usage.cmt
            - lib/coq-core/boot/boot__Usage.cmi
            - lib/coq-core/boot/boot__Path.cmx
            - lib/coq-core/boot/boot__Path.cmt
            - lib/coq-core/boot/boot__Path.cmi
            - lib/coq-core/boot/boot__Env.cmx
            - lib/coq-core/boot/boot__Env.cmti
            - lib/coq-core/boot/boot__Env.cmt
            - lib/coq-core/boot/boot__Env.cmi
            - lib/coq-core/boot/boot.ml
            - lib/coq-core/boot/boot.cmxs
            - lib/coq-core/boot/boot.cmxa
            - lib/coq-core/boot/boot.cmx
            - lib/coq-core/boot/boot.cmt
            - lib/coq-core/boot/boot.cmi
            - lib/coq-core/boot/boot.cma
            - lib/coq-core/boot/boot.a
            - lib/coq-core/META
            - doc/coq/coqide-server/README.md
            - doc/coq/coqide-server/LICENSE
            - doc/coq/coq-core/README.md
            - doc/coq/coq-core/LICENSE
            - bin/votour
            - bin/ocamllibdep
            - bin/csdpcert
            - bin/coqworkmgr
            - bin/coqwc
            - bin/coqtop.opt
            - bin/coqtop.byte
            - bin/coqtop
            - bin/coqtacticworker.opt
            - bin/coqqueryworker.opt
            - bin/coqproofworker.opt
            - bin/coqpp
            - bin/coqnative
            - bin/coqidetop.opt
            - bin/coqidetop.byte
            - bin/coqdoc
            - bin/coqdep
            - bin/coqchk
            - bin/coqc.byte
            - bin/coqc
            - bin/coq_makefile
            - bin/coq-tex
[NOTE] While removing coq.8.16.0: not removing non-empty directories:
         - share/texmf/tex/latex/misc
         - lib/coqide-server/protocol
         - lib/coqide-server/core
         - lib/coq/user-contrib/Ltac2
         - lib/coq/theories/ssrmatching
         - lib/coq/theories/setoid_ring
         - lib/coq/theories/rtauto
         - lib/coq/theories/omega
         - lib/coq/theories/nsatz
         - lib/coq/theories/micromega
         - lib/coq/theories/funind
         - lib/coq/theories/extraction
         - lib/coq/theories/derive
         - lib/coq/theories/btauto
         - 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/Cauchy
         - lib/coq/theories/Reals/Abstract
         - 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/Floats
         - lib/coq/theories/FSets
         - lib/coq/theories/Compat
         - lib/coq/theories/Classes
         - lib/coq/theories/Bool
         - lib/coq/theories/Array
         - lib/coq/theories/Arith
         - lib/coq-core/vm
         - lib/coq-core/vernac
         - lib/coq-core/toplevel
         - lib/coq-core/top_printers
         - lib/coq-core/tools/coqdoc
         - lib/coq-core/tactics
         - lib/coq-core/sysinit
         - lib/coq-core/stm
         - lib/coq-core/proofs
         - lib/coq-core/printing
         - lib/coq-core/pretyping
         - lib/coq-core/plugins/zify
         - lib/coq-core/plugins/tutorial/p3
         - lib/coq-core/plugins/tutorial/p2
         - lib/coq-core/plugins/tutorial/p1
         - lib/coq-core/plugins/tutorial/p0
         - lib/coq-core/plugins/tauto
         - lib/coq-core/plugins/ssrmatching
         - lib/coq-core/plugins/ssreflect
         - lib/coq-core/plugins/rtauto
         - lib/coq-core/plugins/ring
         - lib/coq-core/plugins/number_string_notation
         - lib/coq-core/plugins/nsatz
         - lib/coq-core/plugins/micromega
         - lib/coq-core/plugins/ltac2
         - lib/coq-core/plugins/funind
         - lib/coq-core/plugins/firstorder
         - lib/coq-core/plugins/extraction
         - lib/coq-core/plugins/derive
         - lib/coq-core/plugins/cc
         - lib/coq-core/plugins/btauto
         - lib/coq-core/parsing
         - lib/coq-core/library
         - lib/coq-core/kernel
         - lib/coq-core/interp
         - lib/coq-core/gramlib
         - lib/coq-core/engine
         - lib/coq-core/config
         - lib/coq-core/clib
         - lib/coq-core/boot
         - doc/coq/coqide-server
         - doc/coq/coq-core
-> removed   coq.8.16.0
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