Merge branch 'master' into master

.circleci/config.yml

@@ -0,0 +1,79 @@
+version: 2.1
+
+jobs:
+ build:
+ parameters:
+ coq:
+ type: string
+ docker:
+ - image: <<parameters.coq>>
+ resource_class: medium
+ environment:
+ OPAMJOBS: 2
+ OPAMVERBOSE: 1
+ OPAMYES: true
+ TERM: xterm
+ steps:
+ - checkout
+ - run:
+ name: Pull submodules
+ command: git submodule update --init --recursive
+ - run:
+ name: Configure environment
+ command: echo . ~/.profile >> $BASH_ENV
+ - run:
+ name: Install dependencies
+ command: |
+ opam repo -a --set-default add coq-extra-dev https://coq.inria.fr/opam/extra-dev
+ opam update
+ opam install --deps-only .
+ - run:
+ name: List installed packages
+ command: opam list
+ - run:
+ name: Build, test, and install package
+ command: opam install -t .
+ - run:
+ name: Generate Coqdoc
+ command: |
+ make -j`nproc` html
+ tar cfz coqdoc.tgz html
+ - store_artifacts:
+ path: coqdoc.tgz
+ - run:
+ name: Test dependants
+ command: |
+ PINS=$(opam list -s --pinned --columns=package | xargs | tr ' ' ,)
+ PACKAGES=`opam list -s --depends-on coq-ext-lib --coinstallable-with $PINS`
+ if [ -n "$PACKAGES" ]
+ then opam install -t $PACKAGES
+ fi
+ - run:
+ name: Uninstall package
+ command: opam uninstall .
+
+workflows:
+ version: 2
+ test:
+ jobs:
+ - build:
+ name: "Coq 8.8"
+ coq: "coqorg/coq:8.8"
+ - build:
+ name: "Coq 8.9"
+ coq: "coqorg/coq:8.9"
+ - build:
+ name: "Coq 8.10"
+ coq: "coqorg/coq:8.10"
+ - build:
+ name: "Coq 8.11"
+ coq: "coqorg/coq:8.11"
+ - build:
+ name: "Coq 8.12"
+ coq: "coqorg/coq:8.12"
+ - build:
+ name: "Coq 8.13"
+ coq: "coqorg/coq:8.13"
+ - build:
+ name: "Coq dev"
+ coq: "coqorg/coq:dev"

.gitignore

@@ -7,11 +7,19 @@
 *.native
 *.o
 *.aux
-Makefile.coq
+Makefile.coq*
 Makefile.opam.coq
 *~
 \#*
 .#*
 .dir-locals.el
 deps.dot
-deps.pdf
+deps.pdf
+.coqdeps.d
+.DS_Store
+html
+index.md
+*.coq.d
+*.vok
+*.vos
+.lia.cache

.gitmodules

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

Makefile

@@ -1,27 +1,37 @@
 all: theories examples
 
-theories: Makefile.coq
- $(MAKE) -f Makefile.coq
+-include coqdocjs/Makefile.doc
+COQMAKEFILE?=Makefile.coq
 
-Makefile.coq:
- $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
+theories: $(COQMAKEFILE)
+ $(MAKE) -f $(COQMAKEFILE)
 
-install: Makefile.coq
- $(MAKE) -f Makefile.coq install
+$(COQMAKEFILE):
+ $(COQBIN)coq_makefile -f _CoqProject -o $(COQMAKEFILE)
+
+install: $(COQMAKEFILE)
+ $(MAKE) -f $(COQMAKEFILE) install
 
 examples: theories
  $(MAKE) -C examples
 
 clean:
- $(MAKE) -f Makefile.coq clean
+ if [ -e $(COQMAKEFILE) ] ; then $(MAKE) -f $(COQMAKEFILE) cleanall ; fi
  $(MAKE) -C examples clean
- @ rm Makefile.coq
+ @rm -f $(COQMAKEFILE) $(COQMAKEFILE).conf
 
 uninstall:
- $(MAKE) -f Makefile.coq uninstall
-
+ $(MAKE) -f $(COQMAKEFILE) uninstall
 
 dist:
  @ git archive --prefix coq-ext-lib/ HEAD -o $(PROJECT_NAME).tgz
 
-.PHONY: all clean dist theories examples
+.PHONY: all clean dist theories examples html
+
+TEMPLATES ?= ../templates
+
+index.html: index.md
+ pandoc -s $^ -o $@
+
+index.md: meta.yml
+ $(TEMPLATES)/generate.sh $@

README.md

@@ -1,8 +1,59 @@
-coq-ext-lib
-===========
+# coq-ext-lib
+
+[![CircleCI][circleci-shield]][circleci-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
+
+[contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
+[contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
+
+[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
+
+[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
+
+
 
 A collection of theories and plugins that may be useful in other Coq developments.
 
+## Meta
+
+- Author(s):
+ - Gregory Malecha (initial)
+- 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
+- Additional dependencies: none
+- Coq namespace: `ExtLib`
+- Related publication(s): none
+
+## Building and installation instructions
+
+The easiest way to install the latest released version of coq-ext-lib
+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-ext-lib
+```
+
+To instead build and install manually, do:
+
+``` shell
+git clone 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
+```
+
+
 Ideas
 -----
 - Embrace new features, e.g. universe polymorphism, primitive projections, etc.
@@ -23,12 +74,3 @@ File Structure
 * theories/
  - Base directory to the provided theories
 
-Install from OPAM
------------------
-Make sure you added the [Coq repository](coq.io/opam/):
-
- opam repo add coq-released https://coq.inria.fr/opam/released
-
-and run:
-
- opam install coq-ext-lib

_CoqProject

@@ -7,17 +7,17 @@ theories/Core/Any.v
 theories/Core/CmpDec.v
 theories/Core/EquivDec.v
 theories/Core/RelDec.v
-theories/Core/Type.v
+theories/Core/Decision.v
 
 theories/Structures/Applicative.v
 theories/Structures/BinOps.v
 theories/Structures/CoFunctor.v
 theories/Structures/CoMonad.v
+theories/Structures/CoMonadLaws.v
 theories/Structures/EqDep.v
 theories/Structures/Foldable.v
 theories/Structures/FunctorLaws.v
 theories/Structures/Functor.v
-theories/Structures/Identity.v
 theories/Structures/IXMonad.v
 theories/Structures/Maps.v
 theories/Structures/MonadCont.v
@@ -33,7 +33,6 @@ theories/Structures/Monad.v
 theories/Structures/MonadWriter.v
 theories/Structures/MonadZero.v
 theories/Structures/Monoid.v
-theories/Structures/Proper.v
 theories/Structures/Reducible.v
 theories/Structures/Sets.v
 theories/Structures/Traversable.v
@@ -104,7 +103,7 @@ theories/Tactics/Injection.v
 theories/Tactics/MonadTac.v
 theories/Tactics/Parametric.v
 theories/Tactics/Reify.v
-theories/Tactics/TypeTac.v
+theories/Tactics/Hide.v
 
 theories/Data/Graph/BuildGraph.v
 theories/Data/Graph/GraphAdjList.v

coq-ext-lib.opam

@@ -0,0 +1,29 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+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"}
+]
+synopsis: "A library of Coq definitions, theorems, and tactics"
+description: """
+A collection of theories and plugins that may be useful in other Coq developments."""
+tags: [
+ "logpath:ExtLib"
+]
+url {
+ src: "git+https://github.com/coq-community/coq-ext-lib"
+}

examples/ConsiderDemo.v

@@ -1,7 +1,7 @@
+Require Import Coq.Bool.Bool.
 Require NPeano.
 Import NPeano.Nat.
 Require Import ExtLib.Tactics.Consider.
-Require Import Coq.Bool.Bool.
 Require Import ExtLib.Data.Nat.
 
 Require Import Coq.ZArith.ZArith.

examples/Makefile

@@ -1,9 +1,9 @@
 coq: Makefile.coq
  $(MAKE) -f Makefile.coq
 
-clean: Makefile.coq
- $(MAKE) -f Makefile.coq clean
- rm Makefile.coq
+clean:
+ if [ -e Makefile.coq ] ; then $(MAKE) -f Makefile.coq cleanall ; fi
+ rm -f Makefile.coq Makefile.coq.conf
 
 Makefile.coq: Makefile _CoqProject
  $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq

examples/MonadReasoning.v

@@ -1,4 +1,3 @@
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Structures.Monad.
 Require Import ExtLib.Structures.MonadLaws.
 Require Import ExtLib.Data.PreFun.
@@ -57,4 +56,4 @@ Section with_m.
  Qed.
 
 End with_m.
-*)
+*)

examples/Notations.v

@@ -0,0 +1,30 @@
+Require Import ExtLib.Structures.Monad.
+Generalizable All Variables.
+
+Module NotationExample.
+
+ Import MonadNotation.
+ Open Scope monad_scope.
+
+ Fixpoint repeatM `{Monad M} (n : nat) `(x : A) (p : A -> M A) : M unit :=
+ match n with
+ | O => ret tt
+ | S n => y <- p x;;
+ repeatM n y p
+ end.
+
+End NotationExample.
+
+Module LetNotationExample.
+
+ Import MonadLetNotation.
+ Open Scope monad_scope.
+
+ Fixpoint repeatM `{Monad M} (n : nat) `(x : A) (p : A -> M A) : M unit :=
+ match n with
+ | O => ret tt
+ | S n => let* y := p x in
+ repeatM n y p
+ end.
+
+End LetNotationExample.

examples/StateGame.v

@@ -13,7 +13,7 @@
  = (Bool, Int)
  *)
 
-Require Import Coq.ZArith.ZArith_base Coq.Strings.String.
+Require Import Coq.ZArith.ZArith_base Coq.Strings.String Coq.Strings.Ascii.
 Require Import ExtLib.Data.Monads.StateMonad ExtLib.Structures.Monads.
 
 Section StateGame.

examples/_CoqProject

@@ -7,3 +7,4 @@ MonadReasoning.v
 Printing.v
 UsingSets.v
 WithDemo.v
+Notations.v