From cf8b991ead6770f7f7a00f29b089fd82d7d3a256 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Thu, 16 May 2019 13:36:42 -0500 Subject: [PATCH] update 8.9 templates --- .travis.yml | 81 ++++++++++++++++++++---------------- README.md | 17 ++++---- opam => coq-aac-tactics.opam | 16 +++++-- meta.yml | 15 +++++-- 4 files changed, 77 insertions(+), 52 deletions(-) rename opam => coq-aac-tactics.opam (52%) diff --git a/.travis.yml b/.travis.yml index 8e6b2c4..cb05b4c 100644 --- 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 index c70f1bf..af959bc 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -# AAC tactics +# AAC Tactics [![Travis][travis-shield]][travis-link] [![Contributing][contributing-shield]][contributing-link] @@ -6,9 +6,6 @@ [![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 b/coq-aac-tactics.opam similarity index 52% rename from opam rename to coq-aac-tactics.opam index cd6aa36..32b1f8f 100644 --- a/opam +++ b/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 index bc7f672..6b9396e 100644 --- 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