From 347ae8ede09e05420ba799d721ab3e45d5b16041 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Mon, 16 Dec 2024 18:31:06 +0100
Subject: [PATCH] bump
---
_CoqProject | 18 ++++++++++++++++--
semantics.opam | 6 +++---
.../program_logics/program_logic/adequacy.v | 2 +-
3 files changed, 20 insertions(+), 6 deletions(-)
diff --git a/_CoqProject b/_CoqProject
index 8643da2..189ee01 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -63,6 +63,7 @@ theories/type_systems/systemf_mu_state/locations.v
theories/type_systems/systemf_mu_state/lang.v
theories/type_systems/systemf_mu_state/notation.v
theories/type_systems/systemf_mu_state/types.v
+theories/type_systems/systemf_mu_state/types_sol.v
theories/type_systems/systemf_mu_state/tactics.v
theories/type_systems/systemf_mu_state/execution.v
theories/type_systems/systemf_mu_state/parallel_subst.v
@@ -106,7 +107,8 @@ theories/program_logics/logrel/ghost_state.v
# resources
theories/program_logics/ra_lib.v
theories/program_logics/resource_algebras_1.v
-#theories/program_logics/resource_algebras_2.v
+theories/program_logics/resource_algebras_2.v
+theories/program_logics/resource_algebras_sol.v
theories/program_logics/fupd.v
@@ -122,17 +124,28 @@ theories/program_logics/reloc/fundamental.v
theories/program_logics/reloc/adequacy.v
theories/program_logics/reloc/contextual_refinement.v
+theories/program_logics/reloc_sol/ghost_state.v
+theories/program_logics/reloc_sol/src_rules.v
+theories/program_logics/reloc_sol/persistent_bipred.v
+theories/program_logics/reloc_sol/notation.v
+theories/program_logics/reloc_sol/proofmode.v
+theories/program_logics/reloc_sol/syntactic.v
+theories/program_logics/reloc_sol/logrel.v
+theories/program_logics/reloc_sol/fundamental.v
+theories/program_logics/reloc_sol/adequacy.v
+theories/program_logics/reloc_sol/contextual_refinement.v
# concurrency
theories/program_logics/concurrency.v
theories/program_logics/concurrent_logrel/syntactic.v
theories/program_logics/concurrent_logrel/logrel.v
+theories/program_logics/concurrent_logrel/logrel_sol.v
theories/program_logics/concurrent_logrel/adequacy.v
-
# By removing the # below, you can add the exercise sheets to make
# <comment-out>
theories/type_systems/warmup/warmup.v
+theories/type_systems/warmup/warmup_sol.v
theories/type_systems/stlc/exercises01.v
theories/type_systems/stlc/exercises02.v
theories/type_systems/stlc/cbn_logrel.v
@@ -141,4 +154,5 @@ theories/type_systems/systemf/exercises04.v
theories/type_systems/systemf/exercises05.v
theories/type_systems/systemf_mu/exercises06.v
theories/type_systems/systemf_mu_state/exercises07.v
+theories/type_systems/systemf_mu_state/exercises07_sol.v
# </comment-out>
diff --git a/semantics.opam b/semantics.opam
index 5649e4c..de21438 100644
--- a/semantics.opam
+++ b/semantics.opam
@@ -9,9 +9,9 @@ bug-reports: "https://gitlab.mpi-sws.org/FP/semantics-course/issues"
version: "dev"
depends: [
- "coq" { (>= "8.18" & < "8.20~") | (= "dev") }
- "coq-iris-heap-lang" { (= "dev.2024-08-20.0.657b34ad") | (= "dev") }
- "coq-equations" { (= "1.3+8.18") | = "1.3+8.19" }
+ "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2024-12-06.1.72e683c9") | (= "dev") }
+ "coq-equations" { (= "1.3+8.19") | (= "1.3+8.20") }
"coq-autosubst" { (= "1.8") | (= "dev") }
]
diff --git a/theories/program_logics/program_logic/adequacy.v b/theories/program_logics/program_logic/adequacy.v
index 499558f..ef05f67 100644
--- a/theories/program_logics/program_logic/adequacy.v
+++ b/theories/program_logics/program_logic/adequacy.v
@@ -94,7 +94,7 @@ Proof.
iIntros (Hstep) "Hσ He". iMod (wptp_steps with "Hσ He") as "Hwp"; first done.
iModIntro. iApply (step_fupdN_wand with "Hwp").
iMod 1 as "(Hσ & Ht & $ & $)"; simplify_eq/=.
- iMod (fupd_plain_keep_l ∅
+ iMod (fupd_plain_keep_l _ ∅
⌜ ∀ e2, s = NotStuck → e2 ∈ es2 → not_stuck e2 σ2 ⌝%I
(state_interp σ2 ∗
wptp s es2 (Φs))%I
--
GitLab