diff --git a/.github/workflows/ci.yml b/.github/workflows/docker-action.yml similarity index 67% rename from .github/workflows/ci.yml rename to .github/workflows/docker-action.yml index 0f553b1..1d4f449 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/docker-action.yml @@ -15,7 +15,8 @@ jobs: strategy: matrix: image: - - 'coqorg/coq:8.17' + - 'coqorg/coq:dev-ocaml-4.14-flambda' + - 'coqorg/coq:8.17-ocaml-4.09-flambda' fail-fast: false steps: - uses: actions/checkout@v3 @@ -23,7 +24,7 @@ jobs: with: opam_file: 'coq-my-plugin.opam' custom_image: ${{ matrix.image }} - before_install: | - startGroup "Print opam config and unpin dune" - opam config list; opam repo list; opam list; opam pin remove dune -y - endGroup + +# See also: +# https://github.com/coq-community/docker-coq-action#readme +# https://github.com/erikmd/docker-coq-github-action-demo diff --git a/CHANGES b/CHANGES deleted file mode 100644 index 4ee5d00..0000000 --- a/CHANGES +++ /dev/null @@ -1,4 +0,0 @@ -0.0.1 ------ - - * Initial version (Emilio J. Gallego Arias) diff --git a/README.md b/README.md index 5c9473e..00ac37d 100644 --- a/README.md +++ b/README.md @@ -1,55 +1,60 @@ -# Template for Coq Plugins using Dune +# Coq Plugin Template using Dune -This repository contains a template for writing a plugin for the +[![Docker CI][docker-action-shield]][docker-action-link] + +[docker-action-shield]: https://github.com/coq-community/coq-plugin-template/workflows/Docker%20CI/badge.svg?branch=v8.17 +[docker-action-link]: https://github.com/coq-community/coq-plugin-template/actions?query=workflow:"Docker%20CI" + +Template repository writing a plugin in [OCaml](https://ocaml.org) for the [Coq](https://coq.inria.fr) proof assistant using the [Dune](https://dune.build) build system. It showcases a few advanced features such as linking to C code or to external libraries. -The current version is tested (and requires): - -- Dune 2.9 -- Coq 8.16 - -Minimal historical requirements are Coq 8.9 and Dune 1.10, but they -are not supported anymore. See template history / branches for -changes at your own risk. +## Meta -See the [Dune documentation](https://dune.readthedocs.io/en/latest/) for more help. +- License: [Unlicense](LICENSE) (change to your license of choice) +- Compatible Coq versions: 8.17 or later +- Additional dependencies: + - [Dune](https://dune.build) 3.8.1 or later +- Coq namespace: `MyPlugin` -## See also - -The [official tutorial](https://github.com/coq/coq/tree/master/doc/plugin_tutorial) -for writing Coq plugins in the Coq repository, which already includes `dune` files -for OCaml parts. - -## How to build +## Building instructions +To install dependencies via [opam](https://opam.ocaml.org/doc/Install.html): ```shell -$ dune build +$ opam install dune.3.8.2 coq.8.17.0 ``` -and the rest of the regular Dune commands. To test your library, you can use +To build the plugin when all dependencies are installed: ```shell -$ dune exec -- coqtop -R _build/default/theories MyPlugin +$ dune build ``` -or starting with Dune 3.2 +The plugin can be tested manually: ```shell $ dune coq top theories/Test.v -``` -## Releasing OPAM packages +Welcome to Coq 8.17.0 -You can use -[`dune-release`](https://github.com/ocamllabs/dune-release) to -automatically release OPAM packages. +Coq < Require Import MyPlugin. +[Loading ML file my_plugin.cmxs (using legacy method) ... done] -For that, you need to update the included `.opam` file, and configure -your Github tokens as described in the documentation of `dune-release`. +Coq < CallC. +Toplevel input, characters 0-6: +> CallC. +> ^^^^^^ +Warning: 546 +``` -## Linking with external libraries +See also the [Dune documentation](https://dune.readthedocs.io/en/latest/) for more help, +and the [official tutorial](https://github.com/coq/coq/tree/master/doc/plugin_tutorial) +for writing Coq plugins in the Coq repository which already includes `dune` files +for the OCaml parts. -Starting with Coq 8.16, Coq will load dependencies of your -plugin. This requires that your plugin is named as a findlib package. +## Releasing opam packages -See [Coq documentation](https://coq.github.io/doc/master/refman/proof-engine/vernacular-commands.html#coq:cmd.Declare-ML-Module) for more information. +You can use [`dune-release`](https://github.com/tarides/dune-release) to +automatically release opam packages. + +For that, you need to update the included `.opam` file, and configure +your Github tokens as described in the documentation of `dune-release`. diff --git a/coq-my-plugin.opam b/coq-my-plugin.opam index 7e42a6a..efd3658 100644 --- a/coq-my-plugin.opam +++ b/coq-my-plugin.opam @@ -1,10 +1,11 @@ opam-version: "2.0" maintainer: "you@example.com" +version: "dev" -homepage: "https://github.com/your-github/my-plugin" -dev-repo: "git+https://github.com/your-github/my-plugin.git" -bug-reports: "https://github.com/your-github/my-plugin/issues" -doc: "https://your-github.github.io/my-plugin" +homepage: "https://github.com/coq-community/my-plugin" +dev-repo: "git+https://github.com/coq-community/my-plugin.git" +bug-reports: "https://github.com/coq-community/my-plugin/issues" +doc: "https://coq-community.github.io/my-plugin" license: "SPDX-identifier-for-your-license" synopsis: "One line description of your plugin" @@ -16,7 +17,7 @@ build: ["dune" "build" "-p" name "-j" jobs] depends: [ "ocaml" {>= "4.09.0"} "dune" {>= "3.8.2"} - "coq" {>= "8.17"} + "coq" {>= "8.17.1"} ] tags: [