diff --git a/Makefile.common b/Makefile.common index 21375da9c5..dd6ca82650 100644 --- a/Makefile.common +++ b/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 diff --git a/etc/builddoc_dependency_dot.pl b/etc/builddoc_dependency_dot.pl index 8fa5715f5e..68aac5bc90 100644 --- a/etc/builddoc_dependency_dot.pl +++ b/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";