Update for Dune-Coq 0.8 and Coq 8.17

.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

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`.

coq-my-plugin.opam

@@ -1,11 +1,12 @@
 opam-version: "2.0"
 maintainer: "[email protected]"
+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: [

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)

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.
  )

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.