Merge pull request #50 from coq-community/move-docs

migrate coqdoc to gh-pages branch
coq-community · Jan 10, 2020 · 73303f9 · 73303f9
2 parents b0a9f1d + b98daae
commit 73303f9
Show file tree

Hide file tree

Showing 44 changed files with 28 additions and 19,072 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,10 +1,11 @@
 Makefile.coq
 Makefile.coq.conf
+_build
+docs
 *~
 *.d
 *.aux
 *.glob
 *.vo
 *.vos
 *.vok
-result
diff --git a/Makefile.coq.local b/Makefile.coq.local
@@ -1,19 +1,20 @@
 GLOBFILES = $(VFILES:.v=.glob)
 CSSFILES = resources/coqdoc.css resources/coqdocjs.css
 JSFILES = resources/config.js resources/coqdocjs.js
-HTMLFILES = resources/header.html resources/footer.html resources/index.html
+HTMLFILES = resources/header.html resources/footer.html
+COQDOCDIR = docs/coqdoc
 
 COQDOCHTMLFLAGS = --toc --toc-depth 2 --index indexpage --html \
   --interpolate --no-lib-name --parse-comments \
   --with-header resources/header.html --with-footer resources/footer.html
 
+coqdoc: $(GLOBFILES) $(VFILES) $(CSSFILES) $(JSFILES) $(HTMLFILES)
+	$(SHOW)'COQDOC -d $(COQDOCDIR)'
+	$(HIDE)mkdir -p $(COQDOCDIR)
+	$(HIDE)$(COQDOC) $(COQDOCHTMLFLAGS) $(COQDOCLIBS) -d $(COQDOCDIR) $(VFILES)
+	$(SHOW)'COPY resources'
+	$(HIDE)cp $(CSSFILES) $(JSFILES) $(COQDOCDIR)
+.PHONY: coqdoc
+
 resources/index.html: resources/index.md
 	pandoc -s -o $@ $<
-
-docs: $(GLOBFILES) $(VFILES) $(CSSFILES) $(JSFILES) $(HTMLFILES)
-	$(SHOW)'COQDOC -d docs'
-	$(HIDE)mkdir -p docs
-	$(HIDE)$(COQDOC) $(COQDOCHTMLFLAGS) $(COQDOCLIBS) -d docs $(VFILES)
-	$(SHOW)'COPY resources'
-	$(HIDE)cp $(CSSFILES) $(JSFILES) resources/index.html docs
-.PHONY: docs
diff --git a/README.md b/README.md
@@ -20,7 +20,7 @@
 [gitter-link]: https://gitter.im/coq-community/Lobby
 
 [coqdoc-shield]: https://img.shields.io/badge/docs-coqdoc-blue.svg
-[coqdoc-link]: https://coq-community.github.io/lemma-overloading/toc.html
+[coqdoc-link]: https://coq-community.github.io/lemma-overloading/docs/latest/coqdoc/toc.html
 
 [doi-shield]: https://zenodo.org/badge/DOI/10.1017/S0956796813000051.svg
 [doi-link]: https://doi.org/10.1017/S0956796813000051
@@ -77,7 +77,7 @@ make install
 
 The Coq source files mentioned in the paper [How to make ad hoc proof automation less ad hoc][lessadhoc],
 Journal of Functional Programming 23(4), pp. 357-401, are described below. See also the
-[coqdoc presentation][coqdoc] of the files.
+[coqdoc presentation][coqdoc] of the files from the latest release.
 
 ### `indom.v`
 
@@ -139,4 +139,4 @@ pp. 261-274.
 
 [lessadhoc]: https://software.imdea.org/~aleks/papers/lessadhoc/journal.pdf
 [reflect]: https://software.imdea.org/~aleks/papers/reflect/reflect.pdf
-[coqdoc]: https://coq-community.github.io/lemma-overloading/toc.html
+[coqdoc]: https://coq-community.github.io/lemma-overloading/docs/latest/coqdoc/toc.html
diff --git a/docs/LemmaOverloading.auto.html b/docs/LemmaOverloading.auto.html
diff --git a/docs/LemmaOverloading.cancel.html b/docs/LemmaOverloading.cancel.html
diff --git a/docs/LemmaOverloading.cancel2.html b/docs/LemmaOverloading.cancel2.html
diff --git a/docs/LemmaOverloading.cancelCTC.html b/docs/LemmaOverloading.cancelCTC.html
diff --git a/docs/LemmaOverloading.cancelD.html b/docs/LemmaOverloading.cancelD.html
diff --git a/docs/LemmaOverloading.domains.html b/docs/LemmaOverloading.domains.html
diff --git a/docs/LemmaOverloading.finmap.html b/docs/LemmaOverloading.finmap.html
diff --git a/docs/LemmaOverloading.heaps.html b/docs/LemmaOverloading.heaps.html
diff --git a/docs/LemmaOverloading.hprop.html b/docs/LemmaOverloading.hprop.html
diff --git a/docs/LemmaOverloading.indom.html b/docs/LemmaOverloading.indom.html
diff --git a/docs/LemmaOverloading.indomCTC.html b/docs/LemmaOverloading.indomCTC.html
diff --git a/docs/LemmaOverloading.llistR.html b/docs/LemmaOverloading.llistR.html
diff --git a/docs/LemmaOverloading.noalias.html b/docs/LemmaOverloading.noalias.html
diff --git a/docs/LemmaOverloading.noaliasBT.html b/docs/LemmaOverloading.noaliasBT.html
diff --git a/docs/LemmaOverloading.noaliasCTC.html b/docs/LemmaOverloading.noaliasCTC.html
diff --git a/docs/LemmaOverloading.ordtype.html b/docs/LemmaOverloading.ordtype.html
diff --git a/docs/LemmaOverloading.perms.html b/docs/LemmaOverloading.perms.html
diff --git a/docs/LemmaOverloading.prefix.html b/docs/LemmaOverloading.prefix.html
diff --git a/docs/LemmaOverloading.prelude.html b/docs/LemmaOverloading.prelude.html
diff --git a/docs/LemmaOverloading.rels.html b/docs/LemmaOverloading.rels.html
diff --git a/docs/LemmaOverloading.stlog.html b/docs/LemmaOverloading.stlog.html
diff --git a/docs/LemmaOverloading.stlogCTC.html b/docs/LemmaOverloading.stlogCTC.html
diff --git a/docs/LemmaOverloading.stlogR.html b/docs/LemmaOverloading.stlogR.html
diff --git a/docs/LemmaOverloading.stmod.html b/docs/LemmaOverloading.stmod.html
diff --git a/docs/LemmaOverloading.stsep.html b/docs/LemmaOverloading.stsep.html
diff --git a/docs/LemmaOverloading.terms.html b/docs/LemmaOverloading.terms.html
diff --git a/docs/LemmaOverloading.xfind.html b/docs/LemmaOverloading.xfind.html
diff --git a/docs/LemmaOverloading.xfindCTC.html b/docs/LemmaOverloading.xfindCTC.html
diff --git a/docs/config.js b/docs/config.js
diff --git a/docs/coqdoc.css b/docs/coqdoc.css