Merge pull request #84 from Zimmi48/update-meta-8.11

Update meta.yml to test Coq 8.11 (and wrt latest templates).

.travis.yml

@@ -1,44 +1,50 @@
-opam: &OPAM
-  language: minimal
-  sudo: required
+os: linux
+dist: bionic
+language: shell
+
+.opam: &OPAM
+  language: shell
   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 run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/${PACKAGE} -w /home/coq/${PACKAGE} ${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 pin add ${PACKAGE} . -y -n -k path
+      opam install ${PACKAGE} -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'
+  - echo -e "${ANSI_YELLOW}Building ${PACKAGE}...${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}
+      sudo chown -R coq:coq /home/coq/${PACKAGE}
+      opam install ${PACKAGE} -v -y -j ${NJOBS}
       "
   - docker stop COQ  # optional
   - echo -en 'travis_fold:end:script\\r'
 
-nix: &NIX
+.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:
+jobs:
   include:
 
   # Test supported versions of Coq via Nix
+  - env:
+    - COQ=8.11
+    <<: *NIX
   - env:
     - COQ=8.10
     <<: *NIX
@@ -51,14 +57,16 @@ matrix:
   - env:
     - COQ=8.7
     <<: *NIX
-  - env:
-    - COQ=8.6
-    <<: *NIX
 
   # Test supported versions of Coq via OPAM
   - env:
     - COQ_IMAGE=coqorg/coq:dev
-    - CONTRIB_NAME=coq-math-classes
+    - PACKAGE=coq-math-classes.dev
+    - NJOBS=2
+    <<: *OPAM
+  - env:
+    - COQ_IMAGE=coqorg/coq:8.6
+    - PACKAGE=coq-math-classes.dev
     - NJOBS=2
     <<: *OPAM
 

README.md

@@ -18,6 +18,7 @@
 [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
 
@@ -36,9 +37,6 @@ algebraic manipulation (e.g. rewriting) and idiomatic use of
 notations.
 
 
-More details about the project can be found in the paper
-[Type Classes for Mathematics in Type Theory](https://arxiv.org/abs/1102.1323).
-
 ## Meta
 
 - Author(s):
@@ -49,8 +47,11 @@ More details about the project can be found in the paper
   - 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 Coq dependencies:
+- Additional dependencies:
   - [BigNums](https://github.com/coq/bignums)
+- Coq namespace: `MathClasses`
+- Related publication(s):
+  - [Type Classes for Mathematics in Type Theory](https://arxiv.org/abs/1102.1323) doi:[10.1017/S0960129511000119](https://doi.org/10.1017/S0960129511000119)
 
 ## Building and installation instructions
 
@@ -65,16 +66,13 @@ opam install coq-math-classes
 To instead build and install manually, do:
 
 ``` shell
-git clone https://github.com/coq-community/math-classes
+git clone https://github.com/coq-community/math-classes.git
 cd math-classes
 ./configure.sh
 make   # or make -j <number-of-cores-on-your-machine>
 make install
 ```
 
-After installation, the included modules are available under
-the `MathClasses` namespace.
-
 
 ## Directory structure
 

coq-math-classes.opam

@@ -1,5 +1,6 @@
 opam-version: "2.0"
 maintainer: "b.a.w.spitters@gmail.com"
+version: "dev"
 
 homepage: "https://github.com/coq-community/math-classes"
 dev-repo: "git+https://github.com/coq-community/math-classes.git"
@@ -29,8 +30,7 @@ build: [
 ]
 install: [make "install"]
 depends: [
-  "ocaml"
-  "coq" {(>= "8.6" & < "8.11~") | (= "dev")}
+  "coq" {(>= "8.6" & < "8.12~") | (= "dev")}
   "coq-bignums" 
 ]
 

default.nix

@@ -22,5 +22,5 @@ pkgs.stdenv.mkDerivation {
 
   src = if shell then null else ./.;
 
-  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
+  installFlags = "COQMF_COQLIB=$(out)/lib/coq/${coq.coq-version}/";
 }

meta.yml

@@ -3,6 +3,8 @@ fullname: Math Classes
 shortname: math-classes
 organization: coq-community
 community: true
+travis: true
+doi: 10.1017/S0960129511000119
 
 synopsis: >-
   A library of abstract interfaces for mathematical structures in Coq.
@@ -22,10 +24,10 @@ description: |
   algebraic manipulation (e.g. rewriting) and idiomatic use of
   notations.
 
-paper:
-  doi: 10.1017/S0960129511000119
-  url: https://arxiv.org/abs/1102.1323
-  title: Type Classes for Mathematics in Type Theory
+publications:
+- pub_doi: 10.1017/S0960129511000119
+  pub_url: https://arxiv.org/abs/1102.1323
+  pub_title: Type Classes for Mathematics in Type Theory
 
 authors:
 - name: Eelis van der Weegen
@@ -47,17 +49,18 @@ license:
 
 supported_coq_versions:
   text: Coq 8.6 or later (use releases for other Coq versions)
-  opam: '{(>= "8.6" & < "8.11~") | (= "dev")}'
+  opam: '{(>= "8.6" & < "8.12~") | (= "dev")}'
 
 tested_coq_nix_versions:
+- version_or_url: "8.11"
 - 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_versions:
 - version: dev
+- version: "8.6"
 
 dependencies:
 - opam: