ยซ Up

mathcomp-analysis 0.3.8 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.13.1      Formal proof management system
num                   1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
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/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-01"
  "logpath:mathcomp.analysis"
]
authors: [
  "Reynald Affeldt"
  "Cyril Cohen"
  "Marie Kerjean"
  "Assia Mahboubi"
  "Damien Rouhling"
  "Pierre Roux"
  "Kazuhiko Sakaguchi"
  "Pierre-Yves Strub"
  "Laurent Thery"
]
url {
  http: "https://github.com/math-comp/analysis/archive/0.3.8.tar.gz"
  checksum: "sha512=765067b9cd5ed899e92f693040a3fcb279d21bdb3bdad4b5810d31ce3b30e164369b56825691a7fb7c035969e9895e9552b515e7c37fc38349c2713a5f0ef28b"
}

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.8 coq.8.13.1
Return code
5120
Output
[NOTE] Package coq is already installed (current version is 8.13.1).
The following dependencies couldn't be met:
  - coq-mathcomp-analysis -> coq-hierarchy-builder >= dev -> coq-elpi (< 1.9~ | >= dev) -> coq (< 8.13~ | >= 8.15) -> ocaml < 4.12
      base of this switch (use `--unlock-base' to force)
  - coq-mathcomp-analysis -> coq-hierarchy-builder >= dev -> coq-elpi (< 1.9~ | >= dev) -> elpi < 1.14.0~ -> ppx_tools_versioned < 5.2.1 -> ocaml < 4.08.0
      base of this switch (use `--unlock-base' to force)
  - coq-mathcomp-analysis -> coq-hierarchy-builder >= dev -> coq-elpi (< 1.9~ | >= dev) -> elpi < 1.14.0~ -> ocaml-migrate-parsetree < 2.0.0 -> ocaml < 4.13
      base of this switch (use `--unlock-base' to force)
  - coq-mathcomp-analysis -> coq-hierarchy-builder >= dev -> coq-elpi (< 1.9~ | >= dev) -> elpi < 1.14.0~ -> camlp5 < 8.00~alpha01 -> ocaml < 4.13.0
      base of this switch (use `--unlock-base' to force)
  - coq-mathcomp-analysis -> coq-hierarchy-builder >= dev -> coq-elpi (< 1.9~ | >= 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-mathcomp-analysis.0.3.8
Return code
15360
Output
The following actions will be performed:
  - remove coq 8.13.1
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[WARNING] While removing coq.8.13.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/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/retrieveObl.cmx
            - lib/coq/vernac/retrieveObl.cmi
            - lib/coq/vernac/record.cmx
            - lib/coq/vernac/record.cmi
            - lib/coq/vernac/recLemmas.cmx
            - lib/coq/vernac/recLemmas.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/printmod.cmx
            - lib/coq/vernac/printmod.cmi
            - lib/coq/vernac/prettyp.cmx
            - lib/coq/vernac/prettyp.cmi
            - lib/coq/vernac/ppvernac.cmx
            - lib/coq/vernac/ppvernac.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/loadpath.cmx
            - lib/coq/vernac/loadpath.cmi
            - lib/coq/vernac/library.cmx
            - lib/coq/vernac/library.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/egramml.cmx
            - lib/coq/vernac/egramml.cmi
            - lib/coq/vernac/egramcoq.cmx
            - lib/coq/vernac/egramcoq.cmi
            - lib/coq/vernac/declaremods.cmx
            - lib/coq/vernac/declaremods.cmi
            - lib/coq/vernac/declareUniv.cmx
            - lib/coq/vernac/declareUniv.cmi
            - lib/coq/vernac/declareInd.cmx
            - lib/coq/vernac/declareInd.cmi
            - lib/coq/vernac/declare.cmx
            - lib/coq/vernac/declare.cmi
            - lib/coq/vernac/comTactic.cmx
            - lib/coq/vernac/comTactic.cmi
            - lib/coq/vernac/comSearch.cmx
            - lib/coq/vernac/comSearch.cmi
            - lib/coq/vernac/comProgramFixpoint.cmx
            - lib/coq/vernac/comProgramFixpoint.cmi
            - lib/coq/vernac/comPrimitive.cmx
            - lib/coq/vernac/comPrimitive.cmi
            - lib/coq/vernac/comInductive.cmx
            - lib/coq/vernac/comInductive.cmi
            - lib/coq/vernac/comHints.cmx
            - lib/coq/vernac/comHints.cmi
            - lib/coq/vernac/comFixpoint.cmx
            - lib/coq/vernac/comFixpoint.cmi
            - lib/coq/vernac/comDefinition.cmx
            - lib/coq/vernac/comDefinition.cmi
            - lib/coq/vernac/comCoercion.cmx
            - lib/coq/vernac/comCoercion.cmi
            - lib/coq/vernac/comAssumption.cmx
            - lib/coq/vernac/comAssumption.cmi
            - lib/coq/vernac/comArguments.cmx
            - lib/coq/vernac/comArguments.cmi
            - lib/coq/vernac/classes.cmx
            - lib/coq/vernac/classes.cmi
            - lib/coq/vernac/canonical.cmx
            - lib/coq/vernac/canonical.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/user-contrib/Ltac2/tac2types.cmi
            - lib/coq/user-contrib/Ltac2/tac2tactics.cmx
            - lib/coq/user-contrib/Ltac2/tac2tactics.cmi
            - lib/coq/user-contrib/Ltac2/tac2stdlib.cmx
            - lib/coq/user-contrib/Ltac2/tac2stdlib.cmi
            - lib/coq/user-contrib/Ltac2/tac2quote.cmx
            - lib/coq/user-contrib/Ltac2/tac2quote.cmi
            - lib/coq/user-contrib/Ltac2/tac2qexpr.cmi
            - lib/coq/user-contrib/Ltac2/tac2print.cmx
            - lib/coq/user-contrib/Ltac2/tac2print.cmi
            - lib/coq/user-contrib/Ltac2/tac2match.cmx
            - lib/coq/user-contrib/Ltac2/tac2match.cmi
            - lib/coq/user-contrib/Ltac2/tac2interp.cmx
            - lib/coq/user-contrib/Ltac2/tac2interp.cmi
            - lib/coq/user-contrib/Ltac2/tac2intern.cmx
            - lib/coq/user-contrib/Ltac2/tac2intern.cmi
            - lib/coq/user-contrib/Ltac2/tac2ffi.cmx
            - lib/coq/user-contrib/Ltac2/tac2ffi.cmi
            - lib/coq/user-contrib/Ltac2/tac2extffi.cmx
            - lib/coq/user-contrib/Ltac2/tac2extffi.cmi
            - lib/coq/user-contrib/Ltac2/tac2expr.cmi
            - lib/coq/user-contrib/Ltac2/tac2env.cmx
            - lib/coq/user-contrib/Ltac2/tac2env.cmi
            - lib/coq/user-contrib/Ltac2/tac2entries.cmx
            - lib/coq/user-contrib/Ltac2/tac2entries.cmi
            - lib/coq/user-contrib/Ltac2/tac2dyn.cmx
            - lib/coq/user-contrib/Ltac2/tac2dyn.cmi
            - lib/coq/user-contrib/Ltac2/tac2core.cmx
            - lib/coq/user-contrib/Ltac2/tac2core.cmi
            - lib/coq/user-contrib/Ltac2/ltac2_plugin.o
            - lib/coq/user-contrib/Ltac2/ltac2_plugin.cmxs
            - lib/coq/user-contrib/Ltac2/ltac2_plugin.cmx
            - lib/coq/user-contrib/Ltac2/ltac2_plugin.cmo
            - lib/coq/user-contrib/Ltac2/ltac2_plugin.cmi
            - lib/coq/user-contrib/Ltac2/g_ltac2.cmx
            - 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/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/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
            - 
[...] truncated
terp/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/deprecation.cmx
            - lib/coq/interp/deprecation.cmi
            - lib/coq/interp/decls.cmx
            - lib/coq/interp/decls.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_parser.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/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/META
            - bin/votour
            - bin/ocamllibdep
            - 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.13.1: not removing non-empty directories:
         - share/texmf/tex/latex/misc
         - lib/coq/vernac
         - lib/coq/user-contrib/Ltac2
         - lib/coq/toplevel
         - lib/coq/topbin
         - lib/coq/tools/coqdoc
         - lib/coq/theories/ssrsearch
         - 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/tactics
         - lib/coq/stm
         - lib/coq/proofs
         - lib/coq/printing
         - lib/coq/pretyping
         - lib/coq/plugins/syntax
         - lib/coq/plugins/ssrsearch
         - lib/coq/plugins/ssrmatching
         - lib/coq/plugins/rtauto
         - lib/coq/plugins/ring
         - 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.13.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)

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