(2021-04-06 20:47:58 UTC)
# 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 3 Virtual package relying on a GMP lib system installation
coq dev Formal proof management system
num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.10.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.10.1 Official release 4.10.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.1 A library manager for OCaml
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "FCSL <fcsl@software.imdea.org>"
homepage: "http://software.imdea.org/fcsl/"
bug-reports: "https://github.com/imdea-software/fcsl-pcm/issues"
dev-repo: "git+https://github.com/imdea-software/fcsl-pcm.git"
license: "Apache-2.0"
build: [ make "-j%{jobs}%" ]
install: [ make "install" ]
depends: [
"coq" {(>= "8.11" & < "8.13~") | (= "dev")}
"coq-mathcomp-ssreflect" {(>= "1.10.0" & < "1.12~") | (= "dev")}
]
tags: [
"keyword:separation logic"
"keyword:partial commutative monoid"
"category:Computer Science/Data Types and Data Structures"
"logpath:fcsl"
"date:2020-10-15"
]
authors: [
"Aleksandar Nanevski"
]
synopsis: "Partial Commutative Monoids"
description: """
The PCM library provides a formalisation of Partial Commutative Monoids (PCMs),
a common algebraic structure used in separation logic for verification of
pointer-manipulating sequential and concurrent programs.
The library provides lemmas for mechanised and automated reasoning about PCMs
in the abstract, but also supports concrete common PCM instances, such as heaps,
histories and mutexes.
This library relies on extensionality axioms: propositional and
functional extentionality."""
url {
src: "https://github.com/imdea-software/fcsl-pcm/archive/v1.3.0.tar.gz"
checksum: "sha256=3ac78341d681df1a35ad720a84b81089eec1bee30197b15d15b29a3d8c3cec85"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-fcsl-pcm.1.3.0 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 2h opam install -y --deps-only coq-fcsl-pcm.1.3.0 coq.devopam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y -v coq-fcsl-pcm.1.3.0 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 3 Virtual package relying on a GMP lib system installation coq dev Formal proof management system coq-mathcomp-ssreflect dev Small Scale Reflection num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.10.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.10.1 Official release 4.10.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.1 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-fcsl-pcm 1.3.0 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/1: [coq-fcsl-pcm.1.3.0: http] [coq-fcsl-pcm.1.3.0] downloaded from https://github.com/imdea-software/fcsl-pcm/archive/v1.3.0.tar.gz Processing 1/1: <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/2: [coq-fcsl-pcm: make] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.10.1/.opam-switch/build/coq-fcsl-pcm.1.3.0) - coq_makefile -f _CoqProject -o CoqMakefile - make --no-print-directory -f CoqMakefile - COQDEP VFILES - COQC options.v - COQC core/axioms.v - COQC core/ordtype.v - File "./core/axioms.v", line 92, characters 0-28: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - COQC core/prelude.v - File "./core/ordtype.v", line 132, characters 15-32: - Warning: Notation subseq_order_path is deprecated since mathcomp 1.12.0. - Use subseq_path instead. [deprecated-syntactic-definition,deprecated] - File "./core/ordtype.v", line 132, characters 15-32: - Warning: Notation subseq_order_path is deprecated since mathcomp 1.12.0. - Use subseq_path instead. [deprecated-syntactic-definition,deprecated] - File "./core/ordtype.v", line 136, characters 17-30: - Warning: Notation eq_sorted_irr is deprecated since mathcomp 1.12.0. - Use irr_sorted_eq instead. [deprecated-syntactic-definition,deprecated] - File "./core/ordtype.v", line 136, characters 17-30: - Warning: Notation eq_sorted_irr is deprecated since mathcomp 1.12.0. - Use irr_sorted_eq instead. [deprecated-syntactic-definition,deprecated] - File "./core/ordtype.v", line 140, characters 0-52: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - File "./core/ordtype.v", line 445, characters 7-20: - Warning: Notation eq_sorted_irr is deprecated since mathcomp 1.12.0. - Use irr_sorted_eq instead. [deprecated-syntactic-definition,deprecated] - File "./core/ordtype.v", line 445, characters 7-20: - Warning: Notation eq_sorted_irr is deprecated since mathcomp 1.12.0. - Use irr_sorted_eq instead. [deprecated-syntactic-definition,deprecated] - File "./core/prelude.v", line 376, characters 0-86: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - COQC core/pred.v - File "./core/pred.v", line 129, characters 0-122: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 131, characters 0-114: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 133, characters 0-156: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 133, characters 0-156: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 135, characters 0-151: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 135, characters 0-151: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 217, characters 0-120: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 219, characters 0-137: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 221, characters 0-181: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 221, characters 0-181: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 225, characters 0-164: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 225, characters 0-164: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 228, characters 0-153: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 228, characters 0-153: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 231, characters 0-139: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 231, characters 0-139: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 285, characters 0-53: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - File "./core/pred.v", line 434, characters 0-30: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - File "./core/pred.v", line 529, characters 0-167: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 533, characters 0-190: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 537, characters 0-133: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 540, characters 0-147: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./core/pred.v", line 739, characters 0-39: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - File "./core/pred.v", line 818, characters 0-30: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - COQC core/seqperm.v - File "./core/seqperm.v", line 183, characters 0-113: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - COQC core/finmap.v - COQC pcm/pcm.v - File "./pcm/pcm.v", line 184, characters 0-31: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - File "./pcm/pcm.v", line 741, characters 0-62: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - COQC pcm/morphism.v - COQC core/rtc.v - COQC pcm/invertible.v - COQC pcm/unionmap.v - COQC pcm/mutex.v - COQC pcm/lift.v - File "./pcm/unionmap.v", line 840, characters 0-48: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - File "./pcm/unionmap.v", line 849, characters 9-22: - Warning: Notation eq_sorted_irr is deprecated since mathcomp 1.12.0. - Use irr_sorted_eq instead. [deprecated-syntactic-definition,deprecated] - File "./pcm/unionmap.v", line 849, characters 9-22: - Warning: Notation eq_sorted_irr is deprecated since mathcomp 1.12.0. - Use irr_sorted_eq instead. [deprecated-syntactic-definition,deprecated] - File "./pcm/unionmap.v", line 1164, characters 0-31: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - File "./pcm/unionmap.v", line 1240, characters 0-32: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - File "./pcm/unionmap.v", line 1795, characters 20-33: - Warning: Notation eq_sorted_irr is deprecated since mathcomp 1.12.0. - Use irr_sorted_eq instead. [deprecated-syntactic-definition,deprecated] - File "./pcm/unionmap.v", line 1795, characters 20-33: - Warning: Notation eq_sorted_irr is deprecated since mathcomp 1.12.0. - Use irr_sorted_eq instead. [deprecated-syntactic-definition,deprecated] - File "./pcm/unionmap.v", line 1805, characters 20-33: - Warning: Notation eq_sorted_irr is deprecated since mathcomp 1.12.0. - Use irr_sorted_eq instead. [deprecated-syntactic-definition,deprecated] - File "./pcm/unionmap.v", line 1805, characters 20-33: - Warning: Notation eq_sorted_irr is deprecated since mathcomp 1.12.0. - Use irr_sorted_eq instead. [deprecated-syntactic-definition,deprecated] - File "./pcm/unionmap.v", line 2059, characters 0-48: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - File "./pcm/unionmap.v", line 2818, characters 0-134: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./pcm/unionmap.v", line 2818, characters 0-134: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./pcm/unionmap.v", line 2821, characters 0-129: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./pcm/unionmap.v", line 2821, characters 0-129: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./pcm/unionmap.v", line 2824, characters 0-130: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./pcm/unionmap.v", line 2824, characters 0-130: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./pcm/unionmap.v", line 2827, characters 0-138: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./pcm/unionmap.v", line 2827, characters 0-138: - Warning: grammar entry "ident" permitted "_" in addition to proper - identifiers; this use is deprecated and its meaning will change in the - future; use "name" instead. [deprecated-ident-entry,deprecated] - File "./pcm/unionmap.v", line 2942, characters 2-66: - Error: - No assumption in (exists w0 : V, - [/\ C k, valid (pts x z \+ omap a f), - (k, w0) \In pts x w \+ f - & a (k, w0) = Some v]) - - make[2]: *** [CoqMakefile:720: pcm/unionmap.vo] Error 1 - make[1]: *** [CoqMakefile:344: all] Error 2 - make: *** [Makefile:13: invoke-coqmakefile] Error 2 [ERROR] The compilation of coq-fcsl-pcm failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j4". #=== ERROR while compiling coq-fcsl-pcm.1.3.0 =================================# # context 2.0.6 | linux/x86_64 | ocaml-base-compiler.4.10.1 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.10.1/.opam-switch/build/coq-fcsl-pcm.1.3.0 # command ~/.opam/opam-init/hooks/sandbox.sh build make -j4 # exit-code 2 # env-file ~/.opam/log/coq-fcsl-pcm-30197-335865.env # output-file ~/.opam/log/coq-fcsl-pcm-30197-335865.out ### output ### # [...] # identifiers; this use is deprecated and its meaning will change in the # future; use "name" instead. [deprecated-ident-entry,deprecated] # File "./pcm/unionmap.v", line 2942, characters 2-66: # Error: # No assumption in (exists w0 : V, # [/\ C k, valid (pts x z \+ omap a f), # (k, w0) \In pts x w \+ f # & a (k, w0) = Some v]) # # make[2]: *** [CoqMakefile:720: pcm/unionmap.vo] Error 1 # make[1]: *** [CoqMakefile:344: all] Error 2 # make: *** [Makefile:13: invoke-coqmakefile] Error 2 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-fcsl-pcm 1.3.0 +- - No changes have been performed # Run eval $(opam env) to update the current shell environment 'opam install -y -v coq-fcsl-pcm.1.3.0 coq.dev' failed.
No files were installed.
true