From 0c15131623390cb84505251b3c00fa1a90fefa2f Mon Sep 17 00:00:00 2001
From: Meven Lennon-Bertrand <58942857+MevenBertrand@users.noreply.github.com>
Date: Tue, 5 Sep 2023 09:27:28 +0100
Subject: [PATCH] Dependency graph generation (#39)

* add a recipe for generating a dependency graph

* dependency graph in the right folder

* documentation

* useless dependency

* rebase dependency graph

* add dependency graph generation to CI

* fix CI

---------

Co-authored-by: Yannick Forster <yannick.forster@inria.fr>
---
 .github/workflows/build.yml                 |  5 ++++
 .gitignore                                  |  2 ++
 Makefile.coq.local                          | 13 ++++++++--
 README.md                                   |  8 +++---
 docs/index.md                               |  6 +----
 generate_deps.pl                            | 28 +++++++++++++++++++++
 theories/AlgorithmicTyping.v                |  2 +-
 theories/Consequences.v                     |  2 ++
 theories/Decidability/Functions.v           |  2 +-
 theories/Decidability/Soundness.v           | 10 +++-----
 theories/DeclarativeInstance.v              |  2 +-
 theories/DeclarativeSubst.v                 |  2 +-
 theories/LogicalRelation/Weakening.v        |  2 +-
 theories/Normalisation.v                    |  4 +--
 theories/Substitution/Introductions/Pi.v    |  2 +-
 theories/Substitution/Introductions/Poly.v  |  2 +-
 theories/Substitution/Introductions/Sigma.v |  2 +-
 theories/Substitution/Properties.v          |  2 +-
 theories/TypeConstructorsInj.v              |  2 +-
 theories/UntypedValues.v                    |  2 +-
 20 files changed, 70 insertions(+), 30 deletions(-)
 create mode 100644 generate_deps.pl

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 5acdf5f..963fc10 100644
--- a/.github/workflows/build.yml
+++ b/.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
diff --git a/.gitignore b/.gitignore
index b187098..b1ef404 100644
--- a/.gitignore
+++ b/.gitignore
@@ -16,3 +16,5 @@ Makefile.coq.conf
 *.cache
 
 _opam
+
+*.dot
\ No newline at end of file
diff --git a/Makefile.coq.local b/Makefile.coq.local
index 328f452..d7187c1 100644
--- a/Makefile.coq.local
+++ b/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
\ No newline at end of file
diff --git a/README.md b/README.md
index c336ce4..bdd5d87 100644
--- a/README.md
+++ b/README.md
@@ -15,10 +15,12 @@ Building
 
 The project builds with Coq version `8.16.1`. It needs the opam package `coq-smpl`. Once these have been installed, you can simply issue `make` in the root folder.
 
-Browsing the Development
+The `make depgraph` recipe can be used to generate the [dependency graph](https://coqhott.github.io/logrel-coq/dependency_graph.png).
+
+Browsing the development
 ==================
 
-The development, rendered using `coqdoc`, can be [browsed online](https://coqhott.github.io/logrel-coq/coqdoc/toc.html).
+The development, rendered using `coqdoc`, can be [browsed online](https://coqhott.github.io/logrel-coq/). A dependency graph for the project is available [here](https://coqhott.github.io/logrel-coq/dependency_graph.png).
 
 Syntax (re)generation
 ============
@@ -30,7 +32,7 @@ re-generating the syntax.
 - change the imports at the beginning of the files;
 - add the `#[global]` keyword to all instances.
 
-Getting Started
+Getting started with using the development
 =================
 
 A few things to get accustomed to if you want to use the development.
diff --git a/docs/index.md b/docs/index.md
index 03297fa..2f156a6 100644
--- a/docs/index.md
+++ b/docs/index.md
@@ -1,11 +1,7 @@
 Browsing the sources
 ============================
 
-The table of content of the development is accessible [here](https://coqhott.github.io/logrel-coq/coqdoc/toc.html).
-
-File description
-==========
-
+The full table of content of the development is accessible [here](https://coqhott.github.io/logrel-coq/coqdoc/toc.html).
 To complement it, here is a rough description of the content of every file.
 
 Utilities and AST
diff --git a/generate_deps.pl b/generate_deps.pl
new file mode 100644
index 0000000..ead6235
--- /dev/null
+++ b/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";
\ No newline at end of file
diff --git a/theories/AlgorithmicTyping.v b/theories/AlgorithmicTyping.v
index bce1f97..e8d5426 100644
--- a/theories/AlgorithmicTyping.v
+++ b/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.
 
diff --git a/theories/Consequences.v b/theories/Consequences.v
index c090a1d..3a9a45a 100644
--- a/theories/Consequences.v
+++ b/theories/Consequences.v
@@ -40,6 +40,8 @@ Proof.
   eapply empty_isEmpty; tea.
 Qed.
 
+Print Assumptions consistency.
+
 (** *** Canonicity: every closed natural number is a numeral, i.e. an iteration of [tSucc] on [tZero]. *)
 
 Section NatCanonicityInduction.
diff --git a/theories/Decidability/Functions.v b/theories/Decidability/Functions.v
index 8be02fa..61994fb 100644
--- a/theories/Decidability/Functions.v
+++ b/theories/Decidability/Functions.v
@@ -2,7 +2,7 @@
 From Coq Require Import Nat Lia.
 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.
diff --git a/theories/Decidability/Soundness.v b/theories/Decidability/Soundness.v
index e11a813..d7e5cbe 100644
--- a/theories/Decidability/Soundness.v
+++ b/theories/Decidability/Soundness.v
@@ -2,12 +2,12 @@
 From Coq Require Import Nat Lia Arith.
 From Equations Require Import Equations.
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
-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.
+From LogRel Require Import Utils BasicAst Context Notations UntypedReduction GenericTyping NormalForms.
+From LogRel Require Import AlgorithmicTyping.
 From LogRel.Decidability Require Import Functions.
 From PartialFun Require Import Monad PartialFun.
 
-Import DeclarativeTypingProperties.
+Import AlgorithmicTypingData.
 Import IndexedDefinitions.
 
 Set Universe Polymorphism.
@@ -155,8 +155,6 @@ Ltac funelim_conv :=
 
 Section ConversionSound.
 
-  Import AlgorithmicTypingData.
-
   #[local]Existing Instance ty_errors.
 
   #[universes(polymorphic)]Definition conv_sound_type
@@ -226,8 +224,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.
diff --git a/theories/DeclarativeInstance.v b/theories/DeclarativeInstance.v
index 74a55dc..8292c57 100644
--- a/theories/DeclarativeInstance.v
+++ b/theories/DeclarativeInstance.v
@@ -1,7 +1,7 @@
 (** * LogRel.DeclarativeInstance: proof that declarative typing is an instance of generic typing. *)
 From Coq Require Import CRelationClasses.
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
-From LogRel Require Import Utils BasicAst Notations Context NormalForms UntypedReduction UntypedValues Weakening GenericTyping DeclarativeTyping.
+From LogRel Require Import Utils BasicAst Notations Context NormalForms UntypedReduction Weakening GenericTyping DeclarativeTyping.
 
 Import DeclarativeTypingData.
 
diff --git a/theories/DeclarativeSubst.v b/theories/DeclarativeSubst.v
index 61641a5..801c5aa 100644
--- a/theories/DeclarativeSubst.v
+++ b/theories/DeclarativeSubst.v
@@ -2,7 +2,7 @@
 From Coq Require Import CRelationClasses.
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
 From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening UntypedReduction
-  GenericTyping DeclarativeTyping DeclarativeInstance AlgorithmicTyping.
+  GenericTyping DeclarativeTyping DeclarativeInstance.
 From LogRel Require Import LogicalRelation Validity Fundamental.
 From LogRel.LogicalRelation Require Import Induction Escape Irrelevance Transitivity.
 From LogRel.Substitution Require Import Properties Irrelevance.
diff --git a/theories/LogicalRelation/Weakening.v b/theories/LogicalRelation/Weakening.v
index c63425f..e1692c1 100644
--- a/theories/LogicalRelation/Weakening.v
+++ b/theories/LogicalRelation/Weakening.v
@@ -1,6 +1,6 @@
 From Coq Require Import ssrbool.
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
-From LogRel Require Import Notations Utils BasicAst Context NormalForms UntypedValues Weakening GenericTyping LogicalRelation.
+From LogRel Require Import Notations Utils BasicAst Context NormalForms Weakening GenericTyping LogicalRelation.
 From LogRel.LogicalRelation Require Import Induction Irrelevance Transitivity Escape.
 
 Set Universe Polymorphism.
diff --git a/theories/Normalisation.v b/theories/Normalisation.v
index 8705677..7504e3a 100644
--- a/theories/Normalisation.v
+++ b/theories/Normalisation.v
@@ -2,8 +2,8 @@
 From Coq Require Import CRelationClasses.
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
 From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening UntypedReduction
-  GenericTyping DeclarativeTyping DeclarativeInstance AlgorithmicTyping.
-From LogRel Require Import LogicalRelation UntypedValues Validity Fundamental.
+  GenericTyping DeclarativeTyping DeclarativeInstance.
+From LogRel Require Import LogicalRelation Validity Fundamental AlgorithmicTyping.
 From LogRel.LogicalRelation Require Import Escape Neutral Induction ShapeView Reflexivity.
 From LogRel.Substitution Require Import Escape Poly.
 
diff --git a/theories/Substitution/Introductions/Pi.v b/theories/Substitution/Introductions/Pi.v
index dd1c8ea..2914521 100644
--- a/theories/Substitution/Introductions/Pi.v
+++ b/theories/Substitution/Introductions/Pi.v
@@ -1,6 +1,6 @@
 From Coq Require Import ssrbool.
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
-From LogRel Require Import Utils BasicAst Notations Context NormalForms UntypedValues Weakening
+From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening
   GenericTyping LogicalRelation Validity.
 From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance.
 From LogRel.Substitution Require Import Irrelevance Properties.
diff --git a/theories/Substitution/Introductions/Poly.v b/theories/Substitution/Introductions/Poly.v
index 9dbf345..c7133fe 100644
--- a/theories/Substitution/Introductions/Poly.v
+++ b/theories/Substitution/Introductions/Poly.v
@@ -1,6 +1,6 @@
 From Coq Require Import ssrbool.
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
-From LogRel Require Import Utils BasicAst Notations Context NormalForms UntypedValues Weakening
+From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening
   GenericTyping LogicalRelation Validity.
 From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance.
 From LogRel.Substitution Require Import Irrelevance Properties.
diff --git a/theories/Substitution/Introductions/Sigma.v b/theories/Substitution/Introductions/Sigma.v
index ec39391..8f5dab4 100644
--- a/theories/Substitution/Introductions/Sigma.v
+++ b/theories/Substitution/Introductions/Sigma.v
@@ -1,6 +1,6 @@
 From Coq Require Import ssrbool.
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
-From LogRel Require Import Utils BasicAst Notations Context NormalForms UntypedValues Weakening
+From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening
   GenericTyping LogicalRelation Validity.
 From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance Reduction NormalRed Induction Transitivity.
 From LogRel.Substitution Require Import Irrelevance Properties SingleSubst Reflexivity.
diff --git a/theories/Substitution/Properties.v b/theories/Substitution/Properties.v
index 2b289d5..6959e74 100644
--- a/theories/Substitution/Properties.v
+++ b/theories/Substitution/Properties.v
@@ -1,5 +1,5 @@
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
-From LogRel Require Import Utils BasicAst Notations Context NormalForms UntypedValues Weakening GenericTyping LogicalRelation Validity.
+From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening GenericTyping LogicalRelation Validity.
 From LogRel.LogicalRelation Require Import Irrelevance Escape Reflexivity Weakening Neutral Induction.
 From LogRel.Substitution Require Import Irrelevance.
 
diff --git a/theories/TypeConstructorsInj.v b/theories/TypeConstructorsInj.v
index 4bfe999..fd204cf 100644
--- a/theories/TypeConstructorsInj.v
+++ b/theories/TypeConstructorsInj.v
@@ -2,7 +2,7 @@
 From Coq Require Import CRelationClasses.
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
 From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening UntypedReduction
-  GenericTyping DeclarativeTyping DeclarativeInstance AlgorithmicTyping.
+  GenericTyping DeclarativeTyping DeclarativeInstance.
 From LogRel Require Import LogicalRelation Validity Fundamental DeclarativeSubst.
 From LogRel.LogicalRelation Require Import Escape Irrelevance Neutral Induction NormalRed.
 From LogRel.Substitution Require Import Escape Poly.
diff --git a/theories/UntypedValues.v b/theories/UntypedValues.v
index e4d7239..2dd05a2 100644
--- a/theories/UntypedValues.v
+++ b/theories/UntypedValues.v
@@ -1,5 +1,5 @@
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
-From LogRel Require Import Utils BasicAst Notations Context NormalForms UntypedReduction GenericTyping.
+From LogRel Require Import Utils BasicAst Notations Context NormalForms UntypedReduction.
 
 Unset Elimination Schemes.