Merge pull request #19 from coq-community/ci-boilerpolate

add meta.yml and generate README.md, opam file and CI configuration

.github/workflows/docker-action.yml

@@ -0,0 +1,36 @@
+# 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:dev'
+          - 'coqorg/coq:8.19'
+          - 'coqorg/coq:8.18'
+          - 'coqorg/coq:8.17'
+          - 'coqorg/coq:8.16'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v3
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-dedekind-reals.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

README.md

@@ -1,30 +1,68 @@
-A formalization of the Dedekind real numbers in Coq.
+<!---
+This file was generated from `meta.yml`, please do not edit manually.
+Follow the instructions on https://github.com/coq-community/templates to regenerate.
+--->
+# Dedekind Reals
 
-The formalization started as a student project at the University of Ljubljana,
-under the supervision of Andrej Bauer <[email protected]>, and was brought
-to the present state by Vincent Semeria <[email protected]>.
+[![Docker CI][docker-action-shield]][docker-action-link]
+[![Contributing][contributing-shield]][contributing-link]
+[![Code of Conduct][conduct-shield]][conduct-link]
+[![Zulip][zulip-shield]][zulip-link]
 
-At this point the formalization of the field of reals is finished. There are
-still several unfinished theorems concering the lattice-theoretic structure of
-the reals (search for `todo` in the Coq files). We would be delighted by
-contributions that would bring the formalization closer to completion.
+[docker-action-shield]: https://github.com/coq-community/dedekind-reals/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/dedekind-reals/actions/workflows/docker-action.yml
 
-#### Compilation instruction
+[contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
+[contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
 
-A fairly recent version of Coq should do. Run `make` to compile the files:
+[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
 
-* `make` -- to compile
-* `make all` -- to make all that is to be made
-* `make clean` -- to remove the compiled files
-* `make html` -- to make the HTML documentation
-* `make install` -- installs files as the library `DedekindReals`
+[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
 
-#### Structure of the modules
 
-* `MiscLemmas`: various lemmas about rational numbers
-* `Cut`: definition of Dedekind cuts and several other basic notions
-* `Additive`: Additive structure of the reals
-* `Multiplication` : Multiplicative structure of the relas
-* `Order` : The order on the reals
-* `Archimedean`: the proof that the reals satisfy the archimedean property
-* `Completeness`: the reals are Dedekind-complete
+
+A formalization of Dedekind reals numbers that started as a
+student project at the University of Ljubljana under the supervision
+of Andrej Bauer, and was brought to the present state by Vincent Semeria.
+
+At this point the formalization of the field of reals is finished.
+There are still several unfinished theorems concering the lattice-theoretic
+structure of the reals (search for `todo` in the Coq files). We would be
+delighted by contributions that would bring the formalization
+closer to completion.
+
+## Meta
+
+- Author(s):
+  - Andrej Bauer
+  - Vincent Semeria
+- Coq-community maintainer(s):
+  - Andrej Bauer ([**@andrejbauer**](https://github.com/andrejbauer))
+- License: [MIT License](LICENSE)
+- Compatible Coq versions: 8.16 and later
+- Additional dependencies: none
+- Coq namespace: `DedekindReals`
+- Related publication(s): none
+
+## Building instructions
+
+To build and install, do:
+
+```shell
+git clone https://github.com/coq-community/dedekind-reals.git
+cd dedekind-reals
+make   # or make -j <number-of-cores-on-your-machine> 
+make install
+```
+
+## Structure of the modules
+
+- `MiscLemmas`: various lemmas about rational numbers
+- `Cut`: definition of Dedekind cuts and several other basic notions
+- `Additive`: Additive structure of the reals
+- `Multiplication` : Multiplicative structure of the relas
+- `Order` : The order on the reals
+- `Archimedean`: the proof that the reals satisfy the archimedean property
+- `Completeness`: the reals are Dedekind-complete

coq-dedekind-reals.opam

@@ -0,0 +1,40 @@
+# 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: "[email protected]"
+version: "dev"
+
+homepage: "https://github.com/coq-community/dedekind-reals"
+dev-repo: "git+https://github.com/coq-community/dedekind-reals.git"
+bug-reports: "https://github.com/coq-community/dedekind-reals/issues"
+license: "MIT"
+
+synopsis: "A formalization of the Dedekind real numbers in Coq"
+description: """
+A formalization of Dedekind reals numbers that started as a
+student project at the University of Ljubljana under the supervision
+of Andrej Bauer, and was brought to the present state by Vincent Semeria.
+
+At this point the formalization of the field of reals is finished.
+There are still several unfinished theorems concering the lattice-theoretic
+structure of the reals (search for `todo` in the Coq files). We would be
+delighted by contributions that would bring the formalization
+closer to completion."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {>= "8.16"}
+]
+
+tags: [
+  "category:Mathematics/Real Calculus and Topology"
+  "keyword:real numbers"
+  "keyword:analysis"
+  "logpath:DedekindReals"
+]
+authors: [
+  "Andrej Bauer <[email protected]>"
+  "Vincent Semeria <[email protected]>"
+]

meta.yml

@@ -0,0 +1,81 @@
+---
+fullname: Dedekind Reals
+shortname: dedekind-reals
+organization: coq-community
+community: true
+action: true
+
+synopsis: A formalization of the Dedekind real numbers in Coq
+
+description: |-
+  A formalization of Dedekind reals numbers that started as a
+  student project at the University of Ljubljana under the supervision
+  of Andrej Bauer, and was brought to the present state by Vincent Semeria.
+
+  At this point the formalization of the field of reals is finished.
+  There are still several unfinished theorems concering the lattice-theoretic
+  structure of the reals (search for `todo` in the Coq files). We would be
+  delighted by contributions that would bring the formalization
+  closer to completion.
+
+authors:
+- name: Andrej Bauer
+  email: [email protected]
+- name: Vincent Semeria
+  email: [email protected]
+
+maintainers:
+- name: Andrej Bauer
+  nickname: andrejbauer
+
+opam-file-maintainer: [email protected]
+
+opam-file-version: dev
+
+build: |-
+  ## Building instructions
+  
+  To build and install, do:
+  
+  ```shell
+  git clone https://github.com/coq-community/dedekind-reals.git
+  cd dedekind-reals
+  make   # or make -j <number-of-cores-on-your-machine> 
+  make install
+  ```
+
+license:
+  fullname: MIT License
+  identifier: MIT
+
+supported_coq_versions:
+  text: 8.16 and later
+  opam: '{>= "8.16"}'
+
+tested_coq_opam_versions:
+- version: 'dev'
+- version: '8.19'
+- version: '8.18'
+- version: '8.17'
+- version: '8.16'
+
+namespace: DedekindReals
+
+keywords:
+- name: real numbers
+- name: analysis
+
+categories:
+- name: Mathematics/Real Calculus and Topology
+
+documentation: |-
+  ## Structure of the modules
+  
+  - `MiscLemmas`: various lemmas about rational numbers
+  - `Cut`: definition of Dedekind cuts and several other basic notions
+  - `Additive`: Additive structure of the reals
+  - `Multiplication` : Multiplicative structure of the relas
+  - `Order` : The order on the reals
+  - `Archimedean`: the proof that the reals satisfy the archimedean property
+  - `Completeness`: the reals are Dedekind-complete
+---