Update CI; update InteractionTrees submodule

PrincetonUniversity · Jan 6, 2025 · d7d4c98 · d7d4c98
1 parent 380e641
commit d7d4c98
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 8 deletions.
diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml
@@ -21,16 +21,16 @@ jobs:
         # except for the "make_target" field and make_target related excludes
         coq_version:
           # See https://github.com/coq-community/docker-coq/wiki for supported images
-          - '8.18'
           - '8.19'
+          - '8.20'
           - 'dev'
         bit_size:
           - 32
           - 64
         make_target:
           - vst
         exclude:   
-          - coq_version: 8.18
+          - coq_version: 8.19
             bit_size: 32
           - coq_version: dev
             bit_size: 32
@@ -88,9 +88,8 @@ jobs:
       fail-fast: false
       matrix:
         coq_version:
-#          - '8.17'
-          - '8.18'
           - '8.19'
+          - '8.20'
           - 'dev' 
         make_target:
           - assumptions.txt
@@ -103,9 +102,7 @@ jobs:
           - 32
           - 64
         exclude:
-#          - coq_version: 8.17
-#            bit_size: 32
-          - coq_version: 8.18
+          - coq_version: 8.19
             bit_size: 32
           - coq_version: dev
             bit_size: 32

diff --git a/InteractionTrees b/InteractionTrees
+6 −0		.circleci/config.yml
+7 −0		CHANGELOG.md
+1 −1		_CoqProject.itree
+2 −1		coq-itree-extra.opam
+3 −2		coq-itree.opam
+2 −2		dune-project
+4 −5		extra/Dijkstra/ITreeDijkstra.v
+16 −17		extra/ITrace/ITraceBind.v
+3 −2		extra/ITrace/ITraceFacts.v
+3 −2		extra/ITrace/ITracePrefix.v
+1 −1		extra/Secure/Labels.v
+1 −1		extra/Secure/SecureEqHalt.v
+0 −391		secure_example/Utils_tutorial.v
+2 −0		theories/Basics/Basics.v
+2 −3		theories/Basics/CategoryRelations.v
+70 −36		theories/Basics/CategoryTheory.v
+15 −8		theories/Basics/HeterogeneousRelations.v
+13 −0		theories/Basics/Utils.v
+2 −2		theories/Core/KTreeFacts.v
+1 −1		theories/Eq/Eqit.v
+4 −4		theories/Eq/EuttExtras.v
+1 −1		theories/Eq/Rutt.v
+1 −1		theories/Eq/SimUpToTaus.v
+1 −1		theories/Eq/UpToTaus.v
+1 −1		theories/Events/FailFacts.v
+3 −2		theories/Events/Writer.v
+1 −1		theories/ITreeFacts.v
+1 −1		theories/Interp/RecursionFacts.v
+1 −1		theories/Interp/Traces.v
+1 −1		theories/Props/Finite.v
+1 −1		theories/Props/HasPost.v
+1 −1		theories/Props/Leaf.v
+1 −1		tutorial/Imp.v
+0 −391		tutorial/Utils_tutorial.v