implement a homepage (#183)

* implement coqdoc * make coqdoc to work * update readme
Beluga-lang · Sep 10, 2024 · 02c9f19 · 02c9f19
1 parent e1a03fd
commit 02c9f19
Show file tree

Hide file tree

Showing 15 changed files with 819 additions and 31 deletions.
diff --git a/.github/dependabot.yml b/.github/dependabot.yml
@@ -0,0 +1,9 @@
+version: 2
+updates:
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    schedule:
+      # Check for updates to GitHub Actions every weekday
+      interval: "daily"
+    labels:
+      - "dependencies"
diff --git a/.github/workflows/ci_build.yaml b/.github/workflows/ci_build.yaml
@@ -35,7 +35,16 @@ jobs:
 
       - name: repo checkout
         uses: actions/checkout@v3
-
+
+      - name: Initialise variables
+        run: |
+          # Only deploy if the build follows from pushing to master
+          if [[ '${{ github.ref }}' == 'refs/heads/main' ]]; then
+             echo "DOC_DEPLOY=true" >> $GITHUB_ENV
+          else
+             echo "DOC_DEPLOY=false" >> $GITHUB_ENV
+          fi
+          
       - name: container registry log in
         uses: docker/login-action@v3
         with:
@@ -56,19 +65,21 @@ jobs:
               sudo chown -R coq:coq .
             endGroup
           script: |
-            startGroup "Build Coq lib"
-              cd theories/
-              make -j ${{ steps.cpu-cores.outputs.count }} pretty-timed
+            startGroup "Build binary"
+              if [[ "$DOC" ]]; then
+                make coqdoc
+              else
+                make
+              fi
             endGroup
           after_script: |
-            startGroup "Build binary"
-              cd ..
-              make
+            startGroup "after"
             endGroup
           export: "OPAMJOBS OPAMYES"
         env:
           OPAMJOBS: ${{ steps.cpu-cores.outputs.count }}
           OPAMYES: "true"
+          DOC: ${{ env.DOC_DEPLOY }}
 
       - name: permissions revert
         # to avoid a warning at cleanup time

diff --git a/.gitignore b/.gitignore
@@ -18,6 +18,7 @@ CoqMakefile.mk*
 !CoqMakefile.mk.local
 !CoqMakefile.mk.local-late
 *.log
+theories/html/
 
 # Editor related
 ## Emacs

diff --git a/Makefile b/Makefile
@@ -1,10 +1,13 @@
 .PHONY: all clean
 
 all:
-	@make -C theories
+	@$(MAKE) -C theories
 	@dune build
 
+coqdoc: all
+	@${MAKE} coqdoc -C theories
+
 clean:
-	@make clean -C theories
+	@$(MAKE) clean -C theories
 	@dune clean
 	@echo "Cleaning finished."
diff --git a/README.md b/README.md
@@ -9,6 +9,9 @@ sound and complete: a program passes typechecking if and only if it is a well-ty
 program in MLTT. This will be the first verified proof assistant (despite being
 elementary) and serves as a basis for future extensions. 
 
+## Online Documentation
+
+We have generated a [Coqdoc](toc.html) for browsing our Coq proof.
 
 ## Architecture
 
@@ -67,19 +70,21 @@ opam install ppx_inline_test
 
 ## Development
 
-Before anything, the Coq parser must be extracted to OCaml code. Then, you can run `dune build` like normal for all other changes.
+Use the toplevel `make` to build the whole project:
+```
+make
+```
+Makefile will try to find out the number of your CPU cores and parallel as much as
+possible.
 
-You can build changes to the Coq parser with the following commands:
+Once `make` finishes, you can run the binary:
 ```
-cd theories
-make -j16 # or the number of your cpus
-cd ..
-dune build
+_build/default/driver/mcltt.exe examples/nary.mcl # or your own example
 ```
 
-Then you can interact with the parser at the toplevel with `dune utop`:
+To build Coq proof only, you can go into and only build the Coq folder:
 ```
-# open Mcltt;;
-# open Parser.Cst;;
-# Main.parse "<expression to parse>"
+cd theories
+make
 ```
+
diff --git a/assets/extra/footer.html b/assets/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/coq-community/coqdocjs">CoqdocJS</a>
+</div>
+</div>
+</body>
+
+</html>
diff --git a/assets/extra/header.html b/assets/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="resources/coqdoc.css" rel="stylesheet" type="text/css" />
+<link href="resources/coqdocjs.css" rel="stylesheet" type="text/css"/>
+<script type="text/javascript" src="resources/config.js"></script>
+<script type="text/javascript" src="resources/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">
diff --git a/assets/extra/resources/config.js b/assets/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 = ["==>","<=>", "=>", "->", "<-", ":="];