Merge pull request #428 from maximedenes/build-doc

Add Makefile target to build the doc

2 files changed, 185 insertions, 2 deletions

diff --git a/etc/buildlibgraph b/etc/buildlibgraph
new file mode 100755
index 0000000..0a8de58
--- /dev/null
+++ b/etc/buildlibgraph
@@ -0,0 +1,163 @@
+#!/usr/bin/env lua
+
+nodes = {}
+clusters = {}
+edges = {}
+args = {}
+
+function decompose(n)
+        return n:match("^([^/]+)/([^%.]+)")
+end
+
+for l in io.lines() do
+        local to, froms = l:match("^([^ :]+)[^:]*:(.*)")
+        local cluster, module = decompose(to)
+        clusters[cluster] = clusters[cluster] or {}
+        clusters[cluster][module] = true
+        nodes[module] = true
+        for from in froms:gmatch("[^ ]+") do
+                local cluster, module2 = decompose(from)
+                nodes[module2] = true
+                if module ~= module2 then
+                        clusters[cluster] = clusters[cluster] or {}
+                        clusters[cluster][module2] = true
+                        edges[#edges+1] = { from = module; to = module2 }
+                end
+        end
+end
+
+-- transitive reduction
+--
+-- // reflexive reduction
+-- for (int i = 0; i < N; ++i)
+--   m[i][i] = false;
+-- 
+-- // transitive reduction
+-- for (int j = 0; j < N; ++j)
+--   for (int i = 0; i < N; ++i)
+--     if (m[i][j])
+--       for (int k = 0; k < N; ++k)
+--         if (m[j][k])
+--           m[i][k] = false;
+-- 
+function path_matrix(nodes,edges)
+    local m = {}
+    for j,_ in pairs(nodes) do
+      m[j] = {}
+    end
+    for _,e in ipairs(edges) do                        
+      m[e.from][e.to] = true
+    end
+    -- close
+    for j,_ in pairs(nodes) do
+      for i,_ in pairs(nodes) do
+        for k,_ in pairs(nodes) do
+          if m[i][j] == true and m[j][k] == true then m[i][k] = true end
+        end
+      end
+    end
+    return m
+end
+function tred(nodes,m)
+    -- reduce
+    for j,_ in pairs(nodes) do
+      for i,_ in pairs(nodes) do
+        if m[i][j] == true then
+          for k,_ in pairs(nodes) do
+            if m[j][k] then m[i][k] = false end
+          end
+        end
+      end
+    end
+end
+function matrix_to_list(nodes,m)
+    local edges = {}
+    for j,_ in pairs(nodes) do
+      for i,_ in pairs(nodes) do
+        if m[i][j] == true then
+          edges[#edges+1] = { from = i; to = j }
+        end
+      end
+    end
+    return edges
+end
+
+
+
+m = path_matrix(nodes,edges)
+tred(nodes,m)
+edges = matrix_to_list(nodes,m)
+
+meta_edges = {}
+for c1,nodes1 in pairs(clusters) do
+  for c2,nodes2 in pairs(clusters) do
+    if (c1 ~= c2) then
+      local connected = false
+      for n1,_ in pairs(nodes1) do
+        for n2,_ in pairs(nodes2) do
+          if m[n1][n2] == true then connected = true end
+        end
+      end
+      if connected then meta_edges[#meta_edges+1] = { from = c1; to = c2 } end
+    end
+  end
+end
+
+m = path_matrix(clusters,meta_edges)
+tred(clusters,m)
+meta_edges = matrix_to_list(clusters,m)
+
+function dot()
+        print[[
+        digraph mathcomp {
+                compound = true;
+        ]]
+        for c,nodes in pairs(clusters) do
+                print("subgraph cluster_" .. c .. " {")
+                for node,_ in pairs(nodes) do
+                        print('"'..node..'";')
+                end
+                print("}")
+        end
+        for _,edge in ipairs(edges) do                        
+                print(string.format('"%s" -> "%s";',edge.from,edge.to))
+        end
+        print[[
+        }
+        ]]
+end
+
+function cytoscape()
+        print[[
+        var depends = [
+        ]]
+        for c,nodes in pairs(clusters) do
+                print(string.format('{ data: { id: "cluster_%s", name: "%s" } },', c, c))
+                print(string.format('{ data: { id: "cluster_%s_plus", name: "+", parent: "cluster_%s" } },', c, c))
+                for node,_ in pairs(nodes) do
+			local released = "no"
+			if args[node] then released = "yes" end
+                        print(string.format('{ data: { id: "%s", name: "%s", parent: "cluster_%s", released: "%s" } },', node, node, c, released))
+                end
+        end
+        local i = 0
+        for _,edge in ipairs(edges) do                        
+                print(string.format('{ data: { id: "edge%d", source: "%s", target: "%s" } },', i, edge.from,edge.to))
+                i=i+1
+        end
+        for _,edge in ipairs(meta_edges) do                        
+                print(string.format('{ data: { id: "edge%d", source: "cluster_%s", target: "cluster_%s" } },', i, edge.from,edge.to))
+                i=i+1
+        end
+        print[[ ]; ]]
+end
+
+for i=1,#arg do
+	args[arg[i]] = true
+end
+
+cytoscape()
+
+-- $COQBIN/coqdep -R . mathcomp */*.v | grep -v vio: > depend
+--   cat depend | ./graph.lua dot | tee depend.dot | dot -T png -o depend.png
+--   cat depend | ./graph.lua cytoscape `git show release/1.6:mathcomp/Make | grep 'v *$' | cut -d / -f 2 | cut -d . -f 1` > depend.js
diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common
index 8e84ccc..04c3adc 100644
--- a/mathcomp/Makefile.common
+++ b/mathcomp/Makefile.common
@@ -25,7 +25,7 @@ TGTS?=
 ######################################################################
 
 # local context: -----------------------------------------------------
-.PHONY: all config build only test-suite clean distclean __always__
+.PHONY: all config build only test-suite clean distclean doc doc-clean __always__
 .SUFFIXES:
 
 H:= $(if $(VERBOSE),,@)  # not used yet
@@ -72,7 +72,7 @@ only: sub-only this-only
 
 test-suite: sub-test-suite this-test-suite
 
-clean: sub-clean this-clean
+clean: sub-clean this-clean doc-clean
 
 distclean: sub-distclean this-distclean
 
@@ -127,3 +127,23 @@ endif
 # Make of individual .vo ---------------------------------------------
 %.vo: __always__ Makefile.coq
 	+$(COQMAKE) $@
+
+doc: __always__ Makefile.coq
+	mkdir -p _build_doc/
+	cp -r $(COQFILES) -t _build_doc/ --parents
+	cp Make Makefile* _build_doc
+	mkdir -p _build_doc/htmldoc
+	. ../etc/utils/builddoc_lib.sh; \
+		cd _build_doc && mangle_sources $(COQFILES)
+	+cd _build_doc && $(COQMAKE)
+	cd _build_doc && if [ ! -f .Makefile.coq.d ] ; then cp .coqdeps.d .Makefile.coq.d ; fi #can be removed when coq-8.10 compatibility is dropped
+	cd _build_doc && grep -v vio: .Makefile.coq.d > depend
+	cd _build_doc && cat depend | ../../etc/buildlibgraph $(COQFILES) > htmldoc/depend.js
+	cd _build_doc && $(COQBIN)coqdoc -t "Mathematical Components" \
+		-g --utf8 -R . mathcomp \
+		--parse-comments \
+		--multi-index $(COQFILES) -d htmldoc
+	cp ../etc/artwork/coqdoc.css _build_doc/htmldoc
+
+doc-clean:
+	rm -r _build_doc/