« Up

elpi 1.6.0 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.14.0      Formal proof management system
dune                  3.4.1       Fast, portable, and opinionated build system
ocaml                 4.14.0      The OCaml compiler (virtual package)
ocaml-base-compiler   4.14.0      Official release 4.14.0
ocaml-config          2           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled
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: "Enrico Tassi <enrico.tassi@inria.fr>"
authors: [ "Enrico Tassi" ]
license: "LGPL-2.1-or-later"
homepage: "https://github.com/LPCIC/coq-elpi"
bug-reports: "https://github.com/LPCIC/coq-elpi/issues"
dev-repo: "git+https://github.com/LPCIC/coq-elpi"
build: [ make "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ]
install: [ make "install" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ]
depends: [
  "elpi" {>= "1.11.2" & < "1.12.0~"}
  "coq" {>= "8.12" & < "8.13~"}
  ]
  tags: [
    "logpath:elpi"
  ]
synopsis: "Elpi extension language for Coq"
description: """
Coq-elpi provides a Coq plugin that embeds ELPI.
It also provides a way to embed Coq's terms into λProlog using
the Higher-Order Abstract Syntax approach
and a way to read terms back.  In addition to that it exports to ELPI a
set of Coq's primitives, e.g. printing a message, accessing the
environment of theorems and data types, defining a new constant and so on.
For convenience it also provides a quotation and anti-quotation for Coq's
syntax in λProlog.  E.g. `{{nat}}` is expanded to the type name of natural
numbers, or `{{A -> B}}` to the representation of a product by unfolding
the `->` notation. Finally it provides a way to define new vernacular commands
and new tactics."""
url {
src: "https://github.com/LPCIC/coq-elpi/archive/v1.6.0.tar.gz"
checksum: "sha256=6f047c78ad9e75fca2462bf32f71a34e8db0b83031a5b5b8adc8fc4ca4843d8f"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-elpi.1.6.0 coq.8.14.0
Return code
5120
Output
[NOTE] Package coq is already installed (current version is 8.14.0).
The following dependencies couldn't be met:
  - coq-elpi -> coq < 8.13~ -> ocaml < 4.12
      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-elpi.1.6.0
Return code
15360
Output
The following actions will be performed:
  - remove coq 8.14.0
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[WARNING] While removing coq.8.14.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/ssrsearch/ssrsearch.vos
            - lib/coq/theories/ssrsearch/ssrsearch.vo
            - lib/coq/theories/ssrsearch/ssrsearch.v
            - lib/coq/theories/ssrsearch/ssrsearch.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/Ri
[...] truncated
ys.cmi
            - lib/coq-core/clib/int.mli
            - lib/coq-core/clib/int.ml
            - lib/coq-core/clib/int.cmx
            - lib/coq-core/clib/int.cmti
            - lib/coq-core/clib/int.cmt
            - lib/coq-core/clib/int.cmi
            - lib/coq-core/clib/iStream.mli
            - lib/coq-core/clib/iStream.ml
            - lib/coq-core/clib/iStream.cmx
            - lib/coq-core/clib/iStream.cmti
            - lib/coq-core/clib/iStream.cmt
            - lib/coq-core/clib/iStream.cmi
            - lib/coq-core/clib/heap.mli
            - lib/coq-core/clib/heap.ml
            - lib/coq-core/clib/heap.cmx
            - lib/coq-core/clib/heap.cmti
            - lib/coq-core/clib/heap.cmt
            - lib/coq-core/clib/heap.cmi
            - lib/coq-core/clib/hashset.mli
            - lib/coq-core/clib/hashset.ml
            - lib/coq-core/clib/hashset.cmx
            - lib/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/cPath.mli
            - lib/coq-core/clib/cPath.ml
            - lib/coq-core/clib/cPath.cmx
            - lib/coq-core/clib/cPath.cmti
            - lib/coq-core/clib/cPath.cmt
            - lib/coq-core/clib/cPath.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/META
            - doc/coqide-server/README.md
            - doc/coqide-server/LICENSE
            - doc/coq-core/README.md
            - doc/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.14.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/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-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/ssrsearch
         - 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/float_syntax
         - 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
         - doc/coqide-server
         - doc/coq-core
-> removed   coq.8.14.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