# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base camlp5 7.14 Preprocessor-pretty-printer of OCaml conf-findutils 1 Virtual package relying on findutils conf-perl 2 Virtual package relying on perl coq 8.9.0 Formal proof management system num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.08.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.08.1 Official release 4.08.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.6 A library manager for OCaml # opam file: opam-version: "2.0" maintainer: "christian.doczkal@inria.fr" homepage: "https://github.com/coq-community/comp-dec-modal" dev-repo: "git+https://github.com/coq-community/comp-dec-modal.git" bug-reports: "https://github.com/coq-community/comp-dec-modal/issues" doc: "https://coq-community.github.io/comp-dec-modal/" license: "CECILL-B" synopsis: "Constructive proofs of soundness and completeness for K, K*, CTL, PDL, and PDL with converse" description: """ This project presents machine-checked constructive proofs of soundness, completeness, decidability, and the small-model property for the logics K, K*, CTL, and PDL (with and without converse). For all considered logics, we prove soundness and completeness of their respective Hilbert-style axiomatization. For K, K*, and CTL, we also prove soundness and completeness for Gentzen systems (i.e., sequent calculi). For each logic, the central construction is a pruning-based algorithm computing for a given formula either a satisfying model of bounded size or a proof of its negation. The completeness and decidability results then follow with soundness from the existence of said algorithm. """ build: [make "-j%{jobs}%" ] install: [make "install"] depends: [ "coq" {>= "8.12" & < "8.16~"} "coq-mathcomp-ssreflect" {>= "1.11" & < "1.15~"} ] tags: [ "category:Mathematics/Logic/Modal logic" "keyword:modal logic" "keyword:completeness" "keyword:decidability" "keyword:Hilbert system" "keyword:computation tree logic" "keyword:propositional dynamic logic" "logpath:CompDecModal" "date:2022-01-20" ] authors: [ "Christian Doczkal" ] url { src: "https://github.com/coq-community/comp-dec-modal/archive/v1.1.tar.gz" checksum: "sha512=2cfafecb680d873a6a4e9e9ac43a20787230682a00ab2d9a53ee7bfce8f886caf00dbc8a2f06ccd617f66882594d42307c4b26e44134f530962c00ff1698aa4e" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-comp-dec-modal.1.1 coq.8.9.0
[NOTE] Package coq is already installed (current version is 8.9.0). The following dependencies couldn't be met: - coq-comp-dec-modal -> coq >= 8.12 -> ocaml >= 4.09.0 base of this switch (use `--unlock-base' to force) - coq-comp-dec-modal -> coq >= 8.12 -> coq-core -> ocaml >= 4.09.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-comp-dec-modal.1.1
true
true
No files were installed.
true