Commit c4001d2a authored by Ralf Jung's avatar Ralf Jung

Require Coq 8.11 and fix some warnings

parent 102189ac
Pipeline #33429 passed with stage
in 15 minutes and 26 seconds
......@@ -27,21 +27,16 @@ variables:
## Build jobs
build-coq.8.12.dev:
build-coq.8.12.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.12.dev"
OPAM_PINS: "coq version 8.12.0"
CI_COQCHK: "1"
tags:
- fp-timing
build-coq.8.11.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.11.2"
OPAM_PKG: "coq-orc11"
tags:
- fp-timing
build-coq.8.10.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.10.2"
......@@ -28,7 +28,7 @@ The race detector is summarized as follows (NA: non-atomic / AT : atomic):
This version is known to compile with:
- Coq 8.10.2 / 8.11.2
- Coq 8.11.2 / 8.12.0
- A development version of [stdpp]. See the [opam](opam) file for the exact
version.
......
-Q theories orc11
# We sometimes want to locally override notation, and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# Non-canonical projections require Coq 8.11.
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -projection-no-head-constant
theories/base.v
theories/value.v
......
......@@ -10,7 +10,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/orc11.git"
synopsis: "A Coq formalization of the ORC11 semantics for weak memory"
depends: [
"coq" { (>= "8.10.0" & < "8.13~") | (= "dev") }
"coq" { (>= "8.11.0" & < "8.13~") | (= "dev") }
"coq-stdpp" { (= "dev.2020-08-07.0.67db2f24") | (= "dev") }
]
......
......@@ -393,21 +393,36 @@ Structure latticeT : Type := Make_Lat {
lat_ty :> Type;
lat_equiv : Equiv lat_ty;
lat_sqsubseteq : SqSubsetEq lat_ty;
#[canonical(false)]
lat_join : Join lat_ty;
#[canonical(false)]
lat_meet : Meet lat_ty;
#[canonical(false)]
lat_inhabited : Inhabited lat_ty;
#[canonical(false)]
lat_sqsubseteq_proper : Proper (() ==> () ==> iff) ();
#[canonical(false)]
lat_join_proper : Proper (() ==> () ==> ()) ();
#[canonical(false)]
lat_meet_proper : Proper (() ==> () ==> ()) ();
#[canonical(false)]
lat_equiv_equivalence : Equivalence ();
#[canonical(false)]
lat_pre_order : PreOrder (@{lat_ty});
#[canonical(false)]
lat_sqsubseteq_antisym : AntiSymm () ();
#[canonical(false)]
lat_join_sqsubseteq_l (X Y : lat_ty) : X X Y;
#[canonical(false)]
lat_join_sqsubseteq_r (X Y : lat_ty) : Y X Y;
#[canonical(false)]
lat_join_lub (X Y Z : lat_ty) : X Z Y Z X Y Z;
#[canonical(false)]
lat_meet_sqsubseteq_l (X Y : lat_ty) : X Y X;
#[canonical(false)]
lat_meet_sqsubseteq_r (X Y : lat_ty) : X Y Y;
#[canonical(false)]
lat_meet_glb (X Y Z : lat_ty) : X Y X Z X Y Z
}.
Arguments lat_equiv : simpl never.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment