cherry-picking the dependency graph building recipe

.github/workflows/build.yml

@@ -56,6 +56,11 @@ jobs:
         # to avoid a warning at cleanup time
         if: ${{ always() }}
         run: sudo chown -R 1001:116 .  # <--
+      - name: Install graphviz
+        uses: ts-graphviz/setup-graphviz@v1
+
+      - name: Build dependency graph
+        run: make depgraph
 
       - name: Build doc overview
         uses: docker://pandoc/core:2.9

.gitignore

@@ -16,3 +16,5 @@ Makefile.coq.conf
 *.cache
 
 _opam
+
+*.dot

Makefile.coq.local

@@ -1,4 +1,4 @@
-#Taken from https://github.com/coq-community/reglang
+#Inspired from https://github.com/coq-community/reglang
 
 GLOBFILES = $(VFILES:.v=.glob)
 COQDOCJS_DIR ?= coqdocjs
@@ -22,4 +22,13 @@ coqdoc: $(GLOBFILES) $(VFILES) $(HEADER) $(FOOTER) $(RESOURCES) $(FRONTPAGE)
 .PHONY: coqdoc
 
 clean::
-	$(HIDE)rm -rf $(COQDOCDIR)
+	$(HIDE)rm -rf $(COQDOCDIR)/*.html
+
+$(DOCDIR)/dependency_graph.dot: $(VFILES)
+	coqdep -Q theories LogRel -R coq-partialfun/theories PartialFun $(VFILES) | perl generate_deps.pl | tred > $(DOCDIR)/dependency_graph.dot
+
+$(DOCDIR)/dependency_graph.png: $(DOCDIR)/dependency_graph.dot
+	dot -T png $(DOCDIR)/dependency_graph.dot -o $(DOCDIR)/dependency_graph.png
+
+depgraph: $(DOCDIR)/dependency_graph.png
+.PHONY: depgraph

docs/index.md

@@ -1,7 +1,7 @@
 Browsing the sources
 ============================
 
-The table of content of the development is accessible [here](./coqdoc/toc.html).
+The full table of content of the development is accessible [here](https://coqhott.github.io/logrel-coq/coqdoc/toc.html).
 
 File description
 ==========

generate_deps.pl

@@ -0,0 +1,28 @@
+print "digraph logrel_deps {\n";
+print "  node [shape = ellipse,style=filled];\n";
+print "  subgraph cluster_autosubst { label=\"AutoSubst\" \n}";
+print "  subgraph cluster_logrel { label=\"LogicalRelation\" \n}";
+print "  subgraph cluster_subst { label=\"Validity\" \n}";
+print "  subgraph cluster_dec { label=\"Decidability\" \n}";
+while (<>) {
+  if (m/.*?theories\/([^\s]*)\.vo.*:(.*)/) {
+    $dests = $2 ;
+    ($path,$src) = ($1 =~ s/\//\./rg =~ m/(.*\.)?([^.]*)$/);
+    if ($path =~ m/AutoSubst\./) {
+      print "subgraph cluster_autosubst { \"$path$src\"[label=\"$src\",fillcolor=firebrick]}"
+    }elsif ($path =~ m/LogicalRelation\./) {
+      print "subgraph cluster_logrel { \"$path$src\"[label=\"$src\",fillcolor=forestgreen]}"
+    }elsif ($path =~ m/Substitution\./) {
+      print "subgraph cluster_subst { \"$path$src\"[label=\"$src\",fillcolor=goldenrod1]}"
+    }elsif ($path =~ m/Decidability\./) {
+      print "subgraph cluster_dec { \"$path$src\"[label=\"$src\",fillcolor=deeppink3]}"
+    }else {
+      print "\"$path$src\"[label=\"$src\",fillcolor=dodgerblue1]"
+    }
+    for my $dest (split(" ", $dests)) {
+      $dest =~ s/\//\./g ;
+      print "  \"$1\" -> \"$path$src\";\n" if ($dest =~ m/theories\.(.*)\.vo/);
+    }
+  }
+}
+print "}\n";

theories/AlgorithmicTyping.v

@@ -1,7 +1,7 @@
 (** * LogRel.AlgorithmicTyping: definition of algorithmic conversion and typing. *)
 From Coq Require Import ssrbool.
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
-From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening UntypedReduction GenericTyping DeclarativeTyping.
+From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening UntypedReduction GenericTyping.
 
 Section Definitions.
 

theories/Decidability/Functions.v

@@ -2,7 +2,7 @@
 From Coq Require Import Nat Lia List.
 From Equations Require Import Equations.
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
-From LogRel Require Import Utils BasicAst Context DeclarativeTyping.
+From LogRel Require Import Utils BasicAst Context.
 From PartialFun Require Import Monad PartialFun.
 
 Import MonadNotations.

theories/Decidability/Soundness.v

@@ -2,12 +2,14 @@
 From Coq Require Import Nat List Lia Arith ssrbool.
 From Equations Require Import Equations.
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
+From LogRel Require Import Utils BasicAst Context Notations UntypedReduction GenericTyping NormalForms.
+From LogRel Require Import AlgorithmicTyping.
 From LogRel Require Import Utils BasicAst Context Notations UntypedReduction DeclarativeTyping DeclarativeInstance GenericTyping NormalForms.
 From LogRel Require Import Validity LogicalRelation Fundamental DeclarativeSubst TypeConstructorsInj AlgorithmicTyping BundledAlgorithmicTyping Normalisation TypeUniqueness.
 From LogRel.Decidability Require Import Functions.
 From PartialFun Require Import Monad PartialFun.
 
-Import DeclarativeTypingProperties.
+Import AlgorithmicTypingData.
 Import IndexedDefinitions.
 
 Set Universe Polymorphism.
@@ -293,8 +295,6 @@ Ltac funelim_typing :=
 
 Section TypingCorrect.
 
-  Import AlgorithmicTypingData.
-
   #[local]Existing Instance ty_errors.
 
   Lemma ty_view1_small_can T n : build_ty_view1 T = ty_view1_small n -> ~ isCanonical T.