Put InteractionTree back as submodule

Author: andrew-appel

.github/workflows/coq-action.yml

@@ -27,6 +27,9 @@ jobs:
           - 64
         make_target:
           - vst
+        exclude:
+	  - coq_version: dev
+	    bit_size: 32
     steps:
       - uses: actions/checkout@v4
         with:

Makefile

@@ -303,10 +303,10 @@ CGFLAGS =  -DCOMPCERT -short-idents
 
 # ##### Interaction Trees Flags #####
 
-# the following commented out, because we get from opam instead of submodules
-# ifneq ($(wildcard InteractionTrees/theories),)
-# EXTFLAGS:=$(EXTFLAGS) -Q InteractionTrees/theories ITree
-# endif
+# as of 1 July 2025, coq-itree package seems not compatible with rocq 9.2+alpha, so still using submodule
+ifneq ($(wildcard InteractionTrees/theories),)
+EXTFLAGS:=$(EXTFLAGS) -Q InteractionTrees/theories ITree
+endif
 
 # ##### FCF (Foundational Cryptography Framework) Flags #####
 
@@ -329,9 +329,9 @@ endif
 
 # ##### Flag summary #####
 
-COQFLAGS=$(foreach d, $(VSTDIRS), $(if $(wildcard $(d)), -Q $(d) VST.$(d))) $(foreach d, $(OTHERDIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS) $(SHIM) # -Q ../stdpp/theories stdpp -Q ../iris/iris iris -Q ../fcf/src/fcf FCF
+COQFLAGS=$(foreach d, $(VSTDIRS), $(if $(wildcard $(d)), -Q $(d) VST.$(d))) $(foreach d, $(OTHERDIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS) $(SHIM) # -Q ../stdpp/theories stdpp -Q ../iris/iris iris -Q ../InteractionTrees/theories ITree -Q ../fcf/src/fcf FCF
 
-# old version with InteractionTrees, paco, coq-ext-lib; we now obtain these from opam environment instead of submodules
+# old version with paco, coq-ext-lib; we now obtain these from opam environment instead of submodules
 # COQFLAGS=$(foreach d, $(VSTDIRS), $(if $(wildcard $(d)), -Q $(d) VST.$(d))) $(foreach d, $(OTHERDIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS) $(SHIM) # -Q ../stdpp/theories stdpp -Q ../iris/iris iris -Q ../InteractionTrees/theories ITree -Q ../paco/src Paco -Q ../coq-ext-lib/theories ExtLib -Q ../fcf/src/fcf FCF
 
 
@@ -929,10 +929,10 @@ endif
 # 	$(COQDEP) -Q coq-ext-lib/theories ExtLib coq-ext-lib/theories >>.depend
 # endif
 
+ifneq ($(wildcard InteractionTrees/theories),)
+	$(COQDEP) -Q InteractionTrees/theories ITree InteractionTrees/theories >>.depend
+endif
 # the following commented out, because we get from opam instead of submodules
-# ifneq ($(wildcard InteractionTrees/theories),)
-# 	$(COQDEP) -Q paco/src Paco -Q InteractionTrees/theories ITree InteractionTrees/theories >>.depend
-# endif
 # ifneq ($(wildcard paco/src),)
 # 	$(COQDEP) -Q paco/src Paco paco/src/*.v >>.depend
 # endif

progs/io_combine.v

@@ -11,7 +11,7 @@ Require Import VST.concurrency.conclib.
 Require Import VST.sepcomp.semantics.
 Require Import ITree.ITree.
 Require Import ITree.Interp.Traces.
-Require Import Ensembles.
+From Stdlib Require Import Ensembles.
 Require Import VST.progs.io_specs.
 Require Import VST.progs.io_dry.
 Require Import VST.progs.io_os_specs.

progs/io_os_connection.v

@@ -1,6 +1,6 @@
-Require Import List.
-Require Import ZArith.
-Require Import Psatz.
+From Stdlib Require Import List.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import Psatz.
 Require Import ITree.ITree.
 Require Import ITree.Interp.Traces.
 Require Import compcert.lib.Maps.
@@ -15,6 +15,9 @@ Require Import VST.progs.io_os_specs.
 Require Import VST.zlist.sublist.
 Require Import VST.progs.os_combine.
 Import ExtLib.Structures.Monad.
+From Stdlib Require Import FinFun.
+
+Opaque eq_dec.eq_dec.
 
 Local Ltac inj :=
   repeat match goal with
@@ -567,15 +570,15 @@ Section Invariants.
     NoDup (mkRecvEvents logIdx cs).
   Proof.
     unfold mkRecvEvents, enumerate; intros.
-    apply FinFun.Injective_map_NoDup; auto using combine_NoDup, seq_NoDup.
+    apply Injective_map_NoDup; auto using combine_NoDup, seq_NoDup.
     red; intros (? & ?) (? & ?); intros; inj; auto.
   Qed.
 
   Lemma Zlength_enumerate {A} : forall (xs : list A),
     Zlength (enumerate xs) = Zlength xs.
   Proof.
     unfold enumerate; intros.
-    rewrite Zlength_combine, !Zlength_correct, seq_length; lia.
+    rewrite Zlength_combine, !Zlength_correct, length_seq; lia.
   Qed.
 
   Lemma seq_nth_app : forall len start n pre post,
@@ -585,7 +588,7 @@ Section Invariants.
     intros * Heq.
     enough (n = nth (length pre) (seq start len) O); subst.
     { rewrite Heq, app_nth2, Nat.sub_diag, seq_nth; auto; cbn.
-      rewrite <- (seq_length len start), Heq, length_app; cbn; lia.
+      rewrite <- (length_seq len start), Heq, length_app; cbn; lia.
     }
     rewrite Heq, app_nth2, Nat.sub_diag; auto.
   Qed.
@@ -599,7 +602,7 @@ Section Invariants.
     rewrite combine_fst, map_app in Heq; cbn in Heq.
     apply seq_nth_app in Heq; subst; cbn; auto using length_map.
     rewrite <- Nat2Z.id, <- Zlength_length; rewrite <- Zlength_correct.
-    - rewrite !Zlength_correct, seq_length; auto.
+    - rewrite !Zlength_correct, length_seq; auto.
     - apply Zlength_nonneg.
   Qed.
 
@@ -1913,7 +1916,7 @@ Import functional_base.
       split; auto; cbn in *.
       rewrite Int.signed_repr by (cbn; lia).
       destruct (Coqlib.zeq z1 (-1)); subst; auto.
-      if_tac; try easy.
+      destruct (eq_dec.eq_dec _ _); try easy.
       rewrite Zle_imp_le_bool by lia.
       destruct Hput as (? & [(? & ?) | (? & ?)]); subst; auto; try lia.
       rewrite Zmod_small; auto; functional_base.rep_lia.