Merge pull request #7 from coq-community/reorg-files

Reorganize files, add coqdoc and table of contents

.github/workflows/deploy-coqdoc.yml

@@ -0,0 +1,54 @@
+name: Build and Deploy coqdoc
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build-coqdoc:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Set up Git repository
+        uses: actions/checkout@v2
+
+      - name: Build coqdoc
+        uses: coq-community/docker-coq-action@v1
+        with:
+          custom_image: 'coqorg/coq:dev'
+          custom_script: |
+            {{before_install}}
+            startGroup "Build mmaps dependencies"
+              opam pin add -n -y -k path coq-mmaps .
+              opam update -y
+              opam install -y -j "$(nproc)" coq-mmaps --deps-only
+            endGroup
+            startGroup "Add permissions"
+              sudo chown -R coq:coq .
+            endGroup
+            startGroup "Build coqdoc"
+              make -j "$(nproc)"
+              make coqdoc
+            endGroup
+
+      - name: Revert Coq user permissions
+        # to avoid a warning at cleanup time
+        if: ${{ always() }}
+        run: sudo chown -R 1001:116 .
+
+      - name: Copy HTML and CSS and JavaScript
+        run: |
+          mkdir public
+          cp -r resources/index.html docs/ public/
+
+      - name: Deploy to GitHub pages
+        if: github.event_name == 'push' && github.ref == 'refs/heads/master'
+        uses: crazy-max/ghaction-github-pages@v2
+        with:
+          build_dir: public
+          jekyll: false
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.gitignore

@@ -8,3 +8,5 @@
 .Makefile.coq.d
 Makefile.coq
 Makefile.coq.conf
+_build/
+docs/

Makefile.coq.local

@@ -0,0 +1,20 @@
+GLOBFILES = $(VFILES:.v=.glob)
+CSSFILES = resources/coqdoc.css resources/coqdocjs.css
+JSFILES = resources/config.js resources/coqdocjs.js
+HTMLFILES = resources/header.html resources/footer.html
+COQDOCDIR = docs/coqdoc
+
+COQDOCHTMLFLAGS = --toc --toc-depth 3 --index indexpage --html --utf8 -s \
+  --interpolate --no-lib-name --parse-comments \
+  --with-header resources/header.html --with-footer resources/footer.html
+
+coqdoc: $(GLOBFILES) $(VFILES) $(CSSFILES) $(JSFILES) $(HTMLFILES)
+	$(SHOW)'COQDOC -d $(COQDOCDIR)'
+	$(HIDE)mkdir -p $(COQDOCDIR)
+	$(HIDE)$(COQDOC) $(COQDOCHTMLFLAGS) $(COQDOCLIBS) -d $(COQDOCDIR) $(VFILES)
+	$(SHOW)'COPY resources'
+	$(HIDE)cp $(CSSFILES) $(JSFILES) $(COQDOCDIR)
+.PHONY: coqdoc
+
+resources/index.html: resources/index.md
+	pandoc -s -o $@ $<

README.md

@@ -23,10 +23,11 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 
 
-This project contains several implementations of finite maps
-over arbitrary ordered types using Coq functors. This is an
-updated version of Coq Stdlib's FMaps. It is meant to complement
-the MSet library.
+This project contains several implementations of finite maps,
+including implementations based on AVL trees and red-black trees.
+The finite maps are parameterized on arbitrary ordered types using
+Coq functors. This is an updated version of the Coq Stdlib's FMaps
+that is meant to complement the Stdlib's MSet library.
 
 ## Meta
 
@@ -35,15 +36,25 @@ the MSet library.
 - Coq-community maintainer(s):
   - Pierre Letouzey ([**@letouzey**](https://github.com/letouzey))
   - Karl Palmskog ([**@palmskog**](https://github.com/palmskog))
-- License: [GNU Lesser General Public License v2.1](LICENSE)
+- License: [GNU Lesser General Public License v2.1 only](LICENSE)
 - Compatible Coq versions: 8.14 and later
 - Additional dependencies: none
 - Coq namespace: `MMaps`
-- Related publication(s): none
+- Related publication(s):
+  - [Efficient Verified Red-Black Trees](https://www.cs.princeton.edu/~appel/papers/redblack.pdf) 
+  - [Functors for Proofs and Programs](https://hal.inria.fr/hal-00150913) doi:[10.1007/978-3-540-24725-8_26](https://doi.org/10.1007/978-3-540-24725-8_26)
 
 ## Building and installation instructions
 
-To build and install manually, do:
+The easiest way to install the latest released version of Modular Finite Maps over Ordered Types
+is via [OPAM](https://opam.ocaml.org/doc/Install.html):
+
+```shell
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam install coq-mmaps
+```
+
+To instead build and install manually, do:
 
 ``` shell
 git clone https://github.com/coq-community/coq-mmaps.git
@@ -52,6 +63,7 @@ make   # or make -j <number-of-cores-on-your-machine>
 make install
 ```
 
+
 ## Documentation
 
 As a starting point, you may consider [MMaps.Interface](Interface.v)

_CoqProject

@@ -1,16 +1,17 @@
--R . MMaps
-Utils.v
-Comparisons.v
-Interface.v
-Facts.v
-Raw.v
-WeakList.v
-OrdList.v
-Positive.v
-GenTree.v
-AVL.v
-AVLproofs.v
-RBT.v
-RBTproofs.v
-MMaps.v
-demo.v
+-R theories MMaps
+
+theories/Utils.v
+theories/Comparisons.v
+theories/Interface.v
+theories/Raw.v
+theories/Facts.v
+theories/WeakList.v
+theories/OrdList.v
+theories/Positive.v
+theories/GenTree.v
+theories/AVL.v
+theories/AVLproofs.v
+theories/RBT.v
+theories/RBTproofs.v
+theories/MMaps.v
+theories/demo.v

coq-mmaps.opam

@@ -12,10 +12,11 @@ license: "LGPL-2.1-only"
 
 synopsis: "Several implementations of finite maps over arbitrary ordered types using Coq functors"
 description: """
-This project contains several implementations of finite maps
-over arbitrary ordered types using Coq functors. This is an
-updated version of Coq Stdlib's FMaps. It is meant to complement
-the MSet library."""
+This project contains several implementations of finite maps,
+including implementations based on AVL trees and red-black trees.
+The finite maps are parameterized on arbitrary ordered types using
+Coq functors. This is an updated version of the Coq Stdlib's FMaps
+that is meant to complement the Stdlib's MSet library."""
 
 build: [make "-j%{jobs}%"]
 install: [make "install"]

dune-project

@@ -0,0 +1,3 @@
+(lang dune 2.5)
+(using coq 0.2)
+(name coq-mmaps)

meta.yml

@@ -9,10 +9,18 @@ action: true
 synopsis: Several implementations of finite maps over arbitrary ordered types using Coq functors
 
 description: |-
-  This project contains several implementations of finite maps
-  over arbitrary ordered types using Coq functors. This is an
-  updated version of Coq Stdlib's FMaps. It is meant to complement
-  the MSet library.
+  This project contains several implementations of finite maps,
+  including implementations based on AVL trees and red-black trees.
+  The finite maps are parameterized on arbitrary ordered types using
+  Coq functors. This is an updated version of the Coq Stdlib's FMaps
+  that is meant to complement the Stdlib's MSet library.
+
+publications:
+- pub_url: https://www.cs.princeton.edu/~appel/papers/redblack.pdf
+  pub_title: Efficient Verified Red-Black Trees
+- pub_url: https://hal.inria.fr/hal-00150913
+  pub_title: Functors for Proofs and Programs
+  pub_doi: 10.1007/978-3-540-24725-8_26
 
 authors:
 - name: Pierre Letouzey
@@ -29,7 +37,7 @@ opam-file-maintainer: [email protected]
 opam-file-version: dev
 
 license:
-  fullname: GNU Lesser General Public License v2.1
+  fullname: GNU Lesser General Public License v2.1 only
   identifier: LGPL-2.1-only
 
 supported_coq_versions:
@@ -53,18 +61,6 @@ keywords:
 categories:
 - name: Computer Science/Data Types and Data Structures
 
-build: |-
-  ## Building and installation instructions
-
-  To build and install manually, do:
-
-  ``` shell
-  git clone https://github.com/coq-community/coq-mmaps.git
-  cd coq-mmaps
-  make   # or make -j <number-of-cores-on-your-machine> 
-  make install
-  ```
-
 documentation: |-
   ## Documentation
 

resources/config.js

@@ -0,0 +1,79 @@
+var coqdocjs = coqdocjs || {};
+
+coqdocjs.repl = {
+    "forall": "∀",
+    "exists": "∃",
+    "~": "¬",
+    "/\\": "∧",
+    "\\/": "∨",
+    "->": "→",
+    "<-": "←",
+    "<->": "↔",
+    "=>": "⇒",
+    "<>": "≠",
+    "<=": "≤",
+    ">=": "≥",
+    "el": "∈",
+    "nel": "∉",
+    "<<=": "⊆",
+    "|-": "⊢",
+    ">>": "»",
+    "<<": "⊆",
+    "++": "⧺",
+    "===": "≡",
+    "=/=": "≢",
+    "=~=": "≅",
+    "==>": "⟹",
+    "<==": "⟸",
+    "False": "⊥",
+    "True": "⊤",
+    ":=": "≔",
+    "-|": "⊣",
+    "*": "×",
+    "::": "∷",
+    "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 = ["==>","<=>", "=>", "->", "<-", ":="];