# 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.07.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.07.1 Official release 4.07.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.3 A library manager for OCaml zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers # opam file: opam-version: "2.0" maintainer: "palmskog@gmail.com" homepage: "https://github.com/runtimeverification/vlsm" dev-repo: "git+https://github.com/runtimeverification/vlsm.git" bug-reports: "https://github.com/runtimeverification/vlsm/issues" license: "BSD-3-Clause" synopsis: "Coq formalization of validating labelled state transition and message production systems" description: """ A validating labelled state transition and message production system (VLSM) abstractly models a distributed system with faults. This project contains a formalization of VLSMs and their theory in the Coq proof assistant.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ "coq" {>= "8.13" & < "8.15~"} "coq-stdpp" {>= "1.6.0"} ] tags: [ "category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems" "keyword:fault tolerance" "keyword:distributed algorithms" "logpath:VLSM" "date:2022-02-18" ] authors: [ "Mihai Calancea" "Denisa Diaconescu" "Wojciech Kołowski" "Elaine Li" "Brandon Moore" "Karl Palmskog" "Lucas Peña" "Grigore Roșu" "Traian Șerbănuță" "Jan Tušil" "Vlad Zamfir" ] url { src: "https://github.com/runtimeverification/vlsm/archive/v1.1.tar.gz" checksum: "sha512=9eac41874fea4f622bb7f225b3c6c7f78ca517790ca0b467d571d86476778bdc6e8ea531815cf608b2a9eba966caa21101e90861bce80a10f054ceca53ec65fd" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-vlsm.1.1 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-vlsm.1.1 coq.8.13.1
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-vlsm.1.1 coq.8.13.1
Total: 14 M
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/Projections.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/VLSMProjections.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/ListExtras.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/Projections.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/VLSMProjections.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/VLSM.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/SubProjectionTraces.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/TraceProperties.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Projections.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/VLSM.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/SubProjectionTraces.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/LimitedEquivocation/FixedEquivocation.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/ListExtras.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/MsgDepLimitedEquivocation.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Common.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/LimitedEquivocation/FixedEquivocation.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/MessageProperties.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Composition.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/MsgDepLimitedEquivocation.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/Preamble.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/SimulatingFree/FullReplayTraces.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Composition.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Projections.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/FixedSetEquivocation.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/WitnessedEquivocation.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/ListSetExtras.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/ByzantineTraces/FixedSetByzantineTraces.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/FixedSetEquivocation.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/ByzantineTraces/LimitedByzantineTraces.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/TraceProperties.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Common.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/SortedLists.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/Preamble.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/ProjectionTraces.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/StreamExtras.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/SimulatingFree/FullReplayTraces.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/StreamFilters.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/VLSMProjections.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/SimulatingFree/SimulatingFree.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/TopSort.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/MsgDepFixedSetEquivocation.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/WitnessedEquivocation.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/ProjectionTraces.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/Projections.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/TraceWiseEquivocation.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/VLSM.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/LimitedEquivocation/FixedEquivocationSimulation.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/ListSetExtras.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/ByzantineTraces/FixedSetByzantineTraces.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/Common.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/LimitedEquivocation/LimitedEquivocation.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/AnnotatedVLSM.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/StreamExtras.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/StreamFilters.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/MessageDependencies.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/ByzantineTraces/LimitedByzantineTraces.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Validator.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/EquivocationProjections.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Plans.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/EquivocationProjections.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/LimitedEquivocation.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/LimitedEquivocation/LimitedEquivocation.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/SubProjectionTraces.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/LimitedEquivocation/FixedEquivocationSimulation.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/MsgDepFixedSetEquivocation.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Decisions.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/TopSort.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/LimitedEquivocation/LimitedEquivocationSimulation.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/NoEquivocation.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/FinSetExtras.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/Common.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/StdppExtras.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/ListExtras.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/SimulatingFree/SimulatingFree.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/MessageProperties.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/LimitedEquivocation/FixedEquivocation.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/StdppListSet.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/EquivocatorReplay.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/TraceWiseEquivocation.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/TraceClassicalProperties.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/MessageDependencies.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Validator.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Composition.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Projections.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/Measurable.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/ByzantineTraces.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Plans.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/LimitedEquivocation.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/FixedSetEquivocation.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/StdppExtras.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Common.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/FullNode.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/AnnotatedVLSM.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/SortedLists.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/TraceProperties.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Decisions.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/Temporal.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/WitnessedEquivocation.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/ByzantineTraces/FixedSetByzantineTraces.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/EquivocatorReplay.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/Preamble.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/LimitedEquivocation/LimitedEquivocationSimulation.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/NoEquivocation.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/FinFunExtras.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/ProjectionTraces.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/RealsExtras.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/MsgDepLimitedEquivocation.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/ByzantineTraces.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/SimulatingFree/FullReplayTraces.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/StdppListSet.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/FinExtras.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/MessageProperties.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/ListSetExtras.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/TopSort.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/ByzantineTraces/LimitedByzantineTraces.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/StreamFilters.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/StreamExtras.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/Traces.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/Temporal.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/LimitedEquivocation/FixedEquivocationSimulation.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/LimitedEquivocation/LimitedEquivocation.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/Common.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/SimulatingFree/SimulatingFree.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/MsgDepFixedSetEquivocation.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/FinSetExtras.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/EquivocationProjections.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Validator.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/MessageDependencies.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/ByzantineTraces.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Plans.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/SortedLists.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/TraceWiseEquivocation.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/AnnotatedVLSM.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/LimitedEquivocation.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/FullNode.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/NoEquivocation.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/Measurable.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Decisions.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/TraceClassicalProperties.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/Traces.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/Composition/LimitedEquivocation/LimitedEquivocationSimulation.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocators/EquivocatorReplay.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/StdppExtras.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/StdppListSet.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/RealsExtras.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/Temporal.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/FinFunExtras.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Core/Equivocation/FullNode.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/FinSetExtras.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/Measurable.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/Traces.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/TraceClassicalProperties.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/SsrExport.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/FinFunExtras.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/RealsExtras.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/FinExtras.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/FinExtras.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/SsrExport.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/VLSM/Lib/SsrExport.glob
opam remove -y coq-vlsm.1.1