GH pages

.github/workflows/build.yml

@@ -1,4 +1,4 @@
-name: Test Compilation for OCaml
+name: Compilation for Griotte
 
 # Prevent parallel CI: Stop every workflow of a branch
 concurrency:
@@ -74,3 +74,14 @@ jobs:
           eval "$(opam env)"
           opam exec -- dune build --display short -j ${{ env.JOBS_LIMIT }} --trace-file griotte.trc
           ./pretty-print-trace.sh griotte.trc
+
+      - name: Build docs
+        run: opam exec -- make html
+
+      - name: Deploy docs (if main branch)
+        uses: peaceiris/actions-gh-pages@v4
+        if: ${{ steps.get_branch.outputs.branch == 'main' }}
+        with:
+          github_token: ${{ secrets.GITHUB_TOKEN }}
+          publish_dir: ./html
+          destination_dir: dev

.gitignore

@@ -297,4 +297,5 @@ Makefile.coq
 Makefile.coq.conf
 
 _build/
+html/
 *.trc

Makefile

@@ -1,18 +1,30 @@
-.PHONY: all theories doc
+EXTRA_DIR = rocqdoc_extra
+BUILD_DOC_DIR = _build/default/theories/cap_machine.html
+PUBLISH_DIR = html
 
-all: theories doc
+.PHONY: all theories rocqdoc html
+
+all: theories rocqdoc
 
 theories:
 	dune build --display short --trace-file griotte.trc
 
 pretty-timed: theories
 	./pretty-print-trace.sh griotte.trc
 
-doc:
+rocqdoc: theories
 	dune build @doc --display short
 
+html: rocqdoc
+	rm -rf $(PUBLISH_DIR)
+	mkdir $(PUBLISH_DIR)
+	cp $(BUILD_DOC_DIR)/* $(PUBLISH_DIR)
+	chmod -R +w $(PUBLISH_DIR)
+	cp $(EXTRA_DIR)/resources/* $(PUBLISH_DIR)
+
 clean:
 	dune clean
+	rm -rf $(PUBLISH_DIR)
 	rm -f griotte.trc
 
 # Adapted from https://github.com/AbsInt/CompCert/blob/master/Makefile

README.md

@@ -163,9 +163,6 @@ The organisation of the `theories/` folder is as follows.
 - `region_invariants_allocation.v`:
   Lemmas for allocating a range of standard resources.
 
-- `world_interp_allocation_compartments.v`:
-  Lemmas for allocating standard resources for adversary compartments.
-
 - `model_interp_stack.v`:
   Definitions and lemmas specific to reasoning about the stack region.
 
@@ -174,6 +171,13 @@ The organisation of the `theories/` folder is as follows.
 - `world_ghost_theory.v`:
   Ghost theory of world interpretation.
   Clean interface with the model to ease the proofs for the user.
+
+- `world_interp_allocation_compartments.v`:
+  Lemmas for allocating standard resources for adversary compartments.
+
+- `world_interp_stack.v`:
+  Extension of the ghost theory of world interpretation,
+  specific to stack region.
 
 ## Logical relation and FTLR `logrel/`
 
@@ -186,7 +190,7 @@ The organisation of the `theories/` folder is as follows.
 - `world_interp_stack.v`: A collections of lemmas related to world manipulation
   in presence of safe-to-share.
 
-- `monotone.v`: Proof of the monotonicity of the value relation with regards to
+- `ftlr/monotone.v`: Proof of the monotonicity of the value relation with regards to
   public future worlds, and private future worlds for non local words.
 
 - `fundamental.v`: Contains *Fundamental Theorem of Logical
@@ -198,10 +202,6 @@ The organisation of the `theories/` folder is as follows.
   Definition of resources to have a clean interface with manipulation
   of the world, for stack region.
 
-- `world_interp_stack.v`:
-  Extension of the ghost theory of world interpretation,
-  specific to stack region.
-
 ## Switcher `switcher/`
 
 - `switcher.v`: Code of the Griotte switcher.

dune-project

@@ -18,7 +18,7 @@
  (name griotte)
  (synopsis "Griotte")
  (description "Griotte")
- (depends ocaml dune rocq-iris equations)
+ (depends ocaml dune odoc rocq-iris equations)
  (tags
   (Rocq CHERIoT "capability machine" Iris)))
 

opam

@@ -5,6 +5,7 @@ maintainer: ""
 authors: [ "anonymous" ]
 depends: [
   "dune" {= "3.21.0"}
+  "odoc"
   "rocq-core" {= "9.1.1"}
   "rocq-stdlib" {= "9.0.0"}
   "rocq-stdpp" {= "1.13.0"}

rocqdoc_extra/LICENSE

@@ -0,0 +1,21 @@
+Copyright (c) 2016, Tobias Tebbi
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+    * Redistributions in binary form must reproduce the above copyright
+      notice, this list of conditions and the following disclaimer in the
+      documentation and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE LIABLE FOR ANY
+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

rocqdoc_extra/footer.html

@@ -0,0 +1,8 @@
+</div>
+<div id="footer">
+  Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a>
+</div>
+</div>
+</body>
+
+</html>

rocqdoc_extra/header.html

@@ -0,0 +1,27 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
+<link href="coqdoc.css" rel="stylesheet" type="text/css" />
+<link href="coqdocjs.css" rel="stylesheet" type="text/css"/>
+<script type="text/javascript" src="config.js"></script>
+<script type="text/javascript" src="coqdocjs.js"></script>
+</head>
+
+<body onload="document.getElementById('content').focus()">
+  <div id="header">
+    <span class="left">
+      <span class="modulename"> <script> document.write(document.title) </script> </span>
+    </span>
+
+    <span class="button" id="toggle-proofs"></span>
+
+    <span class="right">
+      <a href="./">Project Page</a>
+      <a href="./indexpage.html"> Index </a>
+      <a href="./toc.html"> Table of Contents </a>
+    </span>
+</div>
+    <div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
+    <div id="main">

rocqdoc_extra/resources/config.js

@@ -0,0 +1,72 @@
+var coqdocjs = coqdocjs || {};
+
+coqdocjs.repl = {
+    "forall": "∀",
+    "exists": "∃",
+    "~": "¬",
+    "/\\": "∧",
+    "\\/": "∨",
+    "->": "→",
+    "<-": "←",
+    "<->": "↔",
+    "=>": "⇒",
+    "<>": "≠",
+    "<=": "≤",
+    ">=": "≥",
+    "el": "∈",
+    "nel": "∉",
+    "<<=": "⊆",
+    "|-": "⊢",
+    ">>": "»",
+    "<<": "⊆",
+    "++": "⧺",
+    "===": "≡",
+    "=/=": "≢",
+    "=~=": "≅",
+    "==>": "⟹",
+    "lhd": "⊲",
+    "rhd": "⊳",
+    "nat": "ℕ",
+    "alpha": "α",
+    "beta": "β",
+    "gamma": "γ",
+    "delta": "δ",
+    "epsilon": "ε",
+    "eta": "η",
+    "iota": "ι",
+    "kappa": "κ",
+    "lambda": "λ",
+    "mu": "μ",
+    "nu": "ν",
+    "omega": "ω",
+    "phi": "ϕ",
+    "pi": "π",
+    "psi": "ψ",
+    "rho": "ρ",
+    "sigma": "σ",
+    "tau": "τ",
+    "theta": "θ",
+    "xi": "ξ",
+    "zeta": "ζ",
+    "Delta": "Δ",
+    "Gamma": "Γ",
+    "Pi": "Π",
+    "Sigma": "Σ",
+    "Omega": "Ω",
+    "Xi": "Ξ"
+};
+
+coqdocjs.subscr = {
+  "0" : "₀",
+  "1" : "₁",
+  "2" : "₂",
+  "3" : "₃",
+  "4" : "₄",
+  "5" : "₅",
+  "6" : "₆",
+  "7" : "₇",
+  "8" : "₈",
+  "9" : "₉",
+};
+
+coqdocjs.replInText = ["==>","<=>", "=>", "->", "<-", ":="];