Merge pull request #7 from coq-community/meta-files

update Makefile and generate files from templates

Author: palmskog

.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/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/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=qarith-stern-brocot
+    - CONTRIB_NAME=coq-qarith-stern-brocot
     - 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
+

Makefile

@@ -1,16 +1,16 @@
 all: Makefile.coq
-	+make -f Makefile.coq all
+	+$(MAKE) -f Makefile.coq all
 
 clean: Makefile.coq
-	+make -f Makefile.coq clean
-	rm -f Makefile.coq
+	+$(MAKE) -f Makefile.coq cleanall
+	rm -f Makefile.coq Makefile.coq.conf
 
 Makefile.coq: _CoqProject
 	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
-_CoqProject: ;
+_CoqProject Makefile: ;
 
 %: Makefile.coq
-	+make -f Makefile.coq $@
+	+$(MAKE) -f Makefile.coq $@
 
 .PHONY: all clean

README.md

@@ -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-540-24849-1_20.svg
-[doi-link]: https://doi.org/10.1007/978-3-540-24849-1_20
-
 [travis-shield]: https://travis-ci.com/coq-community/qarith-stern-brocot.svg?branch=master
 [travis-link]: https://travis-ci.com/coq-community/qarith-stern-brocot/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-540-24849-1_20.svg
+[doi-link]: https://doi.org/10.1007/978-3-540-24849-1_20
+
 Development of rational numbers as finite binary lists and defining
 field operations on them in two different ways: strict and lazy.
 
@@ -36,13 +36,13 @@ More details about the project can be found in the paper
 - Coq-community maintainer(s):
   - Hugo Herbelin ([**@herbelin**](https://github.com/herbelin))
 - License: [GNU Lesser General Public License v2.1 or later](LICENSE)
-- Compatible Coq versions: Coq 8.7 or greater (use releases for other Coq versions)
-- Additional dependencies: none
+- Compatible Coq versions: 8.7 or later (use releases for other Coq versions)
+- 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 Binary Rational Numbers
+is via [OPAM](https://opam.ocaml.org/doc/Install.html):
 
 ```shell
 opam repo add coq-released https://coq.inria.fr/opam/released
@@ -61,6 +61,7 @@ make install
 After installation, the included modules are available under
 the `QArithSternBrocot` namespace.
 
+
 ## Documentation
 
 This package contains a rational arithmetic library for Coq.

opam coq-qarith-stern-brocot.opamopam renamed to coq-qarith-stern-brocot.opam

@@ -1,16 +1,22 @@
-opam-version: "1.2"
+opam-version: "2.0"
 maintainer: "[email protected]"
 
 homepage: "https://github.com/coq-community/qarith-stern-brocot"
-dev-repo: "https://github.com/coq-community/qarith-stern-brocot.git"
+dev-repo: "git+https://github.com/coq-community/qarith-stern-brocot.git"
 bug-reports: "https://github.com/coq-community/qarith-stern-brocot/issues"
 license: "LGPL-2.1-or-later"
 
+synopsis: "Binary rational numbers"
+description: """
+Development of rational numbers as finite binary lists and defining
+field operations on them in two different ways: strict and lazy.
+"""
+
 build: [make "-j%{jobs}%"]
 install: [make "install"]
-remove: ["rm" "-R" "%{lib}%/coq/user-contrib/QArithSternBrocot"]
 depends: [
-  "coq" {(>= "8.7" & < "8.10~") | (= "dev")}
+  "ocaml"
+  "coq" {(>= "8.7" & < "8.11~") | (= "dev")}
 ]
 
 tags: [

meta.yml

@@ -1,6 +1,10 @@
 ---
 fullname: Binary Rational Numbers
 shortname: qarith-stern-brocot
+organization: coq-community
+community: true
+
+synopsis: Binary rational numbers
 
 description: |
   Development of rational numbers as finite binary lists and defining
@@ -26,16 +30,17 @@ license:
   identifier: LGPL-2.1-or-later
 
 supported_coq_versions:
-  text: Coq 8.7 or greater (use releases for other Coq versions)
-  opam: '{(>= "8.7" & < "8.10~") | (= "dev")}'
+  text: 8.7 or later (use releases for other Coq versions)
+  opam: '{(>= "8.7" & < "8.11~") | (= "dev")}'
 
-tested_coq_versions:
+tested_coq_nix_versions:
 - version_or_url: https://github.com/coq/coq/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: QArithSternBrocot