Merge branch 'master' into master

.github/workflows/docker-action.yml

@@ -0,0 +1,76 @@
+# 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:8.9'
+          - 'coqorg/coq:8.11'
+          - 'coqorg/coq:8.12'
+          - 'coqorg/coq:8.13'
+          - 'coqorg/coq:8.14'
+          - 'coqorg/coq:8.15'
+          - 'coqorg/coq:8.16'
+          - 'coqorg/coq:8.17'
+          - 'coqorg/coq:8.18'
+          - 'coqorg/coq:dev'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-ext-lib.opam'
+          custom_image: ${{ matrix.image }}
+          after_script: |
+            startGroup "Test dependants"
+              PINS=$(opam list -s --pinned --columns=package | xargs | tr ' ' ,)
+              PACKAGES=`opam list -s --depends-on coq-ext-lib --coinstallable-with $PINS`
+              for PACKAGE in $PACKAGES
+              do DEPS_FAILED=false
+                 opam install -y --deps-only $PACKAGE || DEPS_FAILED=true
+                 [ $DEPS_FAILED == true ] || opam install -t $PACKAGE
+              done
+            endGroup
+            set -o pipefail  # recommended if the script uses pipes
+
+            startGroup "Generate Coqdoc"
+              make -j`nproc` coqdoc
+            endGroup
+          before_script: |
+            startGroup "Install and configure Clang"
+              opam install conf-clang
+            endGroup
+            startGroup "Workaround permission issue"
+              sudo chown -R coq:coq .
+            endGroup
+          export: 'OPAMWITHTEST OPAMCONFIRMLEVEL'
+        env:
+          OPAMWITHTEST: true
+          OPAMCONFIRMLEVEL: unsafe-yes
+      - name: Revert permissions
+        # to avoid a warning at cleanup time
+        if: ${{ always() }}
+        run: sudo chown -R 1001:116 .
+      - uses: actions/upload-artifact@v3
+        with:
+          name: coqdoc
+          path: html
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo

.github/workflows/stale.yml

@@ -0,0 +1,16 @@
+name: 'Close stale issues and PRs'
+on:
+  schedule:
+    - cron: '30 1 * * 1-5'
+
+permissions:
+  issues: write
+  pull-requests: write
+
+jobs:
+  stale:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/stale@v8
+        with:
+          days-before-close: -1

.gitignore

@@ -19,6 +19,7 @@ deps.pdf
 .DS_Store
 html
 index.md
+index.html
 *.coq.d
 *.vok
 *.vos

.gitmodules

@@ -1,3 +1,6 @@
 [submodule "coqdocjs"]
 	path = coqdocjs
 	url = https://github.com/coq-community/coqdocjs.git
+[submodule "templates"]
+	path = templates
+	url = https://github.com/coq-community/templates.git

LICENSE

@@ -1,3 +1,5 @@
+BSD 2-Clause License
+
 Copyright (c) 2013, Gregory M. Malecha
 All rights reserved.
 
@@ -6,21 +8,18 @@ modification, are permitted provided that the following conditions are met:
 
 1. Redistributions of source code must retain the above copyright notice, this
    list of conditions and the following disclaimer. 
+
 2. Redistributions in binary form must reproduce the above copyright notice,
    this list of conditions and the following disclaimer in the documentation
    and/or other materials provided with the distribution. 
 
 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
 ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
-DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
 ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-
-The views and conclusions contained in the software and documentation are those
-of the authors and should not be interpreted as representing official policies, 
-either expressed or implied, of the FreeBSD Project.

Makefile

@@ -1,5 +1,6 @@
 all: theories examples
 
+COQDOCJS_LN?=true
 -include coqdocjs/Makefile.doc
 COQMAKEFILE?=Makefile.coq
 
@@ -28,10 +29,14 @@ dist:
 
 .PHONY: all clean dist theories examples html
 
-TEMPLATES ?= ../templates
+TEMPLATES ?= templates
 
 index.html: index.md
 	pandoc -s $^ -o $@
 
 index.md: meta.yml
 	$(TEMPLATES)/generate.sh $@
+
+publish%:
+	opam publish --packages-directory=released/packages \
+		--repo=coq/opam-coq-archive --tag=v$* -v $* coq-community/coq-ext-lib

README.md

@@ -1,12 +1,16 @@
+<!---
+This file was generated from `meta.yml`, please do not edit manually.
+Follow the instructions on https://github.com/coq-community/templates to regenerate.
+--->
 # coq-ext-lib
 
-[![CircleCI][circleci-shield]][circleci-link]
+[![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]
 
-[circleci-shield]: https://circleci.com/gh/coq-community/coq-ext-lib.svg?style=svg
-[circleci-link]:   https://circleci.com/gh/coq-community/coq-ext-lib
+[docker-action-shield]: https://github.com/coq-community/coq-ext-lib/workflows/Docker%20CI/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/coq-ext-lib/actions?query=workflow:"Docker%20CI"
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
@@ -28,8 +32,8 @@ A collection of theories and plugins that may be useful in other Coq development
 - Coq-community maintainer(s):
   - Gregory Malecha ([**@gmalecha**](https://github.com/gmalecha))
   - Yishuai Li ([**@liyishuai**](https://github.com/liyishuai))
-- License: [The FreeBSD Copyright](LICENSE)
-- Compatible Coq versions: Coq 8.8 or later
+- License: [BSD 2-Clause "Simplified" License](LICENSE)
+- Compatible Coq versions: Coq 8.11 or later or 8.9
 - Additional dependencies: none
 - Coq namespace: `ExtLib`
 - Related publication(s): none
@@ -47,7 +51,7 @@ opam install coq-ext-lib
 To instead build and install manually, do:
 
 ``` shell
-git clone https://github.com/coq-community/coq-ext-lib.git
+git clone --recurse-submodules https://github.com/coq-community/coq-ext-lib.git
 cd coq-ext-lib
 make theories  # or make -j <number-of-cores-on-your-machine> theories
 make install

_CoqProject

@@ -121,7 +121,6 @@ theories/Data/Monads/FuelMonad.v
 theories/Data/Monads/IdentityMonadLaws.v
 theories/Data/Monads/IdentityMonad.v
 theories/Data/Monads/IStateMonad.v
-theories/Data/Monads/ListMonad.v
 theories/Data/Monads/OptionMonadLaws.v
 theories/Data/Monads/OptionMonad.v
 theories/Data/Monads/ReaderMonadLaws.v

coq-ext-lib.opam

@@ -1,29 +1,29 @@
+# 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: "gmalecha@gmail.com"
+version: "dev"
+
 homepage: "https://github.com/coq-community/coq-ext-lib"
 dev-repo: "git+https://github.com/coq-community/coq-ext-lib.git"
 bug-reports: "https://github.com/coq-community/coq-ext-lib/issues"
-authors: ["Gregory Malecha"]
-license: "BSD"
-build: [
-  [make "-j%{jobs}%" "theories"]
-]
-run-test: [
-  [make "-j%{jobs}%" "examples"]
-]
-install: [
-  [make "install"]
-]
-depends: [
-  "ocaml"
-  "coq" {>= "8.8"}
-]
+license: "BSD-2-Clause"
+
 synopsis: "A library of Coq definitions, theorems, and tactics"
 description: """
 A collection of theories and plugins that may be useful in other Coq developments."""
+
+build: [make "-j%{jobs}%" "theories"]
+run-test: [make "-j%{jobs}%" "examples"]
+install: [make "install"]
+depends: [
+  "coq" { >= "8.9" < "8.10" | >= "8.11" }
+]
+
 tags: [
   "logpath:ExtLib"
 ]
-url {
-  src: "git+https://github.com/coq-community/coq-ext-lib"
-}
+authors: [
+  "Gregory Malecha"
+]

examples/ConsiderDemo.v

@@ -1,30 +1,30 @@
 Require Import Coq.Bool.Bool.
-Require NPeano.
-Import NPeano.Nat.
+Require Import Arith.PeanoNat.
 Require Import ExtLib.Tactics.Consider.
 Require Import ExtLib.Data.Nat.
 
 Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
 
 Set Implicit Arguments.
 Set Strict Implicit.
 
 (**  Some tests *)
 Section test.
-  Goal forall x y z,  (ltb x y && ltb y z) = true ->
-                 ltb x z = true.
+  Goal forall x y z,  (Nat.ltb x y && Nat.ltb y z) = true ->
+                 Nat.ltb x z = true.
   intros x y z.
-  consider (ltb x y && ltb y z).
-  consider (ltb x z); auto. intros. exfalso. omega.
+  consider (Nat.ltb x y && Nat.ltb y z).
+  consider (Nat.ltb x z); auto. intros. exfalso. lia.
   Qed.
 
   Goal forall x y z,
-    ltb x y = true ->
-    ltb y z = true ->
-    ltb x z = true.
+    Nat.ltb x y = true ->
+    Nat.ltb y z = true ->
+    Nat.ltb x z = true.
   Proof.
-    intros. consider (ltb x y); consider (ltb y z); consider (ltb x z); intros; auto.
-    exfalso; omega.
+    intros. consider (Nat.ltb x y); consider (Nat.ltb y z); consider (Nat.ltb x z); intros; auto.
+    exfalso; lia.
   Qed.
 
 End test.

examples/StateTMonad.v

@@ -0,0 +1,15 @@
+From ExtLib Require Import
+     Monad
+     OptionMonad
+     StateMonad.
+
+(** [Monad_stateT] is not in context, so this definition fails *)
+Fail Definition foo : stateT unit option unit :=
+  ret tt.
+
+(** Use [Existing Instance] to bring the Local [Monad_stateT] instance into context *)
+#[global] Existing Instance Monad_stateT.
+
+(** Now the definition succeeds *)
+Definition foo : stateT unit option unit :=
+  ret tt.