[v8.16] Update to 8.16, add continuous integration

.github/workflows/ci.yml

@@ -0,0 +1,48 @@
+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: [v8.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-version }}
+      - name: Display OPAM Setup
+        run: |
+          eval $(opam env)
+          opam list
+      - name: Test Template
+        run: |
+          eval $(opam env)
+          dune build --display=short

README.md

@@ -5,10 +5,10 @@ This repository contains a template for writing a plugin for the
 build system. It showcases a few advanced features such as linking to C code or
 to external libraries.
 
-The current version is tested with:
+The current version is tested (and requires):
 
-- Dune 2.5
-- Coq 8.14
+- 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
@@ -33,6 +33,11 @@ and the rest of the regular Dune commands. To test your library, you can use
 $ dune exec -- coqtop -R _build/default/theories MyPlugin
 ```
 
+or starting with Dune 3.2
+```shell
+$ dune coq top theories/Test.v
+```
+
 ## Releasing OPAM packages
 
 You can use
@@ -44,43 +49,7 @@ your Github tokens as described in the documentation of `dune-release`.
 
 ## Linking with external libraries
 
-If your plugin depends on an external OCaml library, Coq will fail to
-load it as it doesn't know about this dependency.
-
-This should be fixed in Coq hopefully soon, see [Coq's
-issue](https://github.com/coq/coq/issues/7698).
-
-Meanwhile, you need to manage the dependency chain manually; imagine
-you want to depend on `z3`, then in your `(library ...)` stanza you
-will want to add:
-```lisp
-(libraries coq-core.vernac z3)
-```
-That works, and your plugin will now be able to link to `z3`.
-However, when dynamically loading it, you must ensure that the `z3`
-modules have been linked.
-
-To do so manually, load the `z3` plugin in your `Test.v` file:
-```
-Declare ML Module "z3ml".
-Declare ML Module "example_plugin".
-```
-We are almost there! The last thing you need to do is to workaround a Coq Dune bug and
-add `z3` to the list of dependencies of your Coq theory:
-```lisp
-(libraries z3 coq-my-plugin.plugin)
-```
-and that's all!
-
-A last step to make things work in the concrete case of `z3` is to
-update the `LD_LIBRARY_PATH` as the OPAM package is buggy, usually this will do:
-```
-export LD_LIBRARY_PATH=~/.opam/coq.dev/lib/z3:$LD_LIBRARY_PATH
-```
-
-## Caveats
+Starting with Coq 8.16, Coq will load dependencies of your
+plugin. This requires that your plugin is named as a findlib package.
 
-- Coq's linker cannot track dependencies properly, thus YMMV when
-  linking against 3rd party libraries.
-- `coqdep` emits some warnings that should be hard failures, we
-  recommend you treat them as such.
+See [Coq documentation](https://coq.github.io/doc/master/refman/proof-engine/vernacular-commands.html#coq:cmd.Declare-ML-Module) for more information.

dune-project

@@ -1,3 +1,3 @@
-(lang dune 2.5)
-(using coq 0.2)
+(lang dune 2.9)
+(using coq 0.3)
 (name my-plugin)

src/ce_api.ml

@@ -13,4 +13,4 @@ let msg_in_tactic str : unit PV.tactic =
 let printHello : unit PV.tactic =
   let open PV.Notations in
   msg_in_tactic "hello" >>= fun () ->
-  Tacticals.New.tclIDTAC
+  Tacticals.tclIDTAC

src/ce_syntax.mlg

@@ -1,4 +1,4 @@
-DECLARE PLUGIN "my_plugin"
+DECLARE PLUGIN "coq-my-plugin.plugin"
 
 {
 

theories/MyPlugin.v

@@ -0,0 +1 @@
+Declare ML Module "my_plugin:coq-my-plugin.plugin".

theories/Test.v

@@ -1,4 +1,4 @@
-Declare ML Module "my_plugin".
+Require Import MyPlugin.
 
 CallC.