feat: Also use Cmdliner for the main abella program

.github/workflows/check-tests.yml

@@ -11,11 +11,11 @@ jobs:
     strategy:
       matrix:
         os: [ubuntu-latest]
-        ocaml-compiler: [4.12.x, 4.14.x]
+        ocaml-compiler: [4.12.x, 4.14.x, 5.1.x]
     runs-on: ${{ matrix.os }}
     steps:
       - name: Checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
       - name: Use OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v2
         with:

CHANGES.md

@@ -1,3 +1,14 @@
+Changes since 2.0.8-rc1
+-----------------------
+
+Possibly breaking changes
+
+* The command line for the `abella` command has slightly changed.
+  - The old `-v` option is removed; use `--version` instead.
+  - The old `-nr` option is removed; use `--non-recursive` instead.
+* In batch mode, `abella` always produces `file.thc` from `file.thm`.
+
+
 Changes in 2.0.8-rc1 from 2.0.7
 -------------------------------
 

README.md

@@ -1,19 +1,29 @@
 Quick Start
 ===========
 
-Compile Abella by running "make" from the root directory. This will
-create the binary "abella" (on Unix-like systems, including Mac OS X),
-or "abella.exe" (on Windows). This binary can be freely copied
-anywhere.
+The easiest way to install Abella is using [OPAM][opam] (version 2.1+).
 
-Use the following walkthrough for an introduction to using Abella:
+[opam]: https://opam.ocaml.org
 
-  https://abella-prover.org/walkthrough.html
+1. Go to the topmost directory of the clone of this repository,
+   i.e., the location of this very `README.md` file.
+2. Run: `opam pin abella .` (note the final period)
+3. When prompted by OPAM, say `yes` to install Abella.
+4. Whenever you do a `git pull`, also do: `opam reinstall abella`.
+
+To uninstall Abella using OPAM, do:
+
+1. From the same directory as above, run: `opam remove abella`.
+2. Then run: `opam unpin abella`.
 
 
 More Information
 ================
 
+Use the following walkthrough for an introduction to using Abella:
+
+  https://abella-prover.org/walkthrough.html
+
 More information on Abella is available at
 
   https://abella-prover.org/
@@ -27,7 +37,6 @@ issue tracker for Abella, available from:
 
   https://github.com/abella-prover/abella/issues
 
-
 Discussion of Abella and its uses happens on this mailing list.
 
   http://groups.google.com/group/abella-theorem-prover