add meta.yml and generate README and CI configuration from templates

.github/workflows/docker-action.yml

@@ -0,0 +1,39 @@
+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.13'
+          - 'coqorg/coq:8.12'
+          - 'coqorg/coq:8.11'
+          - 'coqorg/coq:8.10'
+          - 'coqorg/coq:8.9'
+          - 'coqorg/coq:8.8'
+          - 'coqorg/coq:8.7'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v2
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-dblib.opam'
+          custom_image: ${{ matrix.image }}
+          export: 'OPAMWITHTEST'
+        env:
+          OPAMWITHTEST: 'true'
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo

Makefile

@@ -1,18 +1,20 @@
 all: Makefile.coq
-	$(MAKE) -f Makefile.coq all
+	@+$(MAKE) -f Makefile.coq all
 
 tests:
-	$(MAKE) -C tests
+	@+$(MAKE) -C tests
 
 clean: Makefile.coq
-	$(MAKE) -f Makefile.coq clean
-	$(MAKE) -C tests clean
-	rm -f Makefile.coq
+	@+$(MAKE) -f Makefile.coq cleanall
+	@+$(MAKE) -C tests clean
+	@rm -f Makefile.coq Makefile.coq.conf
 
 Makefile.coq: _CoqProject
 	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
-%: Makefile.coq
-	$(MAKE) -f Makefile.coq $@
+force _CoqProject Makefile: ;
 
-.PHONY: all clean tests
+%: Makefile.coq force
+	@+$(MAKE) -f Makefile.coq $@
+
+.PHONY: all clean force tests

README.md

@@ -1,51 +1,98 @@
-[![CI](https://github.com/coq-community/dblib/workflows/CI/badge.svg)](https://github.com/coq-community/dblib/actions?query=workflow%3ACI)
-
+<!---
+This file was generated from `meta.yml`, please do not edit manually.
+Follow the instructions on https://github.com/coq-community/templates to regenerate.
+--->
 # Dblib
 
-- **Author**: François Pottier, INRIA. 2013.
-- **License**: GNU GPLv3. See [LICENSE](LICENSE).
-- **Requirements**: Coq 8.7+ (tested on 8.7~8.12 and dev)
+[![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]
 
-## What is Dblib?
+[docker-action-shield]: https://github.com/coq-community/dblib/workflows/Docker%20CI/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/dblib/actions?query=workflow:"Docker%20CI"
 
-The dblib library offers facilities for working with de Bruijn indices in
-Coq. The basic idea is as follows:
+[contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
+[contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
 
-1. The client manually defines the syntax of terms (or types, or whatever
-   syntax she is interested in) as usual, as an inductive type;
+[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
 
-2. The client manually defines a higher-order "traverse" function, which can
-   be thought of as a generic, capture-avoiding substitution function. Its
-   job is (i) to apply a user-supplied function f at every variable, and
-   (ii) to inform f about the number of binders that have been entered. By
-   defining "traverse", the client effectively defines the binding structure.
+[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
+
+
+
+Library with facilities for working with de Bruijn indices in Coq to
+reason about capture-avoiding substitution of variables in syntax with binders.
+
+## Meta
+
+- Author(s):
+  - François Pottier (initial)
+- Coq-community maintainer(s):
+  - Kevin Orr ([**@KevOrr**](https://github.com/KevOrr))
+- License: [GNU General Public License v3.0](LICENSE)
+- Compatible Coq versions: 8.7 or later
+- Additional dependencies: none
+- Coq namespace: `Dblib`
+- Related publication(s): none
+
+## Building and installation instructions
+
+The easiest way to install the latest released version of Dblib
+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-dblib
+```
+
+To instead build and install manually, do:
 
-3. The client proves that the "traverse" function is well-behaved, i.e., it
-   satisfies half a dozen reasonable properties. This proof is usually
+``` shell
+git clone https://github.com/coq-community/dblib.git
+cd dblib
+make   # or make -j <number-of-cores-on-your-machine> 
+make install
+```
+
+
+## Documentation
+
+### Workflow
+
+The basic workflow for using the library is as follows:
+
+1. The client manually defines the syntax of terms (or types, or whatever
+   syntax she is interested in) as usual, as an inductive type.
+2. The client manually defines a higher-order `traverse` function, which can
+   be thought of as a generic, capture-avoiding substitution function. Its
+   job is (i) to apply a user-supplied function `f` at every variable, and
+   (ii) to inform `f` about the number of binders that have been entered. By
+   defining `traverse`, the client effectively defines the binding structure.
+3. The client proves that the `traverse` function is well-behaved, i.e., it
+   satisfies half a dozen reasonable properties. These proofs are usually
    trivial, because the library provides tailor-made tactics for this
    purpose.
-
-4. The library defines weakening ("lift") and substitution ("subst") in
-   terms of "traverse", and proves a rather large number of properties of
+4. The library defines weakening (`lift`) and substitution (`subst`) in
+   terms of `traverse`, and proves a rather large number of properties of
    these functions.
-
-5. The functions "lift" and "subst" are opaque, so an application of these
-   functions cannot be reduced by Coq's builtin tactic "simpl". The library
-   provides "simpl_lift_goal" and "simpl_subst_goal" for this purpose (plus
+5. The functions `lift` and `subst` are opaque, so an application of these
+   functions cannot be reduced by Coq's builtin tactic `simpl`. The library
+   provides `simpl_lift_goal` and `simpl_subst_goal` for this purpose (plus
    a few variants of these tactics that perform simplification within a
    hypothesis, or within all hypotheses).
-
-6. The library also provides hint databases, to be used with [eauto], that
+6. The library also provides hint databases, to be used with `eauto`, that
    can prove many of the typical equalities that arise when proving
    weakening or substitution lemmas.
-
-7. The library defines a "closed" term as one that is invariant under
+7. The library defines a `closed` term as one that is invariant under
    lifting (and substitution), and provides lemmas/tactics for reasoning
    about this notion.
 
 Everything is based on type classes: `traverse`, `lift`, `subst`, etc. are
 overloaded, so the whole process can be repeated, if desired, for another
-inductive type
+inductive type.
 
 The library *does* support multiple *independent* namespaces: for instance, it
 is possible to have terms that contain term variables and types that contain
@@ -56,10 +103,11 @@ between them: for instance, it is *not* possible to have terms that contain
 both term variables and type variables, as in a standard presentation of
 System F. A possible work-around is to define a single namespace of
 "variables" and to use a separate well-kindedness judgement in order to
-distinguish between "term" variables and "type" variables. I have used this
-approach in a large proof where it has turned out to be extremely beneficial.
+distinguish between "term" variables and "type" variables. This
+approach has been used in a large proof, where it has turned out
+to be extremely beneficial.
 
-## Library Files
+### Library Files
 
 The library consists of the following files:
 
@@ -80,7 +128,7 @@ The library consists of the following files:
   is typically useful when defining a typing judgement. The use
   of this library is optional.
 
-## Demos
+### Demos
 
 The documentation takes the form of a few demo files:
 

_CoqProject

@@ -1,5 +1,8 @@
 -Q src Dblib
 
+-arg -w -arg -deprecated-hint-without-locality
+-arg -w -arg -deprecated-instance-without-locality
+
 src/DblibTactics.v
 src/DeBruijn.v
 src/DemoExplicitSystemF.v

coq-dblib.opam

@@ -1,51 +1,32 @@
 opam-version: "2.0"
-maintainer: "Kevin Orr <kevinorr54@gmail.com>"
+maintainer: "palmskog@gmail.com"
 version: "dev"
 
 homepage: "https://github.com/coq-community/dblib"
 dev-repo: "git+https://github.com/coq-community/dblib.git"
 bug-reports: "https://github.com/coq-community/dblib/issues"
 license: "GPL-3.0-only"
-authors: ["François Pottier <francois.pottier@inria.fr> [http://gallium.inria.fr/~fpottier/]"]
 
-synopsis: "De Bruijn indices in Coq"
+synopsis: "Library for de Bruijn indices in Coq"
 description: """
-Dblib offers facilities for working with de Bruijn indices in Coq.
-The basic idea is as follows:
+Library with facilities for working with de Bruijn indices in Coq to
+reason about capture-avoiding substitution of variables in syntax with binders."""
 
-1. Define the abstract syntax of terms as an inductive type
-
-2. Define a higher-order [traverse] function, which can be thought of as a
-   generic, capture-avoiding substitution (CAS) function. By defining
-   [traverse], you effectively define the binding structure of terms
-
-3. Prove that [traverse] is well-behaved, i.e., it satisfies half a dozen
-   reasonable properties. These proofs are usually trivial, because Dblib
-   provides tailor-made tactics for this purpose
-
-4. Dblib defines weakening ([lift]) and substitution ([subst]) in terms of
-   [traverse], and proves a rather large number of properties of these functions
-
-Everything is based on type classes: traverse, lift, subst, etc. are overloaded,
-so the whole process can be repeated, if desired, for another inductive type
+build: [make "-j%{jobs}%" ]
+run-test: [make "tests"]
+install: [make "install"]
+depends: [
+  "coq" {(>= "8.7" & < "8.15~") | (= "dev")}
+]
 
-Dblib does support multiple independent namespaces: for instance, it is possible
-to have terms that contain term variables and types that contain type variables,
-but it is not possible to have terms that contain both term variables and type
-variables. A possible work-around is to define a single namespace of "variables"
-and to use a separate well-kindedness judgement in order to distinguish between
-"term" variables and "type" variables.
-"""
 tags: [
-  "keyword: abstract syntax"
-  "keyword: binders"
-  "keyword: de Bruijn indices"
-  "keyword: substitution"
-  "category: Computer Science/Lambda Calculi"
+  "category:Computer Science/Lambda Calculi"
+  "keyword:abstract syntax"
+  "keyword:binders"
+  "keyword:de Bruijn indices"
+  "keyword:substitution"
+  "logpath:Dblib"
+]
+authors: [
+  "François Pottier"
 ]
-
-build: [make "-j%{jobs}%"]
-run-test: [make "tests"]
-install: [make "install"]
-remove: [make "uninstall"]
-depends: ["coq" {>= "8.7" & < "8.13~" | = "dev"}]