Merge pull request #10 from coq-community/update-opam-8.10

update with latest templates, support for 8.10
coq-community · May 15, 2019 · 949424f · 949424f
2 parents fe9993a + 22a7661
commit 949424f
Show file tree

Hide file tree

Showing 4 changed files with 67 additions and 52 deletions.
diff --git a/.travis.yml b/.travis.yml
@@ -1,48 +1,61 @@
-language: nix
+opam: &OPAM
+  language: minimal
+  sudo: required
+  services: docker
+  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 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 config list
+      opam repo list
+      opam list
+      "
+  script:
+  - echo -e "${ANSI_YELLOW}Building ${CONTRIB_NAME}...${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}
+      "
+  - docker stop COQ  # optional
+  - echo -en 'travis_fold:end:script\\r'
 
-script:
-- nix-build --argstr coq-version-or-url "$COQ" --extra-substituters https://coq.cachix.org --trusted-public-keys "cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= coq.cachix.org-1:5QW/wwEnD+l2jvN6QRbRRsa4hBHG3QiQQ26cxu1F5tI="
+nix: &NIX
+  language: nix
+  script:
+  - nix-build --argstr coq-version-or-url "$COQ" --extra-substituters https://coq.cachix.org --trusted-public-keys "cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= coq.cachix.org-1:5QW/wwEnD+l2jvN6QRbRRsa4hBHG3QiQQ26cxu1F5tI="
 
 matrix:
   include:
 
-  # Test supported versions of Coq
-  - env: COQ=https://github.com/coq/coq-on-cachix/tarball/master
-  - env: COQ=8.9
-  - env: COQ=8.8
-  - env: COQ=8.7
+  # Test supported versions of Coq via Nix
+  - env:
+    - COQ=https://github.com/coq/coq-on-cachix/tarball/master
+    <<: *NIX
+  - env:
+    - COQ=8.9
+    <<: *NIX
+  - env:
+    - COQ=8.8
+    <<: *NIX
+  - env:
+    - COQ=8.7
+    <<: *NIX
 
-  # Test opam package
-  - language: minimal
-    sudo: required
-    services: docker
-    env:
+  # Test supported versions of Coq via OPAM
+  - env:
     - COQ_IMAGE=coqorg/coq:dev
-    - CONTRIB_NAME=huffman
+    - CONTRIB_NAME=coq-huffman
     - NJOBS=2
-    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 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 install -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'
-    - |
-      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 -v -y -j ${NJOBS} .
-        "
-    - docker stop COQ  # optional
-    - echo -en 'travis_fold:end:script\\r'
+    <<: *OPAM
+
diff --git a/README.md b/README.md
@@ -17,6 +17,7 @@
 [gitter-shield]: https://img.shields.io/badge/chat-on%20gitter-%23c1272d.svg
 [gitter-link]: https://gitter.im/coq-community/Lobby
 
+
 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.
@@ -27,16 +28,16 @@ Codes, Proc. IRE, pp. 1098-1101, September 1952.
 
 - Author(s):
   - Laurent Théry (initial)
-- Maintainer(s):
+- Coq-community maintainer(s):
   - Karl Palmskog ([**@palmskog**](https://github.com/palmskog))
 - License: [GNU Lesser General Public License v2.1 or later](LICENSE)
-- Compatible Coq versions: Coq 8.7 or later
-- Additional dependencies: none
+- Compatible Coq versions: 8.7 or later
+- Additional Coq dependencies: none
 
 ## Building and installation instructions
 
-The easiest way to install the latest released version is via
-[OPAM](https://opam.ocaml.org/doc/Install.html):
+The easiest way to install the latest released version of Huffman
+is via [OPAM](https://opam.ocaml.org/doc/Install.html):
 
 ```shell
 opam repo add coq-released https://coq.inria.fr/opam/released
@@ -55,6 +56,7 @@ 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

diff --git a/opam → coq-huffman.opam b/opam → coq-huffman.opam
@@ -15,11 +15,9 @@ Codes, Proc. IRE, pp. 1098-1101, September 1952.
 
 build: [make "-j%{jobs}%"]
 install: [make "install"]
-remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Huffman"]
-flags: light-uninstall
 depends: [
   "ocaml"
-  "coq" {(>= "8.7" & < "8.10~") | (= "dev")}
+  "coq" {(>= "8.7" & < "8.11~") | (= "dev")}
 ]
 
 tags: [

diff --git a/meta.yml b/meta.yml
@@ -2,6 +2,7 @@
 fullname: Huffman
 shortname: huffman
 organization: coq-community
+community: true
 
 synopsis: A Coq proof of the correctness of the Huffman coding algorithm
 
@@ -25,16 +26,17 @@ license:
   identifier: LGPL-2.1-or-later
 
 supported_coq_versions:
-  text: Coq 8.7 or later
-  opam: '{(>= "8.7" & < "8.10~") | (= "dev")}'
+  text: 8.7 or later
+  opam: '{(>= "8.7" & < "8.11~") | (= "dev")}'
 
-tested_coq_versions:
+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
 
-tested_coq_opam_version: dev
+tested_coq_opam_versions:
+- version: dev
 
 namespace: Huffman