Merge pull request #44 from coq-community/v8.9+update-templates

update 8.9 templates
coq-community · May 16, 2019 · a7039f3 · a7039f3
2 parents 069dc3b + cf8b991
commit a7039f3
Show file tree

Hide file tree

Showing 4 changed files with 77 additions and 52 deletions.
diff --git a/.travis.yml b/.travis.yml
@@ -1,45 +1,52 @@
-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=8.9
+  # Test supported versions of Coq via Nix
+  - env:
+    - COQ=8.9
+    <<: *NIX
 
-  # Test opam package
-  - language: minimal
-    sudo: required
-    services: docker
-    env:
+  # Test supported versions of Coq via OPAM
+  - env:
     - COQ_IMAGE=coqorg/coq:8.9
-    - CONTRIB_NAME=aac-tactics
+    - CONTRIB_NAME=coq-aac-tactics
     - 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 -y -j ${NJOBS} .
-        "
-    - docker stop COQ  # optional
-    - echo -en 'travis_fold:end:script\\r'
+    <<: *OPAM
+
diff --git a/README.md b/README.md
@@ -1,14 +1,11 @@
-# AAC tactics
+# AAC Tactics
 
 [![Travis][travis-shield]][travis-link]
 [![Contributing][contributing-shield]][contributing-link]
 [![Code of Conduct][conduct-shield]][conduct-link]
 [![Gitter][gitter-shield]][gitter-link]
 [![DOI][doi-shield]][doi-link]
 
-[doi-shield]: https://zenodo.org/badge/DOI/10.1007/978-3-642-25379-9_14.svg
-[doi-link]: https://doi.org/10.1007/978-3-642-25379-9_14
-
 [travis-shield]: https://travis-ci.com/coq-community/aac-tactics.svg?branch=master
 [travis-link]: https://travis-ci.com/coq-community/aac-tactics/builds
 
@@ -21,6 +18,9 @@
 [gitter-shield]: https://img.shields.io/badge/chat-on%20gitter-%23c1272d.svg
 [gitter-link]: https://gitter.im/coq-community/Lobby
 
+[doi-shield]: https://zenodo.org/badge/DOI/10.1007/978-3-642-25379-9_14.svg
+[doi-link]: https://doi.org/10.1007/978-3-642-25379-9_14
+
 This Coq plugin provides tactics for rewriting universally quantified
 equations, modulo associativity and commutativity of some operator.
 The tactics can be applied for custom operators by registering the
@@ -42,14 +42,14 @@ More details about the project can be found in the paper
   - Fabian Kunze ([**@fakusb**](https://github.com/fakusb))
   - Karl Palmskog ([**@palmskog**](https://github.com/palmskog))
 - License: [GNU Lesser General Public License v3.0 or later](LICENSE)
-- Compatible Coq versions: Coq 8.9 (use the corresponding branch or release for other Coq versions)
+- Compatible Coq versions: 8.9 (use the corresponding branch or release for other Coq versions)
 - Compatible OCaml versions: all versions supported by Coq
-- Additional dependencies: none
+- 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 AAC Tactics
+is via [OPAM](https://opam.ocaml.org/doc/Install.html):
 
 ```shell
 opam repo add coq-released https://coq.inria.fr/opam/released
@@ -68,6 +68,7 @@ make install
 After installation, the included modules are available under
 the `AAC_tactics` namespace.
 
+
 ## Documentation
 
 The following example shows an application of the tactics for reasoning over Z binary numbers:

diff --git a/opam → coq-aac-tactics.opam b/opam → coq-aac-tactics.opam
@@ -1,15 +1,25 @@
-opam-version: "1.2"
+opam-version: "2.0"
 maintainer: "palmskog@gmail.com"
 
 homepage: "https://github.com/coq-community/aac-tactics"
-dev-repo: "https://github.com/coq-community/aac-tactics.git"
+dev-repo: "git+https://github.com/coq-community/aac-tactics.git"
 bug-reports: "https://github.com/coq-community/aac-tactics/issues"
 license: "LGPL-3.0-or-later"
 
+synopsis: "This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators"
+description: """
+This Coq plugin provides tactics for rewriting universally quantified
+equations, modulo associativity and commutativity of some operator.
+The tactics can be applied for custom operators by registering the
+operators and their properties as type class instances. Many common
+operator instances, such as for Z binary arithmetic and booleans, are
+provided with the plugin.
+"""
+
 build: [make "-j%{jobs}%"]
 install: [make "install"]
-remove: ["rm" "-R" "%{lib}%/coq/user-contrib/AAC_tactics"]
 depends: [
+  "ocaml"
   "coq" {>= "8.9" & < "8.10~"}
 ]
 

diff --git a/meta.yml b/meta.yml
@@ -1,6 +1,12 @@
 ---
-fullname: AAC tactics
+fullname: AAC Tactics
 shortname: aac-tactics
+organization: coq-community
+community: true
+
+synopsis: >-
+  This Coq plugin provides tactics for rewriting universally quantified
+  equations, modulo associative (and possibly commutative) operators
 
 description: |
   This Coq plugin provides tactics for rewriting universally quantified
@@ -38,13 +44,14 @@ license:
 plugin: true
 
 supported_coq_versions:
-  text: Coq 8.9 (use the corresponding branch or release for other Coq versions)
+  text: 8.9 (use the corresponding branch or release for other Coq versions)
   opam: '{>= "8.9" & < "8.10~"}'
 
-tested_coq_versions:
+tested_coq_nix_versions:
 - version_or_url: 8.9
 
-tested_coq_opam_version: 8.9
+tested_coq_opam_versions:
+- version: 8.9
 
 namespace: AAC_tactics