Merge pull request #79 from math-comp/prep_release_1.5.1

Preparing next release

.github/workflows/coq-action.yml

@@ -0,0 +1,38 @@
+name: 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:
+          - 'mathcomp/mathcomp:1.11.0-coq-8.10'
+          - 'mathcomp/mathcomp:1.11.0-coq-8.11'
+          - 'mathcomp/mathcomp:1.11.0-coq-8.12'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.10'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.11'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.12'
+          - 'mathcomp/mathcomp-dev:coq-8.10'
+          - 'mathcomp/mathcomp-dev:coq-8.11'
+          - 'mathcomp/mathcomp-dev:coq-8.12'
+          - 'mathcomp/mathcomp-dev:coq-dev'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v2
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-mathcomp-finmap.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

CeCILL-B → CECILL-B

@@ -16,7 +16,7 @@ the two main principles guiding its drafting:
       both authors and holders of the economic rights over software.
 
 The authors of the CeCILL-B (for Ce[a] C[nrs] I[nria] L[ogiciel] L[ibre])
-license are: 
+license are:
 
 Commissariat � l'Energie Atomique - CEA, a public scientific, technical
 and industrial research establishment, having its principal place of
@@ -402,8 +402,8 @@ rights set forth in Article 5).
 
 9.3 The Licensee acknowledges that the Software is supplied "as is" by
 the Licensor without any other express or tacit warranty, other than
-that provided for in Article 9.2 and, in particular, without any warranty 
-as to its commercial value, its secured, safe, innovative or relevant 
+that provided for in Article 9.2 and, in particular, without any warranty
+as to its commercial value, its secured, safe, innovative or relevant
 nature.
 
 Specifically, the Licensor does not warrant that the Software is free

README.md

@@ -1,33 +1,73 @@
-[![Build Status](https://travis-ci.org/math-comp/finmap.svg?branch=master)](https://travis-ci.org/math-comp/finmap)
+# Finite maps
 
-# A finset and finmap library
+[![CI][action-shield]][action-link]
 
-## AUTHORS
+[action-shield]: https://github.com/math-comp/finmap/workflows/CI/badge.svg?branch=master
+[action-link]: https://github.com/math-comp/finmap/actions?query=workflow%3ACI
 
-Cyril Cohen,
-Kazuhiko Sakaguchi (for the order library now moved to the main math-comp repository)
-and contributions from various people https://github.com/math-comp/finmap/graphs/contributors
 
-# RELATED WORK
 
-This library was developed independently but inspired from Pierre-Yves
-Strub's library (https://github.com/strub/ssrmisc/blob/master/fset.v),
-from Christian Doczkal's library
-(https://www.ps.uni-saarland.de/formalizations/fset/html/libs.fset.html)
-and from Beta Ziliani's work (no reference provided so far).
 
-This library should ultimately be integrated to the mathematical
-components library, when it is finished.
+This library is an extension of mathematical component in order to
+support finite sets and finite maps on choicetypes (rather that finite
+types). This includes support for functions with finite support and
+multisets. The library also contains a generic order and set libary,
+which will be used to subsume notations for finite sets, eventually.
+
+## Meta
+
+- Author(s):
+  - Cyril Cohen (initial)
+  - Kazuhiko Sakaguchi
+- License: [CeCILL-B](CECILL-B)
+- Compatible Coq versions: Coq 8.10 to 8.12
+- Additional dependencies:
+  - [MathComp ssreflect 1.10 to 1.12](https://math-comp.github.io)
+  - [MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough)
+- Coq namespace: `mathcomp.finmap`
+- Related publication(s): none
+
+## Building and installation instructions
+
+The easiest way to install the latest released version of Finite maps
+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-finmap
+```
+
+To instead build and install manually, do:
 
-## DOCUMENTATION
+``` shell
+git clone https://github.com/math-comp/finmap.git
+cd finmap
+make   # or make -j <number-of-cores-on-your-machine> 
+make install
+```
+
+
+## Documentation
 
 The documentation is available in the header of the file.
 
-## LICENSING
+This library will be integrated to the mathematical components
+library in the near future.
+
+## Related work
+
+This library was developed independently but inspired from
+[Pierre-Yves Strub's
+library](https://github.com/strub/ssrmisc/blob/master/fset.v), from
+[Christian Doczkal's
+library](https://www.ps.uni-saarland.de/formalizations/fset/html/libs.fset.html)
+and from Beta Ziliani's work (no reference provided so far).
+
+Another alternative is [Arthur Azevedo de Amorim extensional
+structures library](https://github.com/arthuraa/extructures).
 
-This program is free software; you can redistribute it and/or modify
-it under the terms of the CeCILL B FREE SOFTWARE LICENSE.
+## Acknowledgments
 
-You should have received a copy of the CeCILL B License with this
-Kit, in the file named "CeCILL-B".
-If not, visit http://www.cecill.info    
+Many thanks to Kazuhiko Sakaguchi (for the order library now moved to
+the main math-comp repository) and to [various
+contributors](https://github.com/math-comp/finmap/graphs/contributors)

_CoqProject

@@ -3,3 +3,11 @@ multiset.v
 set.v
 
 -R . mathcomp.finmap
+-arg -w -arg -projection-no-head-constant
+-arg -w -arg -redundant-canonical-projection
+-arg -w -arg -notation-overridden
+-arg -w -arg +duplicate-clear
+-arg -w -arg +non-primitive-record
+-arg -w -arg +undeclared-scope
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -uniform-inheritance

config.nix

@@ -0,0 +1,4 @@
+{
+  coq = "8.10";
+  mathcomp = "1.11.0";
+}

opam → coq-mathcomp-finmap.opam

@@ -1,28 +1,35 @@
 opam-version: "2.0"
-name: "coq-mathcomp-finmap"
-version: "dev"
 maintainer: "Cyril Cohen <[email protected]>"
+version: "dev"
 
 homepage: "https://github.com/math-comp/finmap"
-bug-reports: "https://github.com/math-comp/finmap/issues"
 dev-repo: "git+https://github.com/math-comp/finmap.git"
-license: "CeCILL-B"
-
-build: [ make "-j" "%{jobs}%" ]
-install: [ make "install" ]
+bug-reports: "https://github.com/math-comp/finmap/issues"
+license: "CECILL-B"
 
-depends: [
-  "coq" { (>= "8.7" & < "8.13~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.11.0" & < "1.12~") | (= "dev") }
-  "coq-mathcomp-bigenough" { (>= "1.0.0" & < "1.1~")  | (= "dev") }
-]
-tags: [ "keyword:finmap" "keyword:finset" "keyword:multiset" "keyword:order"]
-authors: [ "Cyril Cohen <[email protected]>" "Kazuhiko Sakaguchi <[email protected]>" ]
-synopsis: "Finite sets, finite maps, finitely supported functions, orders"
+synopsis: "Finite sets, finite maps, finitely supported functions"
 description: """
 This library is an extension of mathematical component in order to
 support finite sets and finite maps on choicetypes (rather that finite
 types). This includes support for functions with finite support and
 multisets. The library also contains a generic order and set libary,
-which will be used to subsume notations for finite sets, eventually.
-"""
+which will be used to subsume notations for finite sets, eventually."""
+
+build: [make "-j%{jobs}%" ]
+install: [make "install"]
+depends: [
+  "coq" { (>= "8.10" & < "8.13~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "1.11.0" & < "1.13~") | (= "dev") }
+  "coq-mathcomp-bigenough" {>= "1.0.0"}
+]
+
+tags: [
+  "keyword:finmap"
+  "keyword:finset"
+  "keyword:multiset"
+  "logpath:mathcomp.finmap"
+]
+authors: [
+  "Cyril Cohen"
+  "Kazuhiko Sakaguchi"
+]