release: Version 2.0.8

Also:

* fixes some minor issues with parsing `--flags`
* builds `src/abell_doc_dist.ml` using Makefile instead of dune
  - this removes a dependency on npm, which opam-ci cannot run

.github/workflows/check-tests.yml

@@ -21,5 +21,5 @@ jobs:
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
       - run: opam install . --deps-only --with-test
-      - run: opam exec -- dune build
+      - run: opam exec -- make all-release
       - run: opam exec -- dune runtest

CHANGES.md

@@ -1,21 +1,14 @@
-Changes since 2.0.8-rc1
------------------------
+Changes in 2.0.8 from 2.0.7
+---------------------------
 
 Possibly breaking changes
 
+* Abella now uses [Dune][dune] instead of [ocamlbuild][ocamlbuild].  
+  (#138, additional contributions: Chase Johnson)
 * 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
--------------------------------
-
-Possibly breaking changes
-
-* Abella now uses [Dune][dune] instead of [ocamlbuild][ocamlbuild].  
-  (#138, additional contributions: Chase Johnson)
+* In batch mode, Abella always produces `file.thc` from `file.thm`.
 * Abella's parser changed from [ocamlyacc][ocamlyacc] to [Menhir][menhir]
 * Abella's annotation mode (`-a`) now produces annotations in JSON format
   instead of in HTML fragments. The JSON schema should be seen as
@@ -35,7 +28,7 @@ Additions
   sources into HTML pages that resemble the Abella examples on the
   web-site: https://abella-prover.org/examples/
 
-  Run `abella_doc -help` for usage instructions.
+  Run `abella_doc --help` for usage instructions.
 * **Dependency Generation (`abella_dep`)**: There is now a special
   program called `abella_dep` that can be used to generate a
   `Makefile`-based dependency graph. Executing `make` on that

Makefile

@@ -3,12 +3,18 @@
 BINS := src/abella.exe src/abella_doc.exe src/abella_dep.exe
 
 .PHONY: all all-release
-all:
+all: src/abella_doc_dist.ml
 	dune build $(BINS)
 
 all-release:
 	dune build --release $(BINS)
 
+src/abella_doc_dist.ml: $(wildcard support/**/*.ts support/**/*.css)
+	( cd support && \
+	  npm install --no-save && \
+	  npm run build )
+	ocaml-crunch -m plain -o src/abella_doc_dist.ml support/dist
+
 AIN := abella.install
 
 .PHONY: $(AIN)

abella.opam

@@ -1,6 +1,6 @@
 opam-version: "2.0"
 name: "abella"
-version: "2.0.8-rc1"
+version: "2.0.8"
 synopsis: "Interactive theorem prover based on lambda-tree syntax"
 maintainer: "[email protected]"
 authors: [
@@ -14,13 +14,13 @@ build: [
   [make "all-release" "abella.install"]
 ]
 depends: [
-  "ocaml" { >= "4.12.0" }
-  "cmdliner" { >= "1.2.0" & build }
-  "menhir" { >= "20211012" & build }
-  "dune" { >= "3.11" & build }
-  "crunch" { >= "3.3.0" & build }
-  "yojson" { >= "2.1.1" & build }
-  "ounit2" { with-test }
+  "ocaml"    { >= "4.12.0" }
+  "cmdliner" { >= "1.2.0" }
+  "menhir"   { >= "20211012" }
+  "yojson"   { >= "2.1.1" }
+  "dune"     { >= "3.11" }
+  "crunch"   { >= "3.3.0" & build }
+  "ounit2"   { with-test }
 ]
 bug-reports: "https://github.com/abella-prover/abella/issues"
 dev-repo: "git+https://github.com/abella-prover/abella.git"

dune-project

@@ -1,5 +1,5 @@
 (lang dune 3.11)
 (name abella)
-(version v2.0.8-rc1)
+(version v2.0.8)
 (using menhir 2.0)
 (using directory-targets 0.1)

src/abella.ml

@@ -441,14 +441,21 @@ let query q =
       Output.msg_printf "No more solutions."
   | _ -> assert false
 
-let set_fail ~key ~expected v =
-  failwithf "Unknown value '%s' for key %S; expected %s"
+let on_or_off = {|"on" or "off"|}
+
+let set_fail ~key ?(expected = on_or_off) v =
+  failwithf "Unknown value %S for key %S; expected %s"
     (set_value_to_string v) key expected
 
 let set_subgoal_max_spec spec =
-  let buf = Lexing.from_string spec in
-  let spec = Parser.depth_spec Lexer.token buf in
-  Prover.set_subgoal_max spec
+  try
+    let buf = Lexing.from_string spec in
+    let spec = Parser.depth_spec Lexer.token buf in
+    Prover.set_subgoal_max spec
+  with
+  | Abella_types.Reported_parse_error
+  | Parser.Error ->
+      failwithf "Invalid subgoal depth specification: %S" spec
 
 let set k v =
   match k, v with
@@ -465,30 +472,26 @@ let set k v =
       set_subgoal_max_spec spec
   | "subgoals", _ -> set_fail v
                        ~key:"subgoals"
-                       ~expected:"'on', 'off', non-negative integer, or depth specification"
+                       ~expected:{|"on", "off", non-negative integer, or depth specification|}
 
   | "instantiations", Str "on" -> Prover.show_instantiations := true
   | "instantiations", Str "off" -> Prover.show_instantiations := false
   | "instantiations", _ -> set_fail v
                              ~key:"instantiations"
-                             ~expected:"'on' or 'off'"
 
   | "types", Str "on" -> Metaterm.show_types := true
   | "types", Str "off" -> Metaterm.show_types := false
   | "types", _ -> set_fail v
                     ~key:"types"
-                    ~expected:"'on' or 'off'"
 
   | "search_depth", Int d when d >= 0 -> Prover.search_depth := d
   | "search_depth", _ -> set_fail v
                            ~key:"search_depth"
-                           ~expected:"non-negative integer"
 
   | "witnesses", Str "on" -> witnesses := true
   | "witnesses", Str "off" -> witnesses := false
   | "witnesses", _ -> set_fail v
                         ~key:"witnesses"
-                        ~expected:"'on' or 'off'"
 
   | "load_path", QStr s ->
       Filepath.set_load_path ~wrt:!input_wrt s
@@ -585,12 +588,7 @@ let rec process1 () =
         | Unify.UnifyFailure fl -> Unify.explain_failure fl
         | Unify.UnifyError err -> Unify.explain_error err
         | UserInterrupt -> "Interrupted (use Ctrl-D to quit)"
-        | _ ->
-            Printexc.to_string e ^ "\n\n\
-                                   \ Sorry for displaying a naked OCaml exception. An informative error message\n\
-                                   \ has not been designed for this situation.\n\n\
-                                   \ To help improve Abella's error messages, please file a bug report at\n\
-                                   \ <https://github.com/abella-prover/abella/issues>. Thanks!"
+        | _ -> sorry e
       in
       Output.msg_printf ~severity:Error "Error: %s" msg ;
       interactive_or_exit ()
@@ -766,7 +764,7 @@ and process_top1 () =
       compile (CClose(List.map (fun aty -> (aty, Subordination.subordinates !sr aty)) atys))
   end ;
   if not config.annotate then Output.blank_line ()
-      
+
 (* Command line and startup *)
 
 let welcome_msg = sprintf "Welcome to Abella %s.\n" Version.version
@@ -781,9 +779,15 @@ let set_compile_out filename =
       (Filename.basename filename) ".part" in
   config.compiled <- Some { name = filename ; temp_name ; channel }
 
+let set_or_exit k v =
+  try set k v with
+  | Failure msg ->
+      Output.msg_printf ~severity:Error "Error: %s" msg ;
+      raise @@ AbellaExit 1
+
 let abella_main flags switch output compiled annotate norec _em infile =
   try begin
-    List.iter (fun (k, v) -> set k v) flags ;
+    List.iter (fun (k, v) -> set_or_exit k v) flags ;
     if switch then config.mode <- `switch ;
     Option.iter set_output output ;
     Option.iter set_compile_out compiled ;
@@ -804,7 +808,11 @@ let abella_main flags switch output compiled annotate norec _em infile =
       Output.msg_printf "%s" welcome_msg ;
     State.Undo.set_enabled (config.mode <> `batch) ;
     while true do process1 () done ; 0
-  end with AbellaExit n -> n
+  end with
+  | AbellaExit n -> n
+  | e ->
+      Output.msg_printf ~severity:Error "Error: %s" (sorry e) ;
+      1
 
 let () =
   Sys.set_signal Sys.sigint
@@ -814,32 +822,23 @@ let () =
 
   let flag_conv : (string * set_value) list Arg.conv =
     let parse str =
-      String.split ~test:(fun c -> c = ',') str |>
-      List.map (String.split ~test:(fun c -> c = '=')) |>
-      List.filter_map begin function
-      | [k ; v] -> begin
-          if String.length v < 1 then None else
-          match v.[0] with
-          | '0' .. '9' ->
-              int_of_string_opt v |>
-              Option.map (fun n -> (k, Int n))
-          | '"' ->
-              (* [FIXME] does not handle foo="bar=baz" *)
-              if String.get v (String.length v - 1) = '"'
-              then Some (k, QStr (String.sub v 1 (String.length v - 2)))
-              else None
-          | _ ->
-              Some (k, Str v)
-        end
-      | [k] -> Some (k, Str "on")
-      | _ -> None
-      end |> Result.ok in
+      try
+        Lexing.from_string str |>
+        Parser.cmdline_flags Lexer.token |>
+        Result.ok
+      with
+      | Abella_types.Reported_parse_error
+      | Parser.Error ->
+          Printf.ksprintf (fun s -> `Msg s)
+            "Could not parse argument: %S" str
+          |> Result.error
+    in
     let print _ _ = () in
     Arg.conv (parse, print)
   in
 
   let flags =
-    let doc = "Intialize flags based on $(docv), which is a \
+    let doc = "Intialize Abella flags based on $(docv), which is a \
                comma-separated list of key=value pairs. Unknown \
                flags are silently ignored." in
     Arg.(value @@ opt flag_conv [] @@
@@ -883,7 +882,9 @@ let () =
   in
 
   let file =
-    let doc = "An Abella development (.thm file) to process in batch mode." in
+    let doc = "An Abella development to process in batch mode. \
+               The $(docv) must end with the extension $(b,.thm). \
+               If no $(docv) is provided, Abella runs in interactive mode." in
     Arg.(value @@ pos 0 (some string) None @@
          info [] ~docv:"FILE" ~doc)
   in