Bump to Coq 8.19.1 and new gpfsl

.gitlab-ci.yml

@@ -28,10 +28,10 @@ variables:
 
 ## Build jobs
 
-build-coq.8.18.0:
+build-coq.8.19.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.18.0"
+    OPAM_PINS: "coq version 8.19.1"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
   tags:

README.md

@@ -6,7 +6,7 @@ This is the Coq development accompanying RBrlx.
 
 This version is known to compile with:
 
- - Coq 8.18.0
+ - Coq 8.19.1
  - A development version of [GPFSL].
 
 ## Building from source
@@ -216,4 +216,4 @@ The verification of Full Arc is split into 2 parts:
   mismatches.
 
   [GPFSL]: https://gitlab.mpi-sws.org/iris/gpfsl/
-  [ORC11]: https://gitlab.mpi-sws.org/iris/orc11/
+  [ORC11]: https://gitlab.mpi-sws.org/iris/gpfsl/-/tree/master/orc11

coq-lambda-rust.opam

@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2024-09-10.1.5365229f") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2024-10-03.0.023610f8") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

theories/typing/programs.v

@@ -15,7 +15,7 @@ Section typing.
     (∀ tid (qmax : Qp), ⎡lft_ctx⎤ -∗ elctx_interp E -∗ na_own tid ⊤ -∗ llctx_interp qmax L -∗
                cctx_interp tid qmax C -∗ tctx_interp tid T -∗
                WP e @ tid; ⊤ {{ _, cont_postcondition }})%I.
-  Global Arguments typed_body _ _ _ _ _%E.
+  Global Arguments typed_body _ _ _ _ _%_E.
 
   Global Instance typed_body_llctx_permut E :
     Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> (⊢)) (typed_body E).
@@ -64,7 +64,7 @@ Section typing.
               llctx_interp qmax L -∗ tctx_interp tid T1 -∗
        WP e @ tid; ⊤ {{ v, na_own tid ⊤ ∗
                          llctx_interp qmax L ∗ tctx_interp tid (T2 v) }})%I.
-  Global Arguments typed_instruction _ _ _ _%E _.
+  Global Arguments typed_instruction _ _ _ _%_E _.
 
   (** Writing and Reading **)
   Definition typed_write_def (E : elctx) (L : llctx) (ty1 ty ty2 : type) : vPropI Σ :=
@@ -76,7 +76,7 @@ Section typing.
   Definition typed_write_aux : seal (@typed_write_def). Proof. by eexists. Qed.
   Definition typed_write := typed_write_aux.(unseal).
   Definition typed_write_eq : @typed_write = @typed_write_def := typed_write_aux.(seal_eq).
-  Global Arguments typed_write _ _ _%T _%T _%T.
+  Global Arguments typed_write _ _ _%_T _%_T _%_T.
 
   Global Instance typed_write_persistent (E : elctx) (L : llctx) (ty1 ty ty2 : type) :
     Persistent (typed_write E L ty1 ty ty2).
@@ -97,7 +97,7 @@ Section typing.
   Definition typed_read_aux : seal (@typed_read_def). Proof. by eexists. Qed.
   Definition typed_read := typed_read_aux.(unseal).
   Definition typed_read_eq : @typed_read = @typed_read_def := typed_read_aux.(seal_eq).
-  Global Arguments typed_read _ _ _%T _%T _%T.
+  Global Arguments typed_read _ _ _%_T _%_T _%_T.
 
   Global Instance typed_read_persistent (E : elctx) (L : llctx) (ty1 ty ty2 : type) :
     Persistent (typed_read E L ty1 ty ty2).
@@ -107,11 +107,11 @@ End typing.
 Definition typed_instruction_ty `{!typeG Σ} (E : elctx) (L : llctx) (T : tctx)
     (e : expr) (ty : type) : vPropI Σ :=
   typed_instruction E L T e (λ v, [v ◁ ty]).
-Arguments typed_instruction_ty {_ _} _ _ _ _%E _%T.
+Arguments typed_instruction_ty {_ _} _ _ _ _%_E _%_T.
 
 Definition typed_val `{!typeG Σ} (v : val) (ty : type) : Prop :=
   ∀ E L, ⊢ typed_instruction_ty E L [] (of_val v) ty.
-Arguments typed_val _ _ _%V _%T.
+Arguments typed_val _ _ _%_V _%_T.
 
 Section typing_rules.
   Context `{!typeG Σ}.