add meta.yml and generate boilerplate from templates

.github/workflows/check-links.yml

@@ -0,0 +1,19 @@
+name: Check links
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  check-links:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Set up Git repository
+        uses: actions/checkout@v4
+
+      - name: Check for broken Markdown links
+        uses: gaurav-nelson/github-action-markdown-link-check@v1

.github/workflows/docker-action.yml

@@ -0,0 +1,34 @@
+# 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:
+  schedule:
+    - cron: '0 8 * * TUE'
+  push:
+    branches:
+      - main
+  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'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v4
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-tricks.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

Makefile

@@ -7,7 +7,7 @@ COQ_ARGS :=
 all: $(VO_FILES)
 
 src/%.vo: src/%.v
-	coqc -q -Q . Tricks $(COQ_ARGS) $< -o $@
+	coqc -q -Q src Tricks $(COQ_ARGS) $< -o $@
 
 # these rules set COQ_ARGS where needed
 src/NoInit.vo: COQ_ARGS = -noinit

README.md

@@ -1,22 +1,51 @@
 # Tricks in Coq
 
-[![CI](https://github.com/tchajed/coq-tricks/workflows/CI/badge.svg)](https://github.cm/tchajed/coq-tricks/actions?query=workflow%3ACI)
+[![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]
+
+[docker-action-shield]: https://github.com/coq-community/coq-tricks/actions/workflows/docker-action.yml/badge.svg?branch=main
+[docker-action-link]: https://github.com/coq-community/coq-tricks/actions/workflows/docker-action.yml
+
+[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
 
 Some tips, tricks, and features in Coq that are hard to discover.
 
 If you have a trick you've found useful feel free to submit an issue or pull request!
 
-The code in the repository is licensed under the terms of the MIT license. The
-documentation (including this README) is licensed under the [CC0
-license](https://creativecommons.org/publicdomain/zero/1.0/).
+## Meta
+
+- Author(s):
+  - Tej Chajed (initial)
+- Coq-community maintainer(s):
+  - Tej Chajed ([**@tchajed**](https://github.com/tchajed))
+- License: The code in the repository is licensed under the terms of the [MIT license](LICENSE). The documentation (including this README) is licensed under the [CC0 license](LICENSE-docs).
+- Compatible Coq versions: Coq master
+- Coq namespace: `Tricks`
+
+## Building instructions
+
+``` shell
+git clone https://github.com/coq-community/coq-tricks
+cd coq-tricks
+make   # or make -j <number-of-cores-on-your-machine>
+```
 
 ## Ltac
 
 - The `pattern` tactic generalizes an expression over a variable. For example, `pattern y` transforms a goal of `P x y z` into `(fun y => P x y z) y`. An especially useful way to use this is to pattern match on `eval pattern y in constr:(P x y z)` to extract just the function.
 - `lazymatch` is like `match` but without backtracking on failures inside the match action. If you're not using failures for backtracking (this is often the case), then `lazymatch` gets better error messages because an error inside the action becomes the overall error message rather than the uninformative "no match" error message. (The semantics of `match` mean Coq can't do obviously do better - it can't distinguish between a bug in the action and intentionally using the failure to prevent pattern matching.)
 - `deex` (see [Deex.v](src/Deex.v)) is a useful tactic for extracting the witness from an `exists` hypothesis while preserving the name of the witness and hypothesis.
 - `Ltac t ::= foo.` re-defines the tactic `t` to `foo`. This changes the _binding_, so tactics that refer to `t` will use the new definition. You can use this for a form of extensibility: write `Ltac hook := fail` and then use
-  ```
+  ```coq
   repeat match goal with
          | (* initial cases *)
          | _ => hook
@@ -54,7 +83,7 @@ license](https://creativecommons.org/publicdomain/zero/1.0/).
     These forms would be especially useful if occurrence clauses were first-class objects; that is, if tactics could take and pass occurrence clauses. Currently user-defined tactics support occurrence clauses via a set of tactic notations.
 - Defining tactics (`Tactic Notation`s) that accept multiple optional parameters directly is cumbersome, but it can be done more flexibly using Ltac2. An example can be found in [TacticNotationOptionalParams.v](src/TacticNotationOptionalParams.v).
 - You can use notations to shorten repetitive Ltac patterns (much like Haskell's [PatternSynonyms](https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms#Motivatingexample)). Define a notation with holes (underscores) and use it in an Ltac match, eg `Notation anyplus := (_ + _).` and then
-  ```
+  ```coq
   match goal with
   | |- context[anyplus] => idtac
   end

_CoqProject

@@ -1 +1 @@
--R . Top
+-Q src Tricks

coq-tricks.opam

@@ -0,0 +1,29 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+version: "dev"
+
+homepage: "https://github.com/coq-community/coq-tricks"
+dev-repo: "git+https://github.com/coq-community/coq-tricks.git"
+bug-reports: "https://github.com/coq-community/coq-tricks/issues"
+license: "MIT"
+
+synopsis: "Tips, tricks, and features in Coq that are hard to discover"
+description: """
+Some tips, tricks, and features in Coq that are hard to discover.
+
+If you have a trick you've found useful feel free to submit an issue or pull request!"""
+
+build: [make "-j%{jobs}%"]
+depends: [
+  "coq" {= "dev"}
+]
+
+tags: [
+  "category:Miscellaneous/Coq Use Examples"
+  "keyword:tricks"
+  "keyword:tips"
+  "logpath:Tricks"
+]
+authors: [
+  "Tej Chajed"
+]

meta.yml

@@ -0,0 +1,61 @@
+---
+fullname: Tricks in Coq
+shortname: coq-tricks
+organization: coq-community
+community: true
+action: true
+opam_name: coq-tricks
+branch: main
+
+synopsis: >-
+  Tips, tricks, and features in Coq that are hard to discover
+
+description: |-
+  Some tips, tricks, and features in Coq that are hard to discover.
+
+  If you have a trick you've found useful feel free to submit an issue or pull request!
+
+authors:
+- name: Tej Chajed
+  initial: true
+
+maintainers:
+- name: Tej Chajed
+  nickname: tchajed
+
+opam-file-maintainer: [email protected]
+
+opam-file-version: dev
+
+license:
+  fullname: The code in the repository is licensed under the terms of the MIT license. The documentation (including this README) is licensed under the CC0 license.
+  identifier: MIT
+
+supported_coq_versions:
+  text: Coq master
+  opam: '{= "dev"}'
+
+tested_coq_opam_versions:
+- version: 'dev'
+
+# Tuesday 8am UTC (3am EST)
+ci_cron_schedule: '0 8 * * TUE'
+
+namespace: Tricks
+
+build: |-
+ ## Building instructions
+
+ ``` shell
+ git clone https://github.com/coq-community/coq-tricks
+ cd coq-tricks
+ make   # or make -j <number-of-cores-on-your-machine>
+ ```
+
+keywords:
+- name: tricks
+- name: tips
+
+categories:
+- name: Miscellaneous/Coq Use Examples
+---