Merge pull request #113 from ott-lang/docker-ci

add basic CI based on official Coq Docker images

.github/workflows/docker-action.yml

@@ -0,0 +1,50 @@
+name: Docker CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'coqorg/coq:dev'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v4
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          custom_image: ${{ matrix.image }}
+          custom_script: |
+            {{before_install}}
+            startGroup "Build ott dependencies"
+              opam pin add -n -y -k path ott .
+              opam update -y
+              opam install -y -j $(nproc) ott --deps-only
+            endGroup
+            startGroup "Build ott"
+              opam install -y -v -j $(nproc) ott
+              opam list
+            endGroup
+            startGroup "Build coq-ott dependencies"
+              opam pin add -n -y -k path coq-ott .
+              opam update -y
+              opam install -y -j $(nproc) coq-ott --deps-only
+            endGroup
+            startGroup "Build coq-ott"
+              opam install -y -v -j $(nproc) coq-ott
+              opam list
+            endGroup
+            startGroup "Uninstallation test"
+              opam remove -y coq-ott
+              opam remove -y ott
+            endGroup
+          export: 'OPAMWITHTEST'
+        env:
+          OPAMWITHTEST: 'true'

README.md

@@ -1,5 +1,10 @@
 # Ott
 
+[![Docker CI][docker-action-shield]][docker-action-link]
+
+[docker-action-shield]: https://github.com/ott-lang/ott/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/ott-lang/ott/actions/workflows/docker-action.yml
+
 Ott is a tool for writing definitions of programming languages and
 calculi.  It takes as input a definition of a language syntax and
 semantics, in a concise and readable ASCII notation that is close to
@@ -53,7 +58,7 @@ More substantially, Ott has been used for work on
 <a href="http://www.cl.cam.ac.uk/~so294/ocaml">OCaml light</a>, by
   <a href="http://www.cl.cam.ac.uk/~so294">Scott Owens</a>.
 
-As of 2020, Ott remains in continuous use.
+As of 2024, Ott remains in continuous use.
 
 ## Documentation
 
@@ -119,7 +124,7 @@ Ott is available as
 an [opam](https://opam.ocaml.org) package and a 
 [github repo](https://github.com/ott-lang/ott).
 
-### With OPAM  (released version)
+### With opam (released version)
 
 First, ensure you have opam (the OCaml package manager) installed,
 version 2.0 or greater (opam 1 versions of ott are no longer
@@ -144,13 +149,13 @@ repository:
 and then run `opam install coq-ott`.
 
 
-### With OPAM (github checkout)
+### With opam (github checkout)
 
 In the checkout directory, run `opam pin add ott .`.
 
 To rebuild and reinstall after local changes, run `opam upgrade --working-dir ott`  (or `opam upgrade -w ott`).
 
-### Without OPAM
+### Without opam
 
 Ott depends on OCaml version 4.07.0 or later and the ocamlgraph package. It
 builds with (at least) OCaml 4.07.0 and 4.14.0, and ocamlgraph 1.8.8. 
@@ -207,7 +212,7 @@ Ott Emacs directory.
 (require 'ott-mode)
 ```
 
-For installations using OPAM on \*nix systems, it is sufficient to use the following code, which will call `opam config var prefix` at load-time.
+For installations using opam on \*nix systems, it is sufficient to use the following code, which will call `opam config var prefix` at load-time.
 
 ```ELisp
 (setq opam-share (substring (shell-command-to-string "opam config var share") 0 -1))
@@ -245,7 +250,6 @@ directory                | description
 `tex/`                   | auxiliary files for LaTeX
 `hol/`                   | auxiliary files for HOL
 `menhir/`                | auxiliary files for menhir
-`ocamlgraph-1.7.tar.gz`  | a copy of the ocamlgraph library
 `regression/`            | regression-test machinery
 `tests/`                 | various small example Ott files
 `src/`                   | the (OCaml) Ott sources
@@ -434,9 +438,4 @@ The following LaTeX, Coq, HOL, and Isabelle files, except the proof scripts, are
 
 ## Copyright information
 
-The ocamlgraph library is distributed under the LGPL (from
-http://www.lri.fr/~filliatr/ftp/ocamlgraph/); we include a snapshot
-for convenience. For its authorship and copyright information see the
-files therein.
-
-All other files are distributed under the BSD-style licence in LICENCE.
+Files are distributed under the BSD-style licence in LICENCE.

coq-ott.opam

@@ -1,5 +1,6 @@
 opam-version: "2.0"
 maintainer: "palmskog@gmail.com"
+version: "dev"
 
 homepage: "http://www.cl.cam.ac.uk/~pes20/ott/"
 dev-repo: "git+https://github.com/ott-lang/ott.git"

ott.opam

@@ -1,8 +1,8 @@
 opam-version: "2.0"
-version: "0.33"
+version: "dev"
 maintainer: "Thibaut Pérami <Thibaut.Perami@cl.cam.ac.uk>"
 authors: ["Peter Sewell" "Francesco Zappa Nardelli" "Scott Owens"]
-license: ["BSD-3-Clause" "LGPL-2.1-only"]
+license: "BSD-3-Clause"
 homepage: "http://www.cl.cam.ac.uk/~pes20/ott/"
 bug-reports: "https://github.com/ott-lang/ott/issues"
 depends: [