# 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.13.1 Formal proof management system num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.12.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.12.1 Official release 4.12.1 ocaml-config 2 OCaml Switch Configuration ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled ocamlfind 1.9.6 A library manager for OCaml zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers # opam file: opam-version: "2.0" synopsis: "Extensions to coq-itree" maintainer: ["Li-yao Xia <lysxia@gmail.com>"] authors: [ "Lucas Silver" "Irene Yoon" "Paul He" "Yannick Zakowski" "Steve Zdancewic" ] license: "MIT" homepage: "https://github.com/DeepSpec/InteractionTrees" bug-reports: "https://github.com/DeepSpec/InteractionTrees/issues" dev-repo: "git+https://github.com/DeepSpec/InteractionTrees.git" build: [ [ "./fixup.sh" ] [ "dune" "subst"] {dev} [ "dune" "build" "-p" name "-j" jobs "@install" ] ] depends: [ "dune" {>= "2.6"} "coq" "coq-ext-lib" {>= "0.11.1"} "coq-paco" "coq-itree" {>= "5.1.0"} ] tags: [ "org:deepspec" "logpath: ITree.Extra" "date:2023-10-27" ] url { http: "https://github.com/DeepSpec/InteractionTrees/archive/5.1.2.tar.gz" checksum: "sha512=989f966960f68f55b257e887438e6a03f21c2e7eee743f56bf05452756624f777b266a38b6ec767aa73d2f8fa0fe6953424115d529bef5eb6a89b572db618093" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-itree-extra.5.1.2 coq.8.13.1
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-itree-extra.5.1.2 coq.8.13.1
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-itree-extra.5.1.2 coq.8.13.1
Total: 16 M
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqEuttHalt.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITraceBind.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqWcompat.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITraceFacts.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITracePrefix.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqProgInsens.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/ITreeDijkstra.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/IForest.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureStateHandler.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqBind.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqEuttTrans.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureStateHandlerPi.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/StateIOTrace.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqProgInsensFacts.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/TracesIT.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqHalt.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqHaltProgInsens.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/DelaySpecMonad.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/StateDelaySpec.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/PureITreeDijkstra.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITracePreds.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/StateSpecT.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/PureITreeBasics.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITraceBind.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/IterRel.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqEuttHalt.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/IForest.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITraceDefinition.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITraceFacts.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/PureITreeDijkstra.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/ITreeDijkstra.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/StrongBisimProper.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqProgInsens.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/DijkstraMonad.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqWcompat.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureStateHandler.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/Labels.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/TracesIT.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITracePrefix.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqBind.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqHaltProgInsens.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/DelaySpecMonad.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureStateHandlerPi.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/StateIOTrace.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/StateDelaySpec.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqHalt.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqEuttTrans.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/StateSpecT.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITracePreds.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqProgInsensFacts.v
../ocaml-base-compiler.4.12.1/doc/coq-itree-extra/CHANGELOG.md
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/IterRel.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/PureITreeBasics.v
../ocaml-base-compiler.4.12.1/lib/coq-itree-extra/dune-package
../ocaml-base-compiler.4.12.1/doc/coq-itree-extra/README.md
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/DijkstraMonad.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITraceDefinition.v
../ocaml-base-compiler.4.12.1/doc/coq-itree-extra/LICENSE
../ocaml-base-compiler.4.12.1/lib/coq-itree-extra/opam
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/Labels.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/ITree/Extra/Secure/StrongBisimProper.v
../ocaml-base-compiler.4.12.1/lib/coq-itree-extra/META
opam remove -y coq-itree-extra.5.1.2