Merge pull request #73 from Zimmi48/update-meta

Update with latest version of templates.

Author: spitters

.travis.yml

@@ -1,51 +1,64 @@
-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 -n -k path
+      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" --argstr bignums-url "$BIGNUMS" --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
+  # Test supported versions of Coq via Nix
   - env:
-      COQ=https://github.com/coq/coq-on-cachix/tarball/master
-      BIGNUMS=https://github.com/coq/bignums/tarball/master
-  - env: COQ=8.9
-  - env: COQ=8.8
-  - env: COQ=8.7
-  - env: COQ=8.6
+    - COQ=8.10
+    <<: *NIX
+  - env:
+    - COQ=8.9
+    <<: *NIX
+  - env:
+    - COQ=8.8
+    <<: *NIX
+  - env:
+    - COQ=8.7
+    <<: *NIX
+  - env:
+    - COQ=8.6
+    <<: *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=math-classes
+    - CONTRIB_NAME=coq-math-classes
     - 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
+

README.md

@@ -6,9 +6,6 @@
 [![Gitter][gitter-shield]][gitter-link]
 [![DOI][doi-shield]][doi-link]
 
-[doi-shield]: https://zenodo.org/badge/DOI/10.1017/S0960129511000119.svg
-[doi-link]: https://doi.org/10.1017/S0960129511000119
-
 [travis-shield]: https://travis-ci.com/coq-community/math-classes.svg?branch=master
 [travis-link]: https://travis-ci.com/coq-community/math-classes/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.1017/S0960129511000119.svg
+[doi-link]: https://doi.org/10.1017/S0960129511000119
+
 A library of abstract interfaces for mathematical structures in Coq.
 
 
@@ -33,18 +33,17 @@ More details about the project can be found in the paper
   - Eelis van der Weegen (initial)
   - Bas Spitters (initial)
   - Robbert Krebbers (initial)
-- Maintainer(s):
+- Coq-community maintainer(s):
   - Bas Spitters ([**@spitters**](https://github.com/spitters))
 - License: [Public Domain](LICENSE)
 - Compatible Coq versions: Coq 8.6 or later (use releases for other Coq versions)
-- Additional dependencies:
+- Additional Coq dependencies:
   - [BigNums](https://github.com/coq/bignums)
 
-
 ## 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 Math Classes
+is via [OPAM](https://opam.ocaml.org/doc/Install.html):
 
 ```shell
 opam repo add coq-released https://coq.inria.fr/opam/released
@@ -64,6 +63,7 @@ make install
 After installation, the included modules are available under
 the `MathClasses` namespace.
 
+
 ## Directory structure
 
 ### categories/

default.nix

@@ -1,4 +1,4 @@
-{ pkgs ? (import <nixpkgs> {}), coq-version-or-url, bignums-url ? "", shell ? false }:
+{ pkgs ? (import <nixpkgs> {}), coq-version-or-url, shell ? false }:
 
 let
   coq-version-parts = builtins.match "([0-9]+).([0-9]+)" coq-version-or-url;
@@ -7,11 +7,6 @@ let
       pkgs.mkCoqPackages (import (fetchTarball coq-version-or-url) {})
     else
       pkgs."coqPackages_${builtins.concatStringsSep "_" coq-version-parts}";
-  bignums =
-    if bignums-url == "" then coqPackages.bignums else
-      coqPackages.bignums.overrideAttrs (o: {
-        src = fetchTarball https://github.com/coq/bignums/archive/master.tar.gz;
-      });
 in
 
 with coqPackages;

opam renamed to math-classes.opam

@@ -1,19 +1,24 @@
-opam-version: "1.2"
+opam-version: "2.0"
 maintainer: "[email protected]"
 
 homepage: "https://github.com/coq-community/math-classes"
-dev-repo: "https://github.com/coq-community/math-classes.git"
+dev-repo: "git+https://github.com/coq-community/math-classes.git"
 bug-reports: "https://github.com/coq-community/math-classes/issues"
 license: "Public Domain"
 
+synopsis: ""
+description: """
+A library of abstract interfaces for mathematical structures in Coq.
+"""
+
 build: [
   [ "./configure.sh" ]
   [ make "-j%{jobs}%" ]
 ]
 install: [make "install"]
-remove: ["rm" "-R" "%{lib}%/coq/user-contrib/MathClasses"]
 depends: [
-  "coq" {(>= "8.6" & < "8.10~") | (= "dev")}
+  "ocaml"
+  "coq" {(>= "8.6" & < "8.11~") | (= "dev")}
   "coq-bignums" 
 ]
 

meta.yml

@@ -2,6 +2,7 @@
 fullname: Math Classes
 shortname: math-classes
 organization: coq-community
+community: true
 
 description: |
   A library of abstract interfaces for mathematical structures in Coq.
@@ -27,20 +28,21 @@ opam-file-maintainer: [email protected]
 
 license:
   fullname: Public Domain
-  shortname: Public Domain
+  identifier: Public Domain
 
 supported_coq_versions:
   text: Coq 8.6 or later (use releases for other Coq versions)
-  opam: '{(>= "8.6" & < "8.10~") | (= "dev")}'
+  opam: '{(>= "8.6" & < "8.11~") | (= "dev")}'
 
-tested_coq_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: 8.6
+tested_coq_nix_versions:
+- version_or_url: "8.10"
+- version_or_url: "8.9"
+- version_or_url: "8.8"
+- version_or_url: "8.7"
+- version_or_url: "8.6"
 
-tested_coq_opam_version: dev
+tested_coq_opam_versions:
+- version: dev
 
 dependencies:
 - opam: