diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 36766a2..8273628 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -26,7 +26,7 @@ jobs: - uses: actions/checkout@v2 - uses: coq-community/docker-coq-action@v1 with: - opam_file: 'coq-mczify.opam' + opam_file: 'coq-mathcomp-zify.opam' custom_image: ${{ matrix.image }} # See also: diff --git a/README.md b/README.md index 6cd4600..f16b73f 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,50 @@ -# mczify + +# Mczify + +[![Docker CI][docker-action-shield]][docker-action-link] + +[docker-action-shield]: https://github.com/math-comp/mczify/workflows/Docker%20CI/badge.svg?branch=master +[docker-action-link]: https://github.com/math-comp/mczify/actions?query=workflow:"Docker%20CI" + + + + +This small library enables the use of the Micromega tactics for goals stated +with the definitions of the Mathematical Components library by extending the +zify tactic. + +## Meta + +- Author(s): + - Kazuhiko Sakaguchi (initial) +- License: [CeCILL-B Free Software License Agreement](CeCILL-B) +- Compatible Coq versions: 8.13 or later +- Additional dependencies: + - [MathComp](https://math-comp.github.io) 1.12.0 or later +- Coq namespace: `mathcomp.zify` +- Related publication(s): none + +## Building and installation instructions + +The easiest way to install the latest released version of Mczify +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-mathcomp-zify +``` + +To instead build and install manually, do: + +``` shell +git clone https://github.com/math-comp/mczify.git +cd mczify +make # or make -j +make install +``` + -## Requirements -- Coq 8.13 or later, and -- Mathematical Components 1.12.0 or later. diff --git a/coq-mczify.opam b/coq-mathcomp-zify.opam similarity index 100% rename from coq-mczify.opam rename to coq-mathcomp-zify.opam diff --git a/meta.yml b/meta.yml index 52f7e11..8c737d5 100644 --- a/meta.yml +++ b/meta.yml @@ -1,6 +1,7 @@ --- -fullname: mczify +fullname: Mczify shortname: mczify +opam_name: coq-mathcomp-zify organization: math-comp action: true