# 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.1 Formal proof management system dune 3.12.1 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.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" 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"] {pinned} [ "dune" "build" "-p" name "-j" jobs "@install" ] ] depends: [ "dune" {>= "2.6"} "coq" "coq-ext-lib" "coq-paco" "coq-itree" {>= "5.0.0"} ] tags: [ "org:deepspec" "logpath: ITree.Extra" "date:2022-12-29" ] url { http: "https://github.com/DeepSpec/InteractionTrees/archive/5.1.0.tar.gz" checksum: "sha512=cb8986ab4d2af8eadbf99c05c5824df513cd803ddac1479ef943c5d402c65faa6f6ff4d3ffec4620d1f4139e741b7c40e61a4ac052bb15db1ce05b0edf5080fd" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-itree-extra.5.1.0 coq.8.14.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.0 coq.8.14.1
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-itree-extra.5.1.0 coq.8.14.1
Total: 17 M
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITraceBind.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqEuttHalt.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqWcompat.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITraceFacts.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITracePrefix.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqProgInsens.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/IForest.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/ITreeDijkstra.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureStateHandler.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqBind.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqEuttTrans.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/StateIOTrace.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureStateHandlerPi.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/TracesIT.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqProgInsensFacts.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqHalt.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqHaltProgInsens.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/DelaySpecMonad.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/PureITreeDijkstra.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/StateDelaySpec.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITracePreds.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/StateSpecT.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/PureITreeBasics.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITraceBind.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/IterRel.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqEuttHalt.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/IForest.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITraceDefinition.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITraceFacts.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/PureITreeDijkstra.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/ITreeDijkstra.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/StrongBisimProper.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqProgInsens.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/DijkstraMonad.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqWcompat.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureStateHandler.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/Labels.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/TracesIT.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITracePrefix.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqBind.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqHaltProgInsens.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/DelaySpecMonad.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/StateIOTrace.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureStateHandlerPi.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/StateDelaySpec.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqHalt.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqEuttTrans.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/StateSpecT.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITracePreds.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/SecureEqProgInsensFacts.v
../ocaml-base-compiler.4.07.1/doc/coq-itree-extra/CHANGELOG.md
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/IterRel.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/PureITreeBasics.v
../ocaml-base-compiler.4.07.1/lib/coq-itree-extra/dune-package
../ocaml-base-compiler.4.07.1/doc/coq-itree-extra/README.md
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Dijkstra/DijkstraMonad.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/ITrace/ITraceDefinition.v
../ocaml-base-compiler.4.07.1/doc/coq-itree-extra/LICENSE
../ocaml-base-compiler.4.07.1/lib/coq-itree-extra/opam
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/Labels.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/ITree/Extra/Secure/StrongBisimProper.v
../ocaml-base-compiler.4.07.1/lib/coq-itree-extra/META
opam remove -y coq-itree-extra.5.1.0