Merge pull request #97 from Zimmi48/update-templates

Regenerate files from latest templates.

.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
 

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 <number-of-cores-on-your-machine>
 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`.
 
+
+

corn.opam → coq-corn.opam

@@ -1,5 +1,6 @@
 opam-version: "2.0"
 maintainer: "[email protected]"
+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"
 ]

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}/";
 }

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 <number-of-cores-on-your-machine>
+  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 <number-of-cores-on-your-machine>
+  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`.
-
 ---