diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml deleted file mode 100644 index 7003d63..0000000 --- a/.github/workflows/ci.yml +++ /dev/null @@ -1,48 +0,0 @@ -name: CI - -on: - push: - branches: - - v8.16 - pull_request: - branches: - - v8.16 - - # Allows you to run this workflow manually from the Actions tab - workflow_dispatch: - -jobs: - build: - strategy: - fail-fast: false - matrix: - ocaml-compiler: [4.09.x, 4.14.x] - coq-version: [8.16+rc1] - env: - NJOBS: "2" - OPAMJOBS: "2" - OPAMROOTISOK: "true" - OPAMYES: "true" - runs-on: ubuntu-latest - - steps: - - uses: actions/checkout@v2 - - name: Set up OCaml ${{ matrix.ocaml-compiler }} - uses: avsm/setup-ocaml@v2 - with: - ocaml-compiler: ${{ matrix.ocaml-compiler }} - dune-cache: true - - name: Install Coq - run: | - eval $(opam env) - opam repos add coq-released http://coq.inria.fr/opam/released - opam repos add coq-core-dev http://coq.inria.fr/opam/core-dev - opam install coq.${{ matrix.coq-version }} - - name: Display OPAM Setup - run: | - eval $(opam env) - opam list - - name: Test Template - run: | - eval $(opam env) - dune build --display=short diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml new file mode 100644 index 0000000..208bb4c --- /dev/null +++ b/.github/workflows/docker-action.yml @@ -0,0 +1,30 @@ +name: Docker CI + +on: + push: + branches: + - 'v8.17+0.8' + 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-ocaml-4.14-flambda' + - 'coqorg/coq:8.17.1-ocaml-4.09.1-flambda' + fail-fast: false + steps: + - uses: actions/checkout@v3 + - uses: coq-community/docker-coq-action@v1 + with: + opam_file: 'coq-my-plugin.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/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..e74142c 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.1 or later +- Additional dependencies: + - [Dune](https://dune.build) 3.8.2 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.1 ``` -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.1 -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 6b04d8e..efd3658 100644 --- a/coq-my-plugin.opam +++ b/coq-my-plugin.opam @@ -1,11 +1,12 @@ 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" -license: "MIT" +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" description: """ @@ -14,9 +15,9 @@ cover multiple lines. Including punctuation.""" build: ["dune" "build" "-p" name "-j" jobs] depends: [ - "ocaml" {>= "4.07.1"} - "dune" {>= "2.5"} - "coq" {>= "8.14" & < "8.15"} + "ocaml" {>= "4.09.0"} + "dune" {>= "3.8.2"} + "coq" {>= "8.17.1"} ] tags: [ diff --git a/dune-project b/dune-project index 84084aa..d90a7fd 100644 --- a/dune-project +++ b/dune-project @@ -1,3 +1,3 @@ -(lang dune 2.9) -(using coq 0.3) +(lang dune 3.8) +(using coq 0.8) (name my-plugin) diff --git a/src/dune b/src/dune index 83500fa..a5e89e6 100644 --- a/src/dune +++ b/src/dune @@ -10,18 +10,14 @@ (synopsis "My Coq plugin") ; Synopsis, used in META generation. - (flags :standard -rectypes -w -27) ; Coq requires the `-rectypes` - ; flag; CoqPP generated code - ; requires to disable warning 27 - ; often. + (flags :standard -w -27) ; CoqPP generated code requires to + ; disable warning 27 often. - (foreign_stubs ; we link our plugin with a C + (foreign_stubs ; We link our plugin with a C (language c) ; library! Optional, of course. (names ce_get)) - (libraries ; OCaml Libraries we want to link - ; with, your choice here. - + (libraries ; OCaml libraries we want to link with coq-core.vernac ; Needed for vernac extend. coq-core.plugins.ltac ; Needed for tactic extend. ) diff --git a/theories/dune b/theories/dune index f4cf1d6..3d37af5 100644 --- a/theories/dune +++ b/theories/dune @@ -7,7 +7,7 @@ (package coq-my-plugin) ; Adding this line will make your ; library installable in the opam package - (libraries coq-my-plugin.plugin)) ; Here you should declare all + (plugins coq-my-plugin.plugin)) ; Here you should declare all ; OCaml plugin dependencies ; for your Coq files.