# 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.7.0 Fast, portable, and opinionated build system ocaml 4.07.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.07.1 Official release 4.07.1 ocaml-config 1 OCaml Switch Configuration ocaml-secondary-compiler 4.08.1-1 OCaml 4.08.1 Secondary Switch Compiler ocamlfind 1.9.1 A library manager for OCaml ocamlfind-secondary 1.9.1 Adds support for ocaml-secondary-compiler to ocamlfind zarith 1.12 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/affeldt-aist/monae" dev-repo: "git+https://github.com/affeldt-aist/monae.git" bug-reports: "https://github.com/affeldt-aist/monae/issues" license: "LGPL-2.1-or-later" synopsis: "Monads and equational reasoning in Coq" description: """ This Coq library contains a hierarchy of monads with their laws used in several examples of monadic equational reasoning.""" build: [make "-j%{jobs}%" ] install: [make "install_full"] depends: [ "coq" { (>= "8.13" & < "8.16~") | (= "dev") } "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.15~") | (= "dev") } "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.15~") | (= "dev") } "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.15~") | (= "dev") } "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.15~") | (= "dev") } "coq-mathcomp-field" { (>= "1.13.0" & < "1.15~") | (= "dev") } "coq-mathcomp-analysis" { (>= "0.3.11" & < "0.4~") } "coq-infotheo" { >= "0.3.5" & <= "0.3.6"} "coq-paramcoq" { >= "1.1.3" & < "1.2~" } "coq-hierarchy-builder" { >= "1.1.0" } ] tags: [ "keyword:monae" "keyword:effects" "keyword:probability" "keyword:nondeterminism" "logpath:monae" "date:2022-02-21" ] authors: [ "Reynald Affeldt" "David Nowak" "Takafumi Saikawa" "Jacques Garrigue" "Ayumu Saito" "Celestine Sauvage" "Kazunari Tanaka" ] url { http: "https://github.com/affeldt-aist/monae/archive/0.4.tar.gz" checksum: "sha512=d6e28034d9ef1010290a8380bfd0c0d4205f3d688785f56c8d5c60f51002482381d48009a6432e99fe2e182aa0c5406a209bce9809c5dce8da60b33dd922c979" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-monae.0.4 coq.8.14.0
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
true
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-monae.0.4 coq.8.14.0
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-monae.0.4 coq.8.14.0
Total: 21 M
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/hierarchy.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/monad_model.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/ihierarchy.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/category.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/monad_transformer.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/fail_lib.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/imonad_transformer.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_iquicksort.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/smallstep.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/fail_lib.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/monad_model.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/imonad_model.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/state_lib.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/imonad_transformer.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/imonad_model.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/category.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_quicksort.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_monty.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/ihierarchy.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/monad_transformer.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/ifail_lib.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_monty.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_iquicksort.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/hierarchy.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/ifail_lib.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/gcm_model.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/state_lib.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/proba_lib.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/proba_lib.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/category_ext.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/monad_lib.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/istate_lib.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/ifmt_lifting.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_nqueens.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_nqueens.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/imonad_lib.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/monad_composition.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/smallstep.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/istate_lib.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/altprob_model.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/monad_lib.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/ifmt_lifting.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/imonad_lib.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/gcm_model.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/imonad_composition.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/array_lib.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/imonad_composition.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_spark.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/category_ext.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_relabeling.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/monad_composition.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_spark.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_quicksort.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_transformer.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_relabeling.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/proba_monad_model.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/monad_model.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/trace_lib.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/altprob_model.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/iparametricity_codensity.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/array_lib.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/fail_lib.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/iexample_transformer.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/itrace_lib.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/imonad_model.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/hierarchy.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/iexample_transformer.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/ihierarchy.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/category.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/monae_lib.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/monad_transformer.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/imonae_lib.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/imonad_transformer.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_transformer.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/iparametricity_codensity.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/smallstep.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/itrace_lib.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/ifail_lib.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/gcm_model.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/imonae_lib.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/monae_lib.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_iquicksort.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/trace_lib.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/state_lib.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/monad_lib.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_monty.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/imonad_lib.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/ifmt_lifting.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/proba_lib.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/proba_monad_model.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_nqueens.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/category_ext.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/istate_lib.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_quicksort.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/imonad_composition.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/monad_composition.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_spark.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/altprob_model.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/array_lib.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_relabeling.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/example_transformer.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/iexample_transformer.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/iparametricity_codensity.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/monae_lib.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/imonae_lib.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monaeImpredicativeSet/itrace_lib.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/trace_lib.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/monae/proba_monad_model.v
opam remove -y coq-monae.0.4