* 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-build : ${COQ_HTML}

theme-build : site/style/coq.sass
soupault-build : coq-build

ARTIFACTS += *.vo *.vok *.vos .*.aux *.glob .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}"

%.html : %.v coq.mk
	@cleopatra echo Exporting "$*.v"
	@coqc ${COQCARG} $<
	@coqdoc ${COQDOCARG} -d $(shell dirname $<) $<
	@rm -f $(shell dirname $<)/coqdoc.css
#+END_SRC

#+BEGIN_SRC sass :tangle site/style/coq.sass
div.code
    white-space: nowrap
    line-height : 140%

div.code,
span.inlinecode
    font-family : 'Fira Code', monospace
    font-size : 80%

div.doc
    max-width : 35rem
    line-height : 140%

    /* dirty patch to get the code in full page width */
    pre
        width : calc(100vw - 2*5rem)

.paragraph
    margin-bottom : .8em
#+END_SRC

#+BEGIN_SRC sass :tangle site/style/coq.sass
.code
    .id[title="keyword"]
        color : #d73a49

    .id[title="definition"],
    .id[title="projection"],
    .id[title="theorem"],
    .id[title="lemma"]
        color : #6f42c1

    .id[title="inductive"],
    .id[title="record"],
    .id[title="axiom"],
    .id[title="class"]
        color : #005cc5

    .id[title="constructor"]
        color : #e36209

    a[href]
        color : inherit
        text-decoration : none
        background : #f7f7f7
        padding : .1rem .15rem .1rem .15rem
        border-radius : 15%

        .url-mark
            display: none
#+END_SRC

# Local Variables:
# org-src-preserve-indentation: t
# End: