This result is black-listed as it is considered as too hard to reproduce / to solve. If you find a way to fix this package, please make a pull-request to github.com/coq/opam-coq-archive. The list of black-listed packages is in black_list.rb.
# 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.15.1 Formal proof management system
dune 3.12.1 Fast, portable, and opinionated build system
ocaml 4.06.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.06.1 Official 4.06.1 release
ocaml-config 1 OCaml Switch Configuration
ocaml-secondary-compiler 4.08.1-1 OCaml 4.08.1 Secondary Switch Compiler
ocamlfind 1.9.6 A library manager for OCaml
ocamlfind-secondary 1.9.6 Adds support for ocaml-secondary-compiler to ocamlfind
zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: [
"Érik Martin-Dorel <erik.martin-dorel@irit.fr>"
"Pierre Roux <pierre.roux@onera.fr>"
]
homepage: "https://sourcesup.renater.fr/validsdp/"
dev-repo: "git+https://github.com/validsdp/validsdp.git"
bug-reports: "https://github.com/validsdp/validsdp/issues"
license: "LGPL-2.1-or-later"
build: [
["sh" "-c" "./configure"]
[make "-j%{jobs}%"]
]
run-test: [make "-j%{jobs}%" "test"]
install: [make "install"]
depends: [
"ocaml"
"coq" {>= "8.12" & < "8.16~"}
"coq-bignums" {< "9~"}
"coq-flocq" {>= "3.3.0"}
"coq-interval" {>= "4.0.0" & < "5~"}
"coq-mathcomp-field" {>= "1.12" & < "1.15~"}
"coq-mathcomp-analysis" {>= "0.3.4" & < "0.4~"}
"coq-libvalidsdp" {= "1.0.0"}
"coq-mathcomp-multinomials" {>= "1.2"}
"coq-coqeal" {>= "1.1.0"}
"coq-paramcoq" {>= "1.1.0"}
"osdp" {>= "1.0"}
"ocamlfind" {build}
"conf-autoconf" {build & dev}
]
synopsis: "ValidSDP"
description: """
ValidSDP is a library for the Coq formal proof assistant. It provides
reflexive tactics to prove multivariate inequalities involving
real-valued variables and rational constants, using SDP solvers as
untrusted back-ends and verified checkers based on libValidSDP.
Once installed, you can import the following modules:
From Coq Require Import Reals.
From ValidSDP Require Import validsdp.
"""
tags: [
"keyword:libValidSDP"
"keyword:ValidSDP"
"keyword:floating-point arithmetic"
"keyword:Cholesky decomposition"
"category:Miscellaneous/Coq Extensions"
"logpath:ValidSDP"
]
authors: [
"Érik Martin-Dorel <erik.martin-dorel@irit.fr>"
"Pierre Roux <pierre.roux@onera.fr>"
]
url {
src: "https://github.com/validsdp/validsdp/releases/download/v1.0.0/validsdp-1.0.0.tar.gz"
checksum: "sha512=94d872eb3ef308cc7c344f3c39e60d5bc265b05bc6c50b2399475e1ac4e105b330b1d63cf4193a04388b7a173f142e246bb6b6c46092fe9c221ed85b1d6b7c3f"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-validsdp.1.0.0 coq.8.15.1[NOTE] Package coq is already installed (current version is 8.15.1).
The following dependencies couldn't be met:
- coq-validsdp -> coq-libvalidsdp = 1.0.0 -> coq-mathcomp-analysis < 0.4~ -> coq < 8.9~ -> ocaml < 4.06.0
base of this switch (use `--unlock-base' to force)
- coq-validsdp -> coq-libvalidsdp = 1.0.0 -> coq-mathcomp-analysis < 0.4~ -> coq-hierarchy-builder >= 1.0.0 -> coq-elpi >= 1.6 -> coq (< 8.14~ | >= 8.16) -> ocaml (< 4.06.0 | >= 4.09.0)
base of this switch (use `--unlock-base' to force)
- coq-validsdp -> coq-libvalidsdp = 1.0.0 -> coq-mathcomp-analysis < 0.4~ -> coq-hierarchy-builder >= 1.0.0 -> coq-elpi >= 1.6 -> coq (< 8.14~ | >= 8.16) -> coq-core -> ocaml >= 4.09.0
base of this switch (use `--unlock-base' to force)
- coq-validsdp -> coq-libvalidsdp = 1.0.0 -> coq-mathcomp-analysis < 0.4~ -> coq-hierarchy-builder >= 1.0.0 -> coq-elpi >= 1.6 -> elpi >= 1.16.5 -> ocaml >= 4.07.0
base of this switch (use `--unlock-base' to force)
- coq-validsdp -> coq-libvalidsdp = 1.0.0 -> coq-mathcomp-analysis < 0.4~ -> coq-hierarchy-builder >= 1.0.0 -> coq-elpi >= 1.6 -> ocaml >= 4.07
base of this switch (use `--unlock-base' to force)
- coq-validsdp -> coq-libvalidsdp = 1.0.0 -> coq-mathcomp-analysis < 0.4~ -> coq-mathcomp-finmap < 1.4~ -> coq-mathcomp-ssreflect < 1.8~ -> coq < 8.10~ -> ocaml < 4.06.0
base of this switch (use `--unlock-base' to force)
- coq-validsdp -> coq-libvalidsdp = 1.0.0 -> coq-mathcomp-analysis < 0.4~ -> coq-mathcomp-finmap < 1.4~ -> coq < 8.11.1 -> ocaml < 4.06.0
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:
opam remove -y coq; opam install -y --show-action --unlock-base coq-validsdp.1.0.0The following actions will be performed:
- remove coq 8.15.1
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[WARNING] While removing coq.8.15.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/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
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/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/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__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.15.1: 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.15.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)
truetrueNo files were installed.
true