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 <[email protected]>
CoqHott · Sep 5, 2023 · 0c15131 · 0c15131
1 parent 40aad51
commit 0c15131
Show file tree

Hide file tree

Showing 20 changed files with 70 additions and 30 deletions.
diff --git 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
@@ -16,3 +16,5 @@ Makefile.coq.conf
 *.cache
 
 _opam
+
+*.dot
diff --git 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
diff --git 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
@@ -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
@@ -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";
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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.
Original file line number	Diff line number	Diff line change
Expand Up		@@ -16,3 +16,5 @@ Makefile.coq.conf
		*.cache

		_opam

		*.dot