another attempt at setting up the CI

This is a PR-specific hack and should be replaced once Iris is a standard dependency.
PrincetonUniversity · Mar 19, 2024 · 3eb4c5e · 3eb4c5e
1 parent 5dc8fd7
commit 3eb4c5e
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 5 deletions.
diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml
@@ -56,8 +56,11 @@ jobs:
               opam install -y ${{ matrix.coq_version == 'dev' && 'coq-flocq' || matrix.bit_size == 32 && 'coq-compcert-32.3.13' || 'coq-compcert.3.13' }}
               # Required by test2
               opam install -y coq-ext-lib
-              echo ${{ github.ref_name }}
-              opam install -y ${{ github.ref_name == 'vst_on_iris' && 'coq-iris.dev.2023-05-31.0.a22a81c2' || '' }}
+              if [ ${{ github.ref_name }} = '755/merge']
+              then
+                opam repo add -y iris-dev https://gitlab.mpi-sws.org/iris/opam.git
+                opam install -y coq-iris.dev.2023-05-31.0.a22a81c2
+              fi
             endGroup
           # See https://github.com/coq-community/docker-coq-action/tree/v1#permissions
           before_script: |

diff --git a/floyd/io_events.v b/floyd/io_events.v
@@ -48,6 +48,7 @@ Lemma has_ext_ITREE : forall tr, has_ext tr ⊢ ITREE tr.
 Proof.
   intro; unfold ITREE.
   Exists tr; entailer!.
+  reflexivity.
 Qed.
 
 Lemma ITREE_impl' : forall tr tr', sutt eq tr' tr ->

diff --git a/progs64/verif_io.v b/progs64/verif_io.v
@@ -182,10 +182,9 @@ Proof.
   forward.
   forward_while (∃ i : int, PROP (Int.signed i = -1 \/ Int.signed i = Byte.unsigned c) LOCAL (temp _r (Vint i); temp _c (Vubyte c))
     SEP (ITREE (if eq_dec (Int.signed i) (-1) then (r <- write stdout c;; k) else k))).
-  - Exists (Int.neg (Int.repr 1)); entailer!.
+  - Exists (Int.neg (Int.repr 1)); simpl; entailer!.
   - entailer!.
-  - subst; rewrite -> Int.signed_repr by rep_lia.
-    rewrite -> if_true by auto.
+  - subst; rewrite -> if_true by auto.
     forward_call (c, k).
     Intros i.
     forward.