« Up

mathcomp-analysis 0.3.9 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.6.2       Fast, portable, and opinionated build system
ocaml               4.10.2      The OCaml compiler (virtual package)
ocaml-base-compiler 4.10.2      Official release 4.10.2
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.9.5       A library manager for OCaml
zarith              1.12        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/math-comp/analysis"
dev-repo: "git+https://github.com/math-comp/analysis.git"
bug-reports: "https://github.com/math-comp/analysis/issues"
license: "CECILL-C"
synopsis: "An analysis library for mathematical components"
description: """
This repository contains an experimental library for real analysis for
the Coq proof-assistant and using the Mathematical Components library."""
build: [make "-j%{jobs}%" ]
install: [make "install"]
depends: [
  "coq" { (>= "8.11" & < "8.14~") | (= "dev") }
  "coq-mathcomp-ssreflect" { (>= "1.12.0" & < "1.13~") | (= "dev") }
  "coq-mathcomp-fingroup" { (>= "1.12.0" & < "1.13~") | (= "dev") }
  "coq-mathcomp-algebra" { (>= "1.12.0" & < "1.13~") | (= "dev") }
  "coq-mathcomp-solvable" { (>= "1.12.0" & < "1.13~") | (= "dev") }
  "coq-mathcomp-field" { (>= "1.12.0" & < "1.13~") | (= "dev") }
  "coq-mathcomp-finmap" { (>= "1.5.1" & < "1.6~") | (= "dev") }
  "coq-mathcomp-bigenough" { (>= "1.0.0") }
  "coq-hierarchy-builder" { >= "0.10.0" | (= "dev") }
]
tags: [
  "keyword:analysis"
  "keyword:topology"
  "keyword:real numbers"
  "date:2021-06-12"
  "logpath:mathcomp.analysis"
]
authors: [
  "Reynald Affeldt"
  "Cyril Cohen"
  "Marie Kerjean"
  "Assia Mahboubi"
  "Damien Rouhling"
  "Pierre Roux"
  "Kazuhiko Sakaguchi"
  "Pierre-Yves Strub"
  "Laurent Théry"
]
url {
  http: "https://github.com/math-comp/analysis/archive/0.3.9.tar.gz"
  checksum: "sha512=150e3f485f21d4b0a8978c36c39e8dcec1a2dc791a3f0aa7a9e89e2d8b438503dcb649301fa4291d7acbbda08cf495181066efd0d1f1d79fd39ae1a24835c948"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-mathcomp-analysis.0.3.9 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-mathcomp-analysis -> coq (< 8.14~ & = dev) -> ocaml < 4.10
      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-mathcomp-analysis.0.3.9
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