diff --git a/.travis.yml b/.travis.yml index d64667114..e53763982 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,41 +1,45 @@ -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 + nix: 2.3.5 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 @@ -51,14 +55,11 @@ 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-corn + - PACKAGE=coq-corn.dev - NJOBS=2 <<: *OPAM diff --git a/README.md b/README.md index 4525780a6..81897c1e6 100644 --- a/README.md +++ b/README.md @@ -3,7 +3,7 @@ [![Travis][travis-shield]][travis-link] [![Contributing][contributing-shield]][contributing-link] [![Code of Conduct][conduct-shield]][conduct-link] -[![Gitter][gitter-shield]][gitter-link] +[![Zulip][zulip-shield]][zulip-link] [travis-shield]: https://travis-ci.com/coq-community/corn.svg?branch=master [travis-link]: https://travis-ci.com/coq-community/corn/builds @@ -14,8 +14,9 @@ [conduct-shield]: https://img.shields.io/badge/%E2%9D%A4-code%20of%20conduct-%23f15a24.svg [conduct-link]: https://github.com/coq-community/manifesto/blob/master/CODE_OF_CONDUCT.md -[gitter-shield]: https://img.shields.io/badge/chat-on%20gitter-%23c1272d.svg -[gitter-link]: https://gitter.im/coq-community/Lobby +[zulip-shield]: https://img.shields.io/badge/chat-on%20zulip-%23c1272d.svg +[zulip-link]: https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users + CoRN includes the following parts: @@ -49,7 +50,6 @@ CoRN includes the following parts: integrals, graphs of functions, differential equations. - ## Meta - Author(s): @@ -83,13 +83,15 @@ CoRN includes the following parts: - Bas Spitters ([**@spitters**](https://github.com/spitters)) - Vincent Semeria ([**@vincentse**](https://github.com/vincentse)) - License: [GNU General Public License v2](LICENSE) -- Compatible Coq versions: Coq 8.6 or greater -- Additional Coq dependencies: +- Compatible Coq versions: Coq 8.7 or greater +- Additional dependencies: - [Math-Classes](https://github.com/coq-community/math-classes) 8.8.1 or greater, which is a library of abstract interfaces for mathematical structures that is heavily based on Coq's type classes. - - [Bignums](https://github.com/coq/bignums) + - [Bignums](https://github/com/coq/bignums) +- Coq namespace: `CoRN` +- Related publication(s): none ## Building and installation instructions @@ -124,10 +126,6 @@ make # or make -j make install ``` -After installation, the included modules are available under -the `CoRN` namespace. - - ### Building C-CoRN with SCons C-CoRN supports building with [SCons](http://www.scons.org/). SCons is a modern @@ -148,3 +146,5 @@ For more information, see the [SCons documentation](http://www.scons.org/). To build CoqDoc documentation, say `scons coqdoc`. + + diff --git a/corn.opam b/coq-corn.opam similarity index 96% rename from corn.opam rename to coq-corn.opam index c59a91675..8d7bba8bf 100644 --- a/corn.opam +++ b/coq-corn.opam @@ -1,5 +1,6 @@ opam-version: "2.0" maintainer: "b.a.w.spitters@gmail.com" +version: "dev" homepage: "https://github.com/coq-community/corn" dev-repo: "git+https://github.com/coq-community/corn.git" @@ -45,8 +46,7 @@ build: [ ] install: [make "install"] depends: [ - "ocaml" - "coq" {(>= "8.6" & < "8.11~") | (= "dev")} + "coq" {(>= "8.7" & < "8.13~") | (= "dev")} "coq-math-classes" {(>= "8.8.1") | (= "dev")} "coq-bignums" ] @@ -88,4 +88,5 @@ authors: [ "Pierre Letouzey" "Lionel Mamane" "Nickolay Shmyrev" + "Vincent Semeria" ] diff --git a/default.nix b/default.nix index 755eff999..45f680eae 100644 --- a/default.nix +++ b/default.nix @@ -29,5 +29,5 @@ pkgs.stdenv.mkDerivation { configurePhase = "sh ./configure.sh"; - 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 ade9753fe..2137db0f7 100644 --- a/meta.yml +++ b/meta.yml @@ -3,6 +3,7 @@ fullname: C-CoRN shortname: corn organization: coq-community community: true +travis: true synopsis: The Coq Constructive Repository at Nijmegen. @@ -63,6 +64,7 @@ authors: - name: Pierre Letouzey - name: Lionel Mamane - name: Nickolay Shmyrev +- name: Vincent Semeria maintainers: - name: Bas Spitters @@ -77,15 +79,14 @@ license: identifier: GPL-2.0 supported_coq_versions: - text: Coq 8.6 or greater - opam: '{(>= "8.6" & < "8.11~") | (= "dev")}' + text: Coq 8.7 or greater + opam: '{(>= "8.7" & < "8.13~") | (= "dev")}' 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_versions: - version: dev @@ -118,7 +119,40 @@ categories: - name: Mathematics/Real Calculus and Topology - name: Mathematics/Exact Real computation -documentation: | +build: | + ## Building and installation instructions + + The easiest way to install the latest released version of C-CoRN + 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-corn + ``` + + To instead build and install manually, you have to start with + the `bignums` dependency: + + ``` shell + git clone https://github.com/coq/bignums + cd bignums + make # or make -j + make install + ``` + + The last `make install` is necessary, it copies `bignums` to + a common folder, which is usually `coq/user-contrib`. Afterwards + the similar commands for `math-classes` will find `bignums` there. + Finally build `corn` itself: + + ``` shell + git clone https://github.com/coq-community/corn + cd corn + ./configure.sh + make # or make -j + make install + ``` + ### Building C-CoRN with SCons C-CoRN supports building with [SCons](http://www.scons.org/). SCons is a modern @@ -138,5 +172,4 @@ documentation: | ### Building documentation To build CoqDoc documentation, say `scons coqdoc`. - ---