From 72a60c395c9fb525b87acc280a521dafae24b4f2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Wed, 1 Apr 2020 11:20:07 +0200 Subject: [PATCH] Update meta.yml to test Coq 8.11 (and wrt latest templates). --- .travis.yml | 38 +++++++++++++++++++++++--------------- README.md | 14 ++++++-------- coq-math-classes.opam | 4 ++-- default.nix | 2 +- meta.yml | 15 +++++++++------ 5 files changed, 41 insertions(+), 32 deletions(-) diff --git a/.travis.yml b/.travis.yml index d5db5d04..82ad15b8 100644 --- a/.travis.yml +++ b/.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 diff --git a/README.md b/README.md index 1f2896af..95086df9 100644 --- a/README.md +++ b/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 make install ``` -After installation, the included modules are available under -the `MathClasses` namespace. - ## Directory structure diff --git a/coq-math-classes.opam b/coq-math-classes.opam index 4cb4b2a5..c39c484b 100644 --- a/coq-math-classes.opam +++ b/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" ] diff --git a/default.nix b/default.nix index ada7be5a..aa519071 100644 --- a/default.nix +++ b/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}/"; } diff --git a/meta.yml b/meta.yml index 3fa46245..39813a17 100644 --- a/meta.yml +++ b/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: