summaryrefslogtreecommitdiffstats
path: root/site/posts/cleopatra/coq.org
diff options
context:
space:
mode:
Diffstat (limited to 'site/posts/cleopatra/coq.org')
-rw-r--r--site/posts/cleopatra/coq.org47
1 files changed, 47 insertions, 0 deletions
diff --git a/site/posts/cleopatra/coq.org b/site/posts/cleopatra/coq.org
new file mode 100644
index 0000000..81f3d27
--- /dev/null
+++ b/site/posts/cleopatra/coq.org
@@ -0,0 +1,47 @@
+#+TITLE: Authoring Content with Coq
+
+#+SERIES: ../cleopatra.html
+#+SERIES_PREV: ./dependencies.html
+#+SERIES_NEXT: ./org.html
+
+#+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
+<div id="history">site/cleopatra/coq.org</div>
+#+END_EXPORT
+
+
+* Author Guidelines
+
+* Under the Hood
+
+#+BEGIN_SRC makefile :tangle coq.mk
+COQ_POSTS := $(shell find site/ -name "*.v")
+COQ_HTML := $(COQ_POSTS:.v=.html)
+COQ_ARTIFACTS := $(COQ_POSTS:.v=.vo) \
+ $(COQ_POSTS:.v=.vok) \
+ $(COQ_POSTS:.v=.vos) \
+ $(COQ_POSTS:.v=.glob) \
+ $(join $(dir ${COQ_POSTS}),$(addprefix ".",$(notdir $(COQ_POSTS:.v=.aux))))
+
+coq-build : ${COQ_HTML}
+
+soupault-build : coq-build
+
+ARTIFACTS += ${COQ_ARTIFACTS} .lia.cache
+ARTIFACTS += ${COQ_HTML}
+
+COQLIB := "https://coq.inria.fr/distrib/current/stdlib/"
+COQCARG := -async-proofs-cache force \
+ -w -custom-entry-overriden
+COQDOCARG := --no-index --charset utf8 --short \
+ --body-only --coqlib "${COQLIB}" \
+ --external "https://coq-community.org/coq-ext-lib/v0.11.2/" ExtLib \
+ --external "https://compcert.org/doc/html" compcert \
+ --external "https://lysxia.github.io/coq-simple-io" SimpleIO
+
+%.html : %.v coq.mk _opam/init
+ @cleopatra echo Exporting "$*.v"
+ @coqc ${COQCARG} $<
+ @coqdoc ${COQDOCARG} -d $(shell dirname $<) $<
+ @rm -f $(shell dirname $<)/coqdoc.css
+#+END_SRC