Fix depgraph

.github/workflows/docker-action.yml

@@ -17,8 +17,8 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'coqorg/coq:8.14'
-          - 'coqorg/coq:8.15'
+          - 'coqorg/coq:8.14-ocaml-4.14-flambda'
+          - 'coqorg/coq:8.15-ocaml-4.14-flambda'
           - 'coqorg/coq:8.16'
           - 'coqorg/coq:8.17'
           - 'coqorg/coq:8.18'

Makefile

@@ -49,21 +49,19 @@ _CoqProject: $(COQPATHFILE) _CoqProject.itree _CoqProject.extra Makefile
 	@ echo "# Generating _CoqProject"
 	@ rm -f _CoqProject
 	@ echo "# THIS IS AN AUTOMATICALLY GENERATED FILE" >> _CoqProject
-	@ echo "# PLEASE EDIT _CoqConfig INSTEAD" >> _CoqProject
+	@ echo "# PLEASE EDIT _CoqProject.itree or _CoqPRoject.extra INSTEAD" >> _CoqProject
 	@ echo >> _CoqProject
 ifneq ("$(COQPATHFILE)","")
 	@ echo "# including: _CoqPath"
 	@ cat _CoqPath >> _CoqProject
 	@ echo >> _CoqProject
 endif
-	@ echo "# including: _CoqConfig"
+	@ echo "# including: _CoqProject.itree _CoqProject.extra"
 	@ cat _CoqProject.itree _CoqProject.extra >> _CoqProject
 
 COQDEP=coqdep
 DEPS_DOT=deps.dot
 DEPS_OUT=deps.jpg
 
 depgraph:
-	$(COQDEP) -dumpgraph $(DEPS_DOT) $(shell cat _CoqConfig) > /dev/null 2>&1
-	sed 's%\("theories/\([^"]*\)/\([^"/]*\)"\[label="\)%\1\2/\\n%' -i $(DEPS_DOT)
-	dot $(DEPS_DOT) -Tjpg -o$(DEPS_OUT)
+	sh depgraph.sh

depgraph.sh

@@ -0,0 +1,15 @@
+# Script adapted from https://discourse.rocq-prover.org/t/tool-for-drawing-coq-project-dependency-graph/653/16
+( echo "digraph interval_deps {" ;
+  echo "node [shape=ellipse, style=filled, URL=\"html/ITree.html\"];";
+  ( coqdep $(cat _CoqProject.itree) ) |
+    sed -n -e 's,theories/,,g;s,[^ ]*worker,,g;s,/,.,g;s/[.]vo.*: [^ ]*[.]v//p' |
+    while read src dst; do
+      color=$(echo "$src" | sed -e 's,Eq.*,turquoise,;s,Basics[.].*,plum,;s,Handler.*,lightcoral,;s,Core.*,yellow,;s,Indexed.*,cornflowerblue,;s,Interp.*,green,;s,Events.*,orange,;s,Props.*,olive,;s,[A-Z].*,white,')
+      echo "\"$src\" [fillcolor=$color];"
+      for d in $dst; do
+        echo "\"$src\" -> \"${d%.vo}\" ;"
+      done
+    done;
+  echo "}" ) | tred > deps.dot
+dot -T png deps.dot > deps.png
+# dot -T cmap deps.dot | sed -e 's,>$,/>,' > deps.map

theories/Events/Exception.v

@@ -1,7 +1,7 @@
 (** * Exception event *)
 
 (* begin hide *)
-From ITree Require Import ITree.
+From ITree Require Import Basics.Basics Core.ITreeDefinition Core.Subevent Indexed.Sum.
 
 Set Implicit Arguments.
 (* end hide *)