diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml new file mode 100644 index 0000000..aeff0bb --- /dev/null +++ b/.github/workflows/docker-action.yml @@ -0,0 +1,38 @@ +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. +name: Docker CI + +on: + push: + branches: + - master + pull_request: + branches: + - '**' + +jobs: + build: + # the OS must be GNU/Linux to be able to use the docker-coq-action + runs-on: ubuntu-latest + strategy: + matrix: + image: + - 'coqorg/coq:8.8' + - 'coqorg/coq:8.9' + - 'coqorg/coq:8.10' + - 'coqorg/coq:8.11' + - 'coqorg/coq:8.12' + - 'coqorg/coq:8.13' + - 'coqorg/coq:8.14' + - 'coqorg/coq:dev' + fail-fast: false + steps: + - uses: actions/checkout@v2 + - uses: coq-community/docker-coq-action@v1 + with: + opam_file: 'coq-mathcomp-bigenough.opam' + custom_image: ${{ matrix.image }} + +# See also: +# https://github.com/coq-community/docker-coq-action#readme +# https://github.com/erikmd/docker-coq-github-action-demo diff --git a/.travis.yml b/.travis.yml deleted file mode 100644 index fc0b875..0000000 --- a/.travis.yml +++ /dev/null @@ -1,59 +0,0 @@ -dist: trusty -sudo: required -language: generic - -branches: - only: - - master - -services: - - docker - -env: - global: - - NJOBS="2" - - CONTRIB_NAME="bigenough" - matrix: - - DOCKERIMAGE="mathcomp/mathcomp:1.7.0-coq-8.7" - - DOCKERIMAGE="mathcomp/mathcomp:1.7.0-coq-8.8" - - DOCKERIMAGE="mathcomp/mathcomp:1.7.0-coq-8.9" - - DOCKERIMAGE="mathcomp/mathcomp:1.7.0-coq-dev" - - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.7" - - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.8" - - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.9" - - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-dev" - -install: | - # Prepare the COQ container - docker pull "${DOCKERIMAGE}" - docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/${CONTRIB_NAME} -w /home/coq/${CONTRIB_NAME} "${DOCKERIMAGE}" - 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 - # Using flambda makes sense here as we usually get ~10% faster - # builds in math-comp. - opam switch \$COMPILER_EDGE - eval \$(opam env) - opam update -y - opam config list - opam repo list - opam list - sudo chown -R coq:coq /home/coq/${CONTRIB_NAME} - opam pin add -y -n coq-mathcomp-bigenough . - # install deps only - opam install -y -vvv --deps-only coq-mathcomp-bigenough - " -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 - eval \$(opam env) - opam install -y -vvv coq-mathcomp-bigenough - " -- docker stop COQ # optional -- echo -en 'travis_fold:end:script\\r' - diff --git a/README.md b/README.md index e904fda..d80ead6 100644 --- a/README.md +++ b/README.md @@ -1,18 +1,58 @@ -[![Build Status](https://travis-ci.org/math-comp/bigenough.svg?branch=master)](https://travis-ci.org/math-comp/bigenough) + +# bigenough -# A small library to do epsilon - N reasoning. +[![Docker CI][docker-action-shield]][docker-action-link] -The repository contains a package to reasoning with big enough objects (mostly natural numbers). +[docker-action-shield]: https://github.com/math-comp/bigenough/workflows/Docker%20CI/badge.svg?branch=master +[docker-action-link]: https://github.com/math-comp/bigenough/actions?query=workflow:"Docker%20CI" -This repository is essentially for archiving purposes as `bigenough` will be subsumed by the [near tactics](https://github.com/math-comp/analysis/blob/9bfd5a1971c6989f51d9c44341bb71b2fd5e3c76/topology.v#L93). -The formalization is based on the [Mathematical Components](https://github.com/math-comp/math-comp) library for the [Coq](https://coq.inria.fr) proof assistant, although it requires only the ssreflect package. -## Installation -If you already have OPAM installed: +The package contains a package to reasoning with big enough objects +(mostly natural numbers). This package is essentially for backward +compatibility purposes as `bigenough` will be subsumed by the near +tactics. The formalization is based on the Mathematical Components +library. -``` +## Meta + +- Author(s): + - Cyril Cohen +- License: [CeCILL-B](LICENSE) +- Compatible Coq versions: 8.8 or later +- Additional dependencies: + - [MathComp ssreflect](https://math-comp.github.io) 1.6 or later +- Coq namespace: `mathcomp.bigenough` +- Related publication(s): none + +## Building and installation instructions + +The easiest way to install the latest released version of bigenough +is via [OPAM](https://opam.ocaml.org/doc/Install.html): + +```shell opam repo add coq-released https://coq.inria.fr/opam/released opam install coq-mathcomp-bigenough ``` + +To instead build and install manually, do: + +``` shell +git clone https://github.com/math-comp/bigenough.git +cd bigenough +make # or make -j +make install +``` + + +# A small library to do epsilon - N reasoning. + +This repository is essentially for archiving purposes as `bigenough` +will be subsumed by the [near tactics](https://github.com/math-comp/analysis/blob/9bfd5a1971c6989f51d9c44341bb71b2fd5e3c76/topology.v#L93). + +The formalization is based on the [Mathematical Components](https://github.com/math-comp/math-comp) library for the [Coq](https://coq.inria.fr) proof assistant, +although it requires only the ssreflect package. diff --git a/coq-mathcomp-bigenough.opam b/coq-mathcomp-bigenough.opam new file mode 100644 index 0000000..1f6af63 --- /dev/null +++ b/coq-mathcomp-bigenough.opam @@ -0,0 +1,37 @@ +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. + +opam-version: "2.0" +maintainer: "Cyril Cohen " +version: "dev" + +homepage: "https://github.com/math-comp/bigenough" +dev-repo: "git+https://github.com/math-comp/bigenough.git" +bug-reports: "https://github.com/math-comp/bigenough/issues" +license: "CeCILL-B" + +synopsis: "A small library to do epsilon - N reasoning" +description: """ +The package contains a package to reasoning with big enough objects +(mostly natural numbers). This package is essentially for backward +compatibility purposes as `bigenough` will be subsumed by the near +tactics. The formalization is based on the Mathematical Components +library.""" + +build: [make "-j%{jobs}%"] +install: [make "install"] +depends: [ + "coq" {(>= "8.8" & < "8.15~") | (= "dev")} + "coq-mathcomp-ssreflect" {>= "1.6"} +] + +tags: [ + "keyword:bigenough" + "keyword:asymptotic reasonning" + "keyword:small scale reflection" + "keyword:mathematical components" + "logpath:mathcomp.bigenough" +] +authors: [ + "Cyril Cohen" +] diff --git a/meta.yml b/meta.yml new file mode 100644 index 0000000..259829b --- /dev/null +++ b/meta.yml @@ -0,0 +1,73 @@ +--- +fullname: bigenough +shortname: bigenough +opam_name: coq-mathcomp-bigenough +organization: math-comp +community: false +action: true +coqdoc: false +dune: false + +synopsis: >- + A small library to do epsilon - N reasoning + +description: |- + The package contains a package to reasoning with big enough objects + (mostly natural numbers). This package is essentially for backward + compatibility purposes as `bigenough` will be subsumed by the near + tactics. The formalization is based on the Mathematical Components + library. + +authors: +- name: Cyril Cohen + +maintainers: +- name: Cyril Cohen + nickname: CohenCyril + +opam-file-maintainer: 'Cyril Cohen ' + +opam-file-version: 'dev' + +license: + fullname: CeCILL-B + identifier: CeCILL-B + +supported_coq_versions: + text: '8.8 or later' + opam: '{(>= "8.8" & < "8.15~") | (= "dev")}' + +dependencies: +- opam: + name: coq-mathcomp-ssreflect + version: '{>= "1.6"}' + description: |- + [MathComp ssreflect](https://math-comp.github.io) 1.6 or later + +tested_coq_opam_versions: +- version: '8.8' +- version: '8.9' +- version: '8.10' +- version: '8.11' +- version: '8.12' +- version: '8.13' +- version: '8.14' +- version: 'dev' + +namespace: mathcomp.bigenough + +keywords: +- name: bigenough +- name: asymptotic reasonning +- name: small scale reflection +- name: mathematical components + +documentation: |- + # A small library to do epsilon - N reasoning. + + This repository is essentially for archiving purposes as `bigenough` + will be subsumed by the [near tactics](https://github.com/math-comp/analysis/blob/9bfd5a1971c6989f51d9c44341bb71b2fd5e3c76/topology.v#L93). + + The formalization is based on the [Mathematical Components](https://github.com/math-comp/math-comp) library for the [Coq](https://coq.inria.fr) proof assistant, + although it requires only the ssreflect package. +---