Rocqnavi functional analysis

Makefile.common

@@ -96,6 +96,10 @@ DOCDIR=html
 
 GIT_HASH := $(shell git describe --tags --exact-match 2>/dev/null || git rev-parse --short HEAD)
 
+TIMESTAMP=$(shell date +%Y.%m.%d-%H:%M)
+
+GITHUB_URL="https://github.com/math-comp/analysis/tree/$(shell git rev-parse HEAD)"
+
 $(DOCDIR)/dependency_graph.pre:
 	mkdir -p $(DOCDIR)
 	coqdep -f _CoqProject | perl etc/builddoc_dependency_dot.pl > $(DOCDIR)/dependency_graph.pre
@@ -106,7 +110,7 @@ $(DOCDIR)/dependency_graph.dot: $(DOCDIR)/dependency_graph.pre
 html: build $(DOCDIR)/dependency_graph.dot
 	etc/rocqnavi_generate-hierarchy-graph.sh $(DOCDIR)/hierarchy_graph.dot
 	find . -name "*.v" -or -name "*.glob" | grep -v "/\." | grep -v "_opam/" | xargs rocqnavi \
-	-title "Mathcomp Analysis $(GIT_HASH)" \
+	-title "Mathcomp Analysis $(GIT_HASH) $(TIMESTAMP)" \
 	-d $(DOCDIR) -Q theories mathcomp.analysis \
 	-Q classical mathcomp.classical \
 	-Q reals mathcomp.reals \
@@ -118,6 +122,7 @@ html: build $(DOCDIR)/dependency_graph.dot
 	-structure-graph $(DOCDIR)/hierarchy_graph.dot \
         -index-blacklist etc/rocqnavi_index-blacklist \
         -show-type-information-using-coqtop-process \
+	-doc-source-url $(GITHUB_URL) \
 	-external https://math-comp.github.io/htmldoc_2_5_0/ mathcomp.order \
 	-external https://math-comp.github.io/htmldoc_2_5_0/ mathcomp.boot \
 	-external https://math-comp.github.io/htmldoc_2_5_0/ mathcomp.algebra

etc/builddoc_dependency_dot.pl

@@ -1,50 +1,99 @@
-print "digraph depend {\n";
+my %clusters = ( #         directory => [ Cluster Name, Color, URL ]
+    classical                        => [ "Classical", 1, "" ],
+    'experimental_reals'             => [ "ExperimentalReals", 1, "" ],
+    reals                            => [ "Reals", 2,  "" ],
+    reals_stdlib                     => [ "Reals", 2,  "" ],
+    analysis_stdlib                  => [ "AnalysisStdlib", 5, "" ],
+    'analysis_stdlib/showcase'       => [ "AnalysisStdlib", 5, "" ],
+    theories                         => [ "Analysis", 5, "analysis.%s" ],
+    'theories/showcase'              => [ "Analysis", 5, "analysis.showcase.%s" ],
+
+    'theories/topology_theory'       => [ "Topology", 4,
+                                          "analysis.topology_theory.%s" ],
+    'theories/homotopy_theory'       => [ "Topology", 4,
+                                          "analysis.homotopy_theory.%s" ],
+
+    'theories/normedtype_theory'     => [ "Normedtype", 9,
+                                          "analysis.normedtype_theory.%s" ],
+
+    'theories/lebesgue_integral_theory'
+                                     => [ "LebesgueIntegral", 10,
+                                          "analysis.lebesgue_integral_theory.%s" ],
+
+    'theories/measure_theory'        => [ "Measure", 11,
+                                          "analysis.measure_theory.%s" ],
+
+    'theories/probability_theory'    => [ "Probability", 12,
+                                          "analysis.probability_theory.%s" ],
+
+    'theories/functional_analysis'   => [ "FunctionalAnalysis", 3,
+                                          "analysis.functional_analysis.%s"],
+);
+
+print "digraph dependencies {\n";
 print "  node [shape = ellipse,style=filled,colorscheme = paired12];\n";
-print "  subgraph cluster_analysis { label=\"Analysis\" }\n";
-print "  subgraph cluster_classical { label=\"Classical\" }\n";
-print "  subgraph cluster_reals { label=\"Reals\" }\n";
-print "  subgraph cluster_experimental_reals { label=\"ExperimentalReals\" }\n";
-print "  subgraph cluster_analysis { label=\"Analysis\" }\n";
-print "  subgraph cluster_topology { label=\"Topology\" }\n";
-print "  subgraph cluster_normedtype { label=\"NormedType\" }\n";
-print "  subgraph cluster_measure { label=\"Measure\" }\n";
-print "  subgraph cluster_lebesgue_integral { label=\"Lebesgue_integral\" }\n";
-print "  subgraph cluster_probability { label=\"Probability\" }\n";
+
+my %seen;
+for my $k (sort keys %clusters) {
+    my ($cluster) = @{ $clusters{$k} };
+    next if $seen{$cluster}++;
+
+    my $cluster_name = "cluster_".$cluster;
+    print qq{  subgraph $cluster_name { label="$cluster" }\n};
+}
+
 while (<>) {
-  if (m/([^\s]*)\.vo.*:(.*)/) {
-    $dests = $2 ;
-    ($path,$src) = ($1 =~ s/\//\//rg =~ m/^(?:(.*)\/)?([^.]*)$/);
-    $url="mathcomp.$path.$src.html";
-    if ($path =~ m/classical/) {
-        print "subgraph cluster_classical { \"$path\/$src\"[label=\"$src\",URL=\"$url\",fillcolor=1]}\n";
-    }elsif ($path =~ m/reals/ or $path =~ m/reals_stdlib/) {
-        print "subgraph cluster_reals { \"$path\/$src\"[label=\"$src\",URL=\"$url\",fillcolor=2,fontcolor=white]}";
-    }elsif ($path =~ m/theories\/topology_theory/) {
-        $url="mathcomp.analysis.topology_theory.$src.html";
-        print "subgraph cluster_topology { \"$path\/$src\"[label=\"$src\",URL=\"$url\",fillcolor=4,fontcolor=white]}";
-    }elsif ($path =~ m/theories\/normedtype_theory/) {
-        $url="mathcomp.analysis.normedtype_theory.$src.html";
-        print "subgraph cluster_normedtype { \"$path\/$src\"[label=\"$src\",URL=\"$url\",fillcolor=9]}";
-    }elsif ($path =~ m/theories\/lebesgue_integral_theory/) {
-        $url="mathcomp.analysis.lebesgue_integral_theory.$src.html";
-        print "subgraph cluster_lebesgue_integral { \"$path\/$src\"[label=\"$src\",URL=\"$url\",fillcolor=10,fontcolor=white]}";
-    }elsif ($path =~ m/theories\/measure_theory/) {
-        $url="mathcomp.analysis.measure_theory.$src.html";
-        print "subgraph cluster_measure { \"$path\/$src\"[label=\"$src\",URL=\"$url\",fillcolor=11]}";
-    }elsif ($path =~ m/theories\/probability_theory/) {
-        $url="mathcomp.analysis.probability_theory.$src.html";
-        print "subgraph cluster_probability { \"$path\/$src\"[label=\"$src\",URL=\"$url\",fillcolor=12]}";
-    }elsif ($path =~ m/theories/) {
-       $url="mathcomp.analysis.$src.html";
-       print "subgraph cluster_analysis { \"$path\/$src\"[label=\"$src\",URL=\"$url\",fillcolor=5]}";
-    }elsif ($path =~ m/analysis_stdlib/) {
-       print "subgraph cluster_analysis { \"$path\/$src\"[label=\"$src\",URL=\"$url\",fillcolor=5]}";
-    }else {
-        print "\"$path\/$src\"[label=\"$path=$src\",fillcolor=6,fontcolor=white]";
-    }
-    for my $dest (split(" ", $dests)) {
-        print "  \"$1\" -> \"$path\/$src\";\n" if ($dest =~ m/(.*)\.vo/);
+    if (m/([^\s]*)\.vo.*:(.*)/) {
+
+        my $dests = $2;
+
+        my ($path,$src)
+            = ($1 =~ s/\//\//rg =~ m/^(?:(.*)\/)?([^.]*)$/);
+
+        my $url = "mathcomp.$path.$src.html";
+
+        my ($cluster_label, $color, $urltmpl);
+
+        if (exists $clusters{$path}) {
+            ($cluster_label, $color, $urltmpl) = @{ $clusters{$path} };
+        }
+
+        if (defined $cluster_label) {
+
+            if ($urltmpl ne "") {
+                $url = "mathcomp."
+                     . sprintf($urltmpl,$src)
+                     . ".html";
+            }
+
+            my $fontcolor =
+                ($color == 2 || $color == 4 || $color == 10)
+                ? "white"
+                : "black";
+
+            my $cluster = "cluster_".$cluster_label;
+            print qq{
+subgraph $cluster {
+    "$path/$src"[
+        label="$src",
+        URL="$url",
+        fillcolor=$color
+    ]
+}
+};
+
+        } else {
+
+            my $unknown = $path;
+            $unknown =~ s#[^A-Za-z0-9_]#_#g;
+
+        }
+
+        for my $dest (split " ", $dests) {
+            print qq{  "$1" -> "$path/$src";\n}
+                if $dest =~ /(.*)\.vo/;
+        }
     }
-  }
 }
+
 print "}\n";