# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-findutils 1 Virtual package relying on findutils conf-m4 1 Virtual package relying on m4 coq 8.10.0 Formal proof management system num 1.3 The legacy Num library for arbitrary-precision integer and rational arithmetic 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 ocamlfind 1.8.1 A library manager for OCaml # opam file: opam-version: "2.0" maintainer: "coqdev@inria.fr" homepage: "https://coq.inria.fr/" license: "LGPL-2.1" build: [ ["./configure" "-configdir" "%{lib}%/coq/config" "-mandir" man "-docdir" doc "-prefix" prefix "-usecamlp5" "-camlp5dir" "%{lib}%/camlp5"] [make "-j%{jobs}%" "coqide-files"] [make "-j%{jobs}%" "coqide-binaries"] [make "install-ide-bin" "install-ide-files" "install-ide-info" "install-ide-devfiles"] ] remove: ["rm" "-R" "%{lib}%/coq/ide" "%{doc}%/FAQ-CoqIde"] depends: [ "ocaml" "camlp5" "coq" {= "8.5~beta3"} "lablgtk" "conf-gtksourceview" ] synopsis: "IDE of the Coq formal proof management system." flags: light-uninstall extra-files: ["coq-coqide.install" "md5=d005cda8cb7888fbea94c5416dcb31bc"] url { src: "https://github.com/coq/coq/archive/V8.5beta3.tar.gz" checksum: "md5=5d4b60f163d87e20b8f26cacb61d9d3d" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-coqide.8.5~beta3 coq.8.10.0
[NOTE] Package coq is already installed (current version is 8.10.0). The following dependencies couldn't be met: - coq-coqide -> coq = 8.5~beta3 -> ocaml < 4.05.0 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:
opam remove -y coq; opam install -y --show-action --unlock-base coq-coqide.8.5~beta3
true
true
No files were installed.
true