Revert "Update ocaml_version for coq:dev CI to run. Closes #23" (#25)

Set CI to use 'default' version of OCaml

.github/workflows/coq-action.yml

@@ -7,21 +7,23 @@ on:
     branches: ['**'] # for all submitted Pull Requests
 
 jobs:
-  coq:
+  build:
     runs-on: ubuntu-latest
     strategy:
       matrix:
         coq_version:
+          - '8.12'
           - '8.13'
           - '8.14'
           - '8.15'
           - 'dev'
         ocaml_version:
-          - '4.12-flambda'
+          - 'default'
       fail-fast: false # don't stop jobs if one fails
     steps:
       - uses: actions/checkout@v2
       - uses: coq-community/docker-coq-action@v1
         with:
           coq_version: ${{ matrix.coq_version }}
           ocaml_version: ${{ matrix.ocaml_version }}
+

.gitignore

@@ -52,4 +52,4 @@ Makefile.coq*
 
 _build
 
-html
+docs

Makefile

@@ -13,7 +13,7 @@ uninstall:
 # hacky :) we should replace with dune in a future version
 FILES=$(shell find . -name "*.v" -depth 1) 
 doc: all
-	mkdir -p html
-	cd _build/default && coqdoc -g --utf8 --toc --no-lib-name -d ../../html -R . QuantumLib $(FILES)
+	mkdir -p docs
+	cd _build/default && coqdoc -g --utf8 --toc --no-lib-name -d ../../docs -R . QuantumLib $(FILES)
 
 .PHONY: all clean install uninstall doc

README.md

@@ -1,6 +1,10 @@
 # QuantumLib
 
 [![CI](https://github.com/inQWIRE/QuantumLib/actions/workflows/coq-action.yml/badge.svg)](https://github.com/inQWIRE/QuantumLib/actions/workflows/coq-action.yml)
+[![coqdoc][coqdoc-shield]][coqdoc-link]
+
+[coqdoc-shield]: https://img.shields.io/badge/docs-coqdoc-blue.svg
+[coqdoc-link]: https://inqwire.github.io/QuantumLib/toc.html
 
 QuantumLib is a Coq library for reasoning about quantum programs. It was co-developed with (and is used in) several other projects in inQWIRE including [QWIRE](https://github.com/inQWIRE/QWIRE), [SQIR](https://github.com/inQWIRE/SQIR), and [VyZX](https://github.com/inQWIRE/VyZX).
 
@@ -10,18 +14,14 @@ Tested with Coq versions 8.12 -- 8.15.
 
 To compile run `make all`.
 
-## To Use With Other Projects
-
-To install QuantumLib, simply run `opam pin coq-quantumlib https://github.com/inQWIRE/QuantumLib.git`. This should allow you to import QuantumLib files into other Coq files. Once QuantumLib is an official opam library, the command will be `opam install coq-quantumlib`. When importing/exporting specific files, one should refer to QuantumLib files as `QuantumLib.FILENAME`.
-
-## Documentation
+## Using With Other Projects
 
-Run `make doc` to generate documentation.
-
-**TODO: host generated documentation on a GitHub page**
+To install QuantumLib, run `opam pin coq-quantumlib https://github.com/inQWIRE/QuantumLib.git`. This should allow you to import QuantumLib files into other Coq files. To pull subsequent updates, run `opam install coq-quantumlib`. When importing/exporting specific files, refer to QuantumLib files as `QuantumLib.FILENAME`.
 
 ## Directory Contents
 
+Auto-generated documentation is available at https://inqwire.github.io/QuantumLib/toc.html.
+
 * Complex.v - Definition of Complex numbers, extending [Coquelicot](http://coquelicot.saclay.inria.fr/)'s.
 * Ctopology.v - A topology of open/closed sets is defined for the complex numbers, with lemmas about compactness.
 * DiscreteProb.v - Theory of discrete probability distributions and utility to describe running a quantum program ("apply_u") and sampling from the output distribution.