# 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 dev Formal proof management system
dune 3.1.1 Fast, portable, and opinionated build system
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.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: ["dune" "build" "-p" name "-j" jobs]
depends: [
"dune" {>= "2.5"}
"coq" {>= "8.13"}
"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"
]
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: "git+https://github.com/runtimeverification/vlsm.git#master"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-vlsm.dev coq.devDry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-vlsm.dev coq.devopam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y coq-vlsm.dev coq.dev# 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 dev Formal proof management system coq-stdpp dev An extended "Standard Library" for Coq dune 3.1.1 Fast, portable, and opinionated build system 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.3 A library manager for OCaml zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers [NOTE] Package coq is already installed (current version is dev). The following actions will be performed: - install coq-vlsm dev <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> [coq-vlsm.dev] synchronised from git+https://github.com/runtimeverification/vlsm.git#master <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> [ERROR] The compilation of coq-vlsm failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-vlsm -j 4". #=== ERROR while compiling coq-vlsm.dev =======================================# # context 2.0.8 | linux/x86_64 | ocaml-base-compiler.4.12.1 | file:///home/bench/run/opam-coq-archive/extra-dev # path ~/.opam/ocaml-base-compiler.4.12.1/.opam-switch/build/coq-vlsm.dev # command ~/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-vlsm -j 4 # exit-code 1 # env-file ~/.opam/log/coq-vlsm-11092-e4db2f.env # output-file ~/.opam/log/coq-vlsm-11092-e4db2f.out ### output ### # [...] # A coercion will be introduced in future versions when using ':>' in 'Class' declarations. Use '#[global] Existing Instance field.' instead if you don't want the coercion. # [future-coercion-class-field,records] # (cd _build/default && /home/bench/.opam/ocaml-base-compiler.4.12.1/bin/coqc -q -w -deprecated-instance-without-locality -R theories/VLSM VLSM theories/VLSM/Lib/ListExtras.v) # File "./theories/VLSM/Lib/ListExtras.v", line 1, characters 0-32: # Error: Cannot find a physical path bound to logical path # Itauto with prefix Cdcl. # # (cd _build/default && /home/bench/.opam/ocaml-base-compiler.4.12.1/bin/coqc -q -w -deprecated-instance-without-locality -R theories/VLSM VLSM theories/VLSM/Lib/FinSetExtras.v) # File "./theories/VLSM/Lib/FinSetExtras.v", line 1, characters 0-32: # Error: Cannot find a physical path bound to logical path # Itauto with prefix Cdcl. # <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-vlsm dev +- - No changes have been performed # Run eval $(opam env) to update the current shell environment
No files were installed.
true