From 81802638190ade2b989f34eb7afb92a1413f59c6 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 15 Nov 2019 19:28:02 +0100 Subject: Add Makefile target to build the doc --- etc/buildlibgraph | 163 +++++++++++++++++++++++++++++++++++++++++++++++ mathcomp/Makefile.common | 23 ++++++- 2 files changed, 184 insertions(+), 2 deletions(-) create mode 100755 etc/buildlibgraph 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..2dc4396 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,22 @@ endif # Make of individual .vo --------------------------------------------- %.vo: __always__ Makefile.coq +$(COQMAKE) $@ + +doc: + 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 && 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/ -- cgit v1.2.3 From c08f721483b7d6e8da64f8f475ce68bbaff5b05c Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Nov 2019 14:02:53 +0100 Subject: Add missing dependencies Spotted by Yves. --- mathcomp/Makefile.common | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common index 2dc4396..575ea2b 100644 --- a/mathcomp/Makefile.common +++ b/mathcomp/Makefile.common @@ -128,7 +128,7 @@ endif %.vo: __always__ Makefile.coq +$(COQMAKE) $@ -doc: +doc: __always__ Makefile.coq mkdir -p _build_doc/ cp -r $(COQFILES) -t _build_doc/ --parents cp Make Makefile* _build_doc -- cgit v1.2.3 From 054024e3b03eeb2f4ce93a904d68bcc4f216d38b Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Wed, 20 Nov 2019 15:34:31 +0100 Subject: things that are needed to make 'make doc' work --- mathcomp/Makefile.common | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common index 575ea2b..92e9bfd 100644 --- a/mathcomp/Makefile.common +++ b/mathcomp/Makefile.common @@ -136,7 +136,7 @@ doc: __always__ Makefile.coq . ../etc/utils/builddoc_lib.sh; \ cd _build_doc && mangle_sources $(COQFILES) +cd _build_doc && $(COQMAKE) - cd _build_doc && grep -v vio: .Makefile.coq.d > depend + cd _build_doc && grep -v vio: .coqdeps.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 \ -- cgit v1.2.3 From 467e24a7c00c8743c209a06ef152c14b2ea72136 Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Thu, 21 Nov 2019 16:50:35 +0100 Subject: dependency file will change name after coq-8.10 --- mathcomp/Makefile.common | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common index 92e9bfd..3bae559 100644 --- a/mathcomp/Makefile.common +++ b/mathcomp/Makefile.common @@ -136,7 +136,8 @@ doc: __always__ Makefile.coq . ../etc/utils/builddoc_lib.sh; \ cd _build_doc && mangle_sources $(COQFILES) +cd _build_doc && $(COQMAKE) - cd _build_doc && grep -v vio: .coqdeps.d > depend + [ ! -f .Makefile.coq.d ] || cp .coqdeps.d .Makefile.coq.d + 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 \ -- cgit v1.2.3 From 85b9ab28d11800a7a690267dde7b44eba14505a2 Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Thu, 21 Nov 2019 16:52:12 +0100 Subject: adds a comment so that dead code can be remove when it is no longer used --- mathcomp/Makefile.common | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common index 3bae559..39c9afa 100644 --- a/mathcomp/Makefile.common +++ b/mathcomp/Makefile.common @@ -136,7 +136,7 @@ doc: __always__ Makefile.coq . ../etc/utils/builddoc_lib.sh; \ cd _build_doc && mangle_sources $(COQFILES) +cd _build_doc && $(COQMAKE) - [ ! -f .Makefile.coq.d ] || cp .coqdeps.d .Makefile.coq.d + [ ! -f .Makefile.coq.d ] || cp .coqdeps.d .Makefile.coq.d #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" \ -- cgit v1.2.3 From 6be8dddd806c3515467526ea0e964ca4fee188ad Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Fri, 22 Nov 2019 10:36:56 +0100 Subject: Have to change directory before checking for the dependency file --- mathcomp/Makefile.common | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common index 39c9afa..04c3adc 100644 --- a/mathcomp/Makefile.common +++ b/mathcomp/Makefile.common @@ -136,7 +136,7 @@ doc: __always__ Makefile.coq . ../etc/utils/builddoc_lib.sh; \ cd _build_doc && mangle_sources $(COQFILES) +cd _build_doc && $(COQMAKE) - [ ! -f .Makefile.coq.d ] || cp .coqdeps.d .Makefile.coq.d #can be removed when coq-8.10 compatibility is dropped + 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" \ -- cgit v1.2.3