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 --- mathcomp/Makefile.common | 23 +++++++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) (limited to 'mathcomp') 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(-) (limited to 'mathcomp') 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(-) (limited to 'mathcomp') 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(-) (limited to 'mathcomp') 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(-) (limited to 'mathcomp') 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(-) (limited to 'mathcomp') 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