diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml deleted file mode 100644 index 8cf7d0b..0000000 --- a/.github/workflows/build.yml +++ /dev/null @@ -1,44 +0,0 @@ -name: CI - -# Controls when the action will run: -# https://help.github.com/en/actions/configuring-and-managing-workflows/configuring-a-workflow#filtering-for-specific-branches-tags-and-paths -on: - push: - branches: - - main - pull_request: - schedule: - # Tuesday 8am UTC (3am EST) - - cron: "0 8 * * TUE" - -jobs: - build: - runs-on: ubuntu-latest - strategy: - matrix: - coq_version: - - dev - max-parallel: 4 - fail-fast: false - - steps: - - uses: actions/checkout@v4 - - uses: coq-community/docker-coq-action@v1 - with: - coq_version: ${{ matrix.coq_version }} - install: "" - after_install: "" - before_script: | - sudo chown -R coq:coq . # workaround a permission issue - script: | - startGroup Build - make -j2 -k - endGroup - uninstall: | - make clean - - name: Revert permissions - # to avoid a warning at cleanup time - if: ${{ always() }} - run: sudo chown -R 1001:116 . - - name: Check for broken Markdown links - uses: gaurav-nelson/github-action-markdown-link-check@v1 diff --git a/.github/workflows/check-links.yml b/.github/workflows/check-links.yml new file mode 100644 index 0000000..67b87b3 --- /dev/null +++ b/.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 diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml new file mode 100644 index 0000000..ea21ce7 --- /dev/null +++ b/.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 diff --git a/README.md b/README.md index 828f63c..97ab473 100644 --- a/README.md +++ b/README.md @@ -1,14 +1,43 @@ # 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 +``` ## Ltac @@ -16,7 +45,7 @@ license](https://creativecommons.org/publicdomain/zero/1.0/). - `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 diff --git a/_CoqProject b/_CoqProject index e205252..e16b861 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1 +1 @@ --R . Top +-R src Tricks diff --git a/coq-tricks.opam b/coq-tricks.opam new file mode 100644 index 0000000..75970aa --- /dev/null +++ b/coq-tricks.opam @@ -0,0 +1,29 @@ +opam-version: "2.0" +maintainer: "palmskog@gmail.com" +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" +] diff --git a/meta.yml b/meta.yml new file mode 100644 index 0000000..2bd363a --- /dev/null +++ b/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: palmskog@gmail.com + +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 + ``` + +keywords: +- name: tricks +- name: tips + +categories: +- name: Miscellaneous/Coq Use Examples +---