Skip to content

Commit

Permalink
update README.md, opam package and Docker CI
Browse files Browse the repository at this point in the history
  • Loading branch information
palmskog committed Jul 13, 2023
1 parent 198e877 commit c8d8385
Show file tree
Hide file tree
Showing 4 changed files with 50 additions and 47 deletions.
11 changes: 6 additions & 5 deletions .github/workflows/ci.yml → .github/workflows/docker-action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -15,15 +15,16 @@ 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
- uses: coq-community/docker-coq-action@v1
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
4 changes: 0 additions & 4 deletions CHANGES

This file was deleted.

71 changes: 38 additions & 33 deletions README.md
Original file line number Diff line number Diff line change
@@ -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`.
11 changes: 6 additions & 5 deletions coq-my-plugin.opam
Original file line number Diff line number Diff line change
@@ -1,10 +1,11 @@
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"
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"
Expand All @@ -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: [
Expand Down

0 comments on commit c8d8385

Please sign in to comment.