blob: 81f3d271a5508a3d4977cc4151b6038ce9d7b029 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
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
|