Merge pull request #1455 from JasonGross/alectryon

Generate Documentation with Alectryon

.github/workflows/ci.yml

@@ -103,3 +103,41 @@ jobs:
       run: etc/ci/after_success.sh
       env:
         ACTIONS_DEPLOY_KEY: ${{ secrets.ACTIONS_DEPLOY_KEY }}
+
+  alectryon:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v2
+    - uses: snickerbockers/submodules-init@v4
+    - uses: coq-community/docker-coq-action@v1
+      with:
+        coq_version: 8.13
+        ocaml_version: 4.11-flambda
+        custom_script: |
+          opam install -y coq-serapi
+          sudo apt-get -o Acquire::Retries=30 update -q
+          sudo apt-get -o Acquire::Retries=30 install python3-pip autoconf -y --allow-unauthenticated
+          python3 -m pip install --user --upgrade pygments dominate beautifulsoup4 docutils
+          startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
+            sudo chown -R coq:coq .
+          endGroup
+          ./autogen.sh
+          ./configure
+          make TIMED=1 -j2
+          make alectryon
+    - name: Revert permissions
+      # to avoid a warning at cleanup time - https://github.com/coq-community/docker-coq-action#permissions
+      if: ${{ always() }}
+      run: sudo chown -R 1001:116 .
+    - name: upload alectryon artifact
+      uses: actions/upload-artifact@v1
+      with:
+        name: alectryon-html
+        path: alectryon-html
+    - name: Deploy html files
+      uses: JamesIves/github-pages-deploy-action@releases/v4
+      with:
+        dry-run: ${{ github.ref != 'refs/heads/master' || github.event_name != 'push' }}
+        branch: gh-pages
+        folder: alectryon-html
+        single-commit: false

.gitignore

@@ -21,6 +21,8 @@ proviola/
 proviola-html/
 proviola-xml/
 file-dep-graphs/
+alectryon-html/
+alectryon-cache/
 
 HoTT.deps
 HoTT.dot
@@ -43,6 +45,7 @@ Makefile.in
 Makefile
 Makefile_ssrplugin
 html-done.timestamp
+alectryon-html-done.timestamp
 
 # Ignore links into the original Coq library
 coq/dev

.gitmodules

@@ -9,3 +9,6 @@
 	path = etc/coq-dpdgraph
 	url = https://github.com/andreaslyn/coq-dpdgraph.git
 	branch = hott
+[submodule "etc/alectryon"]
+	path = etc/alectryon
+	url = https://github.com/JasonGross/alectryon.git

Makefile.am

@@ -53,6 +53,9 @@ SILENCE_COQDEP = $(SILENCE_COQDEP_$(V))
 # the proviola camera
 CAMERA = python proviola/camera/camera.py
 
+# the alectryon binary
+ALECTRYON = python3 etc/alectryon/alectryon.py
+
 # read the targets from _CoqMakefile
 
 COQ_PROJECT_CONTENTS = $(shell cat $(srcdir)/_CoqProject)
@@ -108,6 +111,7 @@ ALL_TIMING_HTMLFILES=$(MAIN_TIMING_HTMLFILES)
 ALL_TIMINGFILES=$(ALL_VFILES:.v=.v.timing)
 ALL_XMLFILES=$(patsubst $(srcdir)/html/%,$(srcdir)/proviola-xml/%,$(ALL_HTMLFILES:.html=.xml))
 ALL_PROVIOLA_HTMLFILES=$(patsubst $(srcdir)/proviola-xml/%,$(srcdir)/proviola-html/%,$(ALL_XMLFILES:.xml=.html))
+ALL_ALECTRYON_HTMLFILES=$(patsubst $(srcdir)/html/%,$(srcdir)/alectryon-html/%,$(ALL_HTMLFILES))
 ALL_DPDFILES=$(MAIN_DPDFILES)
 ALL_SVGFILES=$(ALL_DPDFILES:.dpd=.svg)
 ALL_DOTFILES=$(ALL_DPDFILES:.dpd=.dot)
@@ -132,7 +136,7 @@ all-am: Makefile $(SCRIPTS) $(DATA) _CoqProject
 
 .SECONDEXPANSION:
 
-.PHONY: hottlib hott-core hott-categories contrib clean html proviola timing-html clean-local install-data-local proviola-all proviola-xml svg-file-dep-graphs svg-aggregate-dep-graphs svg-dep-graphs clean-dpdgraph strict strict-test strict-no-axiom quick vi2vo checkproofs validate
+.PHONY: hottlib hott-core hott-categories contrib clean html proviola alectryon timing-html clean-local install-data-local proviola-all proviola-xml svg-file-dep-graphs svg-aggregate-dep-graphs svg-dep-graphs clean-dpdgraph strict strict-test strict-no-axiom quick vi2vo checkproofs validate
 
 # targets that we don't need to run coqdep for
 FAST_TARGETS = clean clean-local clean-dpdgraph TAGS
@@ -257,6 +261,24 @@ proviola-xml: $(ALL_XMLFILES)
 
 proviola-all: proviola proviola-xml
 
+# the alectryon files
+alectryon-html/index.html alectryon-html/toc.html alectryon-html/coqdoc.css : alectryon-html/% : html/%
+	- $(mkdir_p) alectryon-html
+	cp -f $< $@
+
+alectryon-html-done.timestamp: $(ALL_GLOBFILES) $(ALL_VFILES)
+	- $(mkdir_p) alectryon-html
+	touch alectryon-html-done.timestamp
+	$(TIMER) $(ALECTRYON) --frontend coq+rst --backend webpage --sertop-arg=--no_prelude --sertop-arg=--indices-matter -R "$(srcdir)/theories" HoTT -Q "$(srcdir)/contrib" HoTT.Contrib --output-directory alectryon-html --cache-directory alectryon-cache $(ALL_VFILES)
+
+alectryon-html:
+	rm -f alectryon-html-done.timestamp
+	$(MAKE) alectryon-html-done.timestamp
+
+$(ALL_ALECTRYON_HTMLFILES) : alectryon-html-done.timestamp
+
+alectryon: $(ALL_ALECTRYON_HTMLFILES) alectryon-html/toc.html alectryon-html/coqdoc.css alectryon-html/index.html
+
 # dpdgraphs
 COQTHMDEP=etc/coq-dpdgraph/coqthmdep
 HOQTHMDEP=etc/hoqthmdep
@@ -353,6 +375,8 @@ clean::
 	$(Q)rm -f $(ALL_XMLFILES)
 	$(VECHO) "RM *.HTML"
 	$(Q)rm -f $(ALL_PROVIOLA_HTMLFILES)
+	$(VECHO) "RM *.HTML"
+	$(Q)rm -f $(ALL_ALECTRYON_HTMLFILES)
 	$(VECHO) "RM *.TIMING"
 	$(Q)rm -f $(ALL_TIMINGFILES)
 	$(VECHO) "RM *.TIMING.HTML"