Merge pull request #12 from coq-community/update-ci

Update CI and documentation

.gitignore

@@ -9,3 +9,5 @@ run_huffman.ml
 *.glob
 *.vo
 *.vio
+*.vok
+*.vos

.travis.yml

@@ -5,27 +5,27 @@ opam: &OPAM
   install: |
     # Prepare the COQ container
     docker pull ${COQ_IMAGE}
-    docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/${CONTRIB_NAME} -w /home/coq/${CONTRIB_NAME} ${COQ_IMAGE}
+    docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/${PACKAGE} -w /home/coq/${PACKAGE} ${COQ_IMAGE}
     docker exec COQ /bin/bash --login -c "
       # This bash script is double-quoted to interpolate Travis CI env vars:
       echo \"Build triggered by ${TRAVIS_EVENT_TYPE}\"
       export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
       set -ex  # -e = exit on failure; -x = trace for debug
       opam update -y
-      opam pin add ${CONTRIB_NAME} . -y --no-action
-      opam install ${CONTRIB_NAME} -y -j ${NJOBS} --deps-only
+      opam pin add ${PACKAGE} . -y -n -k path
+      opam install ${PACKAGE} -y -j ${NJOBS} --deps-only
       opam config list
       opam repo list
       opam list
       "
   script:
-  - echo -e "${ANSI_YELLOW}Building ${CONTRIB_NAME}...${ANSI_RESET}" && echo -en 'travis_fold:start:script\\r'
+  - echo -e "${ANSI_YELLOW}Building ${PACKAGE}...${ANSI_RESET}" && echo -en 'travis_fold:start:script\\r'
   - |
     docker exec COQ /bin/bash --login -c "
       export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
       set -ex
-      sudo chown -R coq:coq /home/coq/${CONTRIB_NAME}
-      opam install ${CONTRIB_NAME} -v -y -j ${NJOBS}
+      sudo chown -R coq:coq /home/coq/${PACKAGE}
+      opam install ${PACKAGE} -v -y -j ${NJOBS}
       "
   - docker stop COQ  # optional
   - echo -en 'travis_fold:end:script\\r'
@@ -42,6 +42,12 @@ matrix:
   - env:
     - COQ=https://github.com/coq/coq-on-cachix/tarball/master
     <<: *NIX
+  - env:
+    - COQ=https://github.com/coq/coq-on-cachix/tarball/v8.11
+    <<: *NIX
+  - env:
+    - COQ=8.10
+    <<: *NIX
   - env:
     - COQ=8.9
     <<: *NIX
@@ -55,7 +61,7 @@ matrix:
   # Test supported versions of Coq via OPAM
   - env:
     - COQ_IMAGE=coqorg/coq:dev
-    - CONTRIB_NAME=coq-huffman
+    - PACKAGE=coq-huffman.dev
     - NJOBS=2
     <<: *OPAM
 

Makefile.coq.local

@@ -1,7 +1,5 @@
-post-all:: run_huffman.ml
-
 clean::
-	$(HIDE)rm -f huffman.ml huffman.mli run_hoffman.ml
+	$(HIDE)rm -f huffman.ml huffman.mli run_huffman.ml
 
 run_huffman.ml: src/ex1.ml src/ex2.ml theories/Extraction.vo
 	cat src/ex1.ml huffman.ml src/ex2.ml > run_huffman.ml

README.md

@@ -22,8 +22,6 @@ This projects contains a Coq proof of the correctness of the Huffman coding algo
 as described in David A. Huffman's paper A Method for the Construction of Minimum-Redundancy
 Codes, Proc. IRE, pp. 1098-1101, September 1952.
 
-
-
 ## Meta
 
 - Author(s):
@@ -33,6 +31,9 @@ Codes, Proc. IRE, pp. 1098-1101, September 1952.
 - License: [GNU Lesser General Public License v2.1 or later](LICENSE)
 - Compatible Coq versions: 8.7 or later
 - Additional Coq dependencies: none
+- Coq namespace: `Huffman`
+- Related publication(s):
+  - [Formalising Huffman's algorithm](https://hal.archives-ouvertes.fr/hal-02149909) 
 
 ## Building and installation instructions
 
@@ -53,13 +54,15 @@ make   # or make -j <number-of-cores-on-your-machine>
 make install
 ```
 
-After installation, the included modules are available under
-the `Huffman` namespace.
-
 
 ## Documentation
 
-To run the algorithm, open an OCaml toplevel (`ocaml`) and do
+To run the extracted algorithm, build the project and then run
+```
+make run_huffman.ml
+```
+
+Next, open an OCaml toplevel (e.g., `ocaml`) and do
 ```ocaml
 #use "run_huffman.ml";;
 ```
@@ -79,13 +82,9 @@ To decode a string:
 decode code c;;
 ```
 
-A [technical report][report] describes the formalization.
-
 Some more information on the development is also available:
 ftp://ftp-sop.inria.fr/marelle/Laurent.Thery/Huffman/index.html
 
 See also the [paper on the algorithm][paper].
 
-[report]: https://hal.archives-ouvertes.fr/hal-02149909
 [paper]: http://compression.ru/download/articles/huff/huffman_1952_minimum-redundancy-codes.pdf
-

_CoqProject

@@ -1,7 +1,6 @@
 -Q theories Huffman
 
 -arg -w -arg +default
--arg -w -arg -auto-template
 
 theories/Aux.v
 theories/Cover.v

coq-huffman.opam

@@ -1,5 +1,6 @@
 opam-version: "2.0"
 maintainer: "palmskog@gmail.com"
+version: "dev"
 
 homepage: "https://github.com/coq-community/huffman"
 dev-repo: "git+https://github.com/coq-community/huffman.git"
@@ -10,14 +11,13 @@ synopsis: "A Coq proof of the correctness of the Huffman coding algorithm"
 description: """
 This projects contains a Coq proof of the correctness of the Huffman coding algorithm,
 as described in David A. Huffman's paper A Method for the Construction of Minimum-Redundancy
-Codes, Proc. IRE, pp. 1098-1101, September 1952.
-"""
+Codes, Proc. IRE, pp. 1098-1101, September 1952."""
 
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
   "ocaml"
-  "coq" {(>= "8.7" & < "8.11~") | (= "dev")}
+  "coq" {(>= "8.7" & < "8.12~") | (= "dev")}
 ]
 
 tags: [

meta.yml

@@ -3,14 +3,19 @@ fullname: Huffman
 shortname: huffman
 organization: coq-community
 community: true
+travis: true
 
 synopsis: A Coq proof of the correctness of the Huffman coding algorithm
 
-description: |
+description: |-
   This projects contains a Coq proof of the correctness of the Huffman coding algorithm,
   as described in David A. Huffman's paper A Method for the Construction of Minimum-Redundancy
   Codes, Proc. IRE, pp. 1098-1101, September 1952.
 
+publications:
+- pub_url: https://hal.archives-ouvertes.fr/hal-02149909
+  pub_title: Formalising Huffman's algorithm
+
 authors:
 - name: Laurent Théry
   initial: true
@@ -21,19 +26,23 @@ maintainers:
 
 opam-file-maintainer: palmskog@gmail.com
 
+opam-file-version: dev
+
 license:
   fullname: GNU Lesser General Public License v2.1 or later
   identifier: LGPL-2.1-or-later
 
 supported_coq_versions:
   text: 8.7 or later
-  opam: '{(>= "8.7" & < "8.11~") | (= "dev")}'
+  opam: '{(>= "8.7" & < "8.12~") | (= "dev")}'
 
 tested_coq_nix_versions:
 - version_or_url: https://github.com/coq/coq-on-cachix/tarball/master
-- version_or_url: 8.9
-- version_or_url: 8.8
-- version_or_url: 8.7
+- version_or_url: https://github.com/coq/coq-on-cachix/tarball/v8.11
+- version_or_url: '8.10'
+- version_or_url: '8.9'
+- version_or_url: '8.8'
+- version_or_url: '8.7'
 
 tested_coq_opam_versions:
 - version: dev
@@ -49,10 +58,15 @@ categories:
 - name: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms
 - name: Miscellaneous/Extracted Programs/Combinatorics
 
-documentation: |
+documentation: |-
   ## Documentation
 
-  To run the algorithm, open an OCaml toplevel (`ocaml`) and do
+  To run the extracted algorithm, build the project and then run
+  ```
+  make run_huffman.ml
+  ```
+
+  Next, open an OCaml toplevel (e.g., `ocaml`) and do
   ```ocaml
   #use "run_huffman.ml";;
   ```
@@ -72,13 +86,10 @@ documentation: |
   decode code c;;
   ```
 
-  A [technical report][report] describes the formalization.
-
   Some more information on the development is also available:
   ftp://ftp-sop.inria.fr/marelle/Laurent.Thery/Huffman/index.html
 
   See also the [paper on the algorithm][paper].
 
-  [report]: https://hal.archives-ouvertes.fr/hal-02149909
   [paper]: http://compression.ru/download/articles/huff/huffman_1952_minimum-redundancy-codes.pdf
 ---