CI&Build fixes (#502)

* Add apt-get update step to workflows

* Some more apt-get updates

* Update to latest cmdliner

* Update bounds for cmdliner version in opam files

* Properly exit after --help/--version

* Require --prefix in configure script if opam is not present

* Try and remove superfluous printing

* Restore prefix in Makefile.config

* WIP

* Restrict dune version to avoid bug in dune uninstall

See ocaml/dune#5542

.github/workflows/build_js.yml

@@ -26,6 +26,10 @@ jobs:
       - name: Checkout code
         uses: actions/checkout@v2
 
+      # Update apt-get database
+      - name: Update apt-get database
+        run: sudo apt-get update
+
       # Retrieve the opam cache with unique key
       # A new cache is created/used if the `.opam` files changes or
       # if we use another ocaml version

.github/workflows/build_make.yml

@@ -24,6 +24,10 @@ jobs:
       - name: Checkout code
         uses: actions/checkout@v2
 
+      # Update apt-get database
+      - name: Update apt-get database
+        run: sudo apt-get update
+
       # Retrieve the opam cache with unique key
       # A new cache is created/used if the `.opam` files changes or
       # if we use another ocaml version
@@ -92,6 +96,10 @@ jobs:
       - name: Checkout code
         uses: actions/checkout@v2
 
+      # Update apt-get database
+      - name: Update apt-get database
+        run: sudo apt-get update
+
       # Retrieve the opam cache with unique key
       # A new cache is created/used if the `.opam` files changes or
       # if we use another ocaml version
@@ -162,6 +170,10 @@ jobs:
       - name: Checkout code
         uses: actions/checkout@v2
 
+      # Update apt-get database
+      - name: Update apt-get database
+        run: sudo apt-get update
+
       # Retrieve the opam cache with unique key
       # A new cache is created/used if the `.opam` files changes or
       # if we use another ocaml version

.github/workflows/build_ubuntu.yml

@@ -31,6 +31,10 @@ jobs:
       - name: Checkout code
         uses: actions/checkout@v2
 
+      # Update apt-get database
+      - name: Update apt-get database
+        run: sudo apt-get update
+
       # Retrieve the opam cache with unique key
       # A new cache is created/used if the `.opam` files changes or
       # if we use another ocaml version
@@ -124,6 +128,10 @@ jobs:
       - name: Checkout code
         uses: actions/checkout@v2
 
+      # Update apt-get database
+      - name: Update apt-get database
+        run: sudo apt-get update
+
       # Retrieve the opam cache with unique key
       # A new cache is created/used if the `.opam` files changes or
       # if we use another ocaml version

.github/workflows/documentation.yml

@@ -34,6 +34,10 @@ jobs:
       - name: Checkout code
         uses: actions/checkout@v2
 
+      # Update apt-get database
+      - name: Update apt-get database
+        run: sudo apt-get update
+
       # Retrieve the opam cache with unique key
       # A new cache is created/used if the `.opam` files changes or
       # if we use another ocaml version

Makefile

@@ -167,7 +167,7 @@ altgr-ergo:
 
 # Run non-regression tests using the scripts in
 # non-regression
-non-regression: all
+non-regression: bin
 	cp $(INSTALL_DIR)/default/bin/alt-ergo non-regression/alt-ergo.opt
 	cd non-regression &&  ./non-regression.sh
 	rm non-regression/alt-ergo.opt

alt-ergo-lib.opam

@@ -15,7 +15,7 @@ doc: "https://ocamlpro.github.io/alt-ergo"
 bug-reports: "https://github.com/OCamlPro/alt-ergo/issues"
 depends: [
   "ocaml" {>= "4.05.0"}
-  "dune" {>= "2.0"}
+  "dune" {>= "2.0" & < "3.0"}
   "dune-configurator"
   "num"
   "ocplib-simplex" {>= "0.4"}

alt-ergo-parsers.opam

@@ -15,7 +15,7 @@ doc: "https://ocamlpro.github.io/alt-ergo"
 bug-reports: "https://github.com/OCamlPro/alt-ergo/issues"
 depends: [
   "ocaml" {>= "4.05.0"}
-  "dune" {>= "2.0"}
+  "dune" {>= "2.0" & < "3.0"}
   "alt-ergo-lib" {= version}
   "psmt2-frontend" {>= "0.3"}
   "camlzip" {>= "1.07"}

alt-ergo.opam

@@ -13,11 +13,11 @@ doc: "https://ocamlpro.github.io/alt-ergo"
 bug-reports: "https://github.com/OCamlPro/alt-ergo/issues"
 depends: [
   "ocaml" {>= "4.05.0"}
-  "dune" {>= "2.0"}
+  "dune" {>= "2.0" & < "3.0"}
   "alt-ergo-lib" {= version}
   "alt-ergo-parsers" {= version}
   "menhir"
-  "cmdliner"
+  "cmdliner" {>= "1.1.0"}
   "odoc" {with-doc}
 ]
 dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"

altgr-ergo.opam

@@ -15,12 +15,12 @@ doc: "https://ocamlpro.github.io/alt-ergo"
 bug-reports: "https://github.com/OCamlPro/alt-ergo/issues"
 depends: [
   "ocaml" {>= "4.05.0"}
-  "dune" {>= "2.0"}
+  "dune" {>= "2.0" & < "3.0"}
   "alt-ergo-lib" {= version}
   "alt-ergo-parsers" {= version}
   "lablgtk"
   "conf-gtksourceview"
-  "cmdliner"
+  "cmdliner" {>= "1.1.0"}
   "odoc" {with-doc}
 ]
 dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"

configure.ml

@@ -84,8 +84,7 @@ let opam_check = lazy (
     Format.eprintf "ERROR: Couldn't find opam in env.@\n%a@."
       Format.pp_print_text "To solve this, you can either install opam, \
                             provide an explicit value to the `--prefix` argument \
-                            of this script, or provide explicit values to both \
-                            the `--libdir` and `--mandir` options of this script.";
+                            of this script.";
     exit 1
 )
 
@@ -112,10 +111,12 @@ let opam_var v =
 (* Compute actual values for config options *)
 let () =
   if !prefix <> "" then begin
+    update "prefix" prefix (fun () -> assert false); (* used to print info *)
     update "libdir" libdir (fun () -> Filename.concat !prefix "lib");
     update "mandir" mandir (fun () -> Filename.concat !prefix "man");
     ()
   end else begin
+    update "prefix" prefix (fun () -> opam_var "prefix");
     update "libdir" libdir (fun () -> opam_var "lib");
     update "mandir" mandir (fun () -> opam_var "man");
     ()
@@ -190,10 +191,12 @@ let () =
   let ch = open_out "Makefile.config" in
   let fmt = Format.formatter_of_out_channel ch in
   let () = Format.fprintf fmt "# Generated by configure@." in
+  let () = Format.fprintf fmt "prefix=%s@." !prefix in
   let () = Format.fprintf fmt "libdir=%s@." !libdir in
   let () = Format.fprintf fmt "mandir=%s@." !mandir in
   let () = close_out ch in
   let () = Format.printf "done.@." in
   ()
 
 let () = Format.printf "Good to go!@."
+

dune-project

@@ -26,11 +26,11 @@ Alt-Ergo is an automatic theorem prover of mathematical formulas. It was develop
 See more details on https://alt-ergo.ocamlpro.com/")
  (depends
   (ocaml (>= 4.05.0))
-  (dune (>= 2.0))
+  (dune (and (>= 2.0) (< 3.0)))
   (alt-ergo-lib (= :version))
   (alt-ergo-parsers (= :version))
    menhir
-   cmdliner
+  (cmdliner (>= 1.1.0))
   (odoc :with-doc)
   )
 )
@@ -51,12 +51,12 @@ See more details on https://alt-ergo.ocamlpro.com/"
 
  (depends
   (ocaml (>= 4.05.0))
-  (dune (>= 2.0))
+  (dune (and (>= 2.0) (< 3.0)))
   (alt-ergo-lib (= :version))
   (alt-ergo-parsers (= :version))
   lablgtk
   conf-gtksourceview
-  cmdliner
+  (cmdliner (>= 1.1.0))
   (odoc :with-doc)
 )
 )
@@ -77,7 +77,7 @@ See more details on http://alt-ergo.ocamlpro.com/"
 
  (depends
   (ocaml (>= 4.05.0))
-  (dune (>= 2.0))
+  (dune (and (>= 2.0) (< 3.0)))
   (alt-ergo-lib (= :version))
   (psmt2-frontend (>= 0.3))
   (camlzip (>= 1.07))
@@ -103,7 +103,7 @@ See more details on http://alt-ergo.ocamlpro.com/"
 
  (depends
   (ocaml (>= 4.05.0))
-  (dune (>= 2.0))
+  (dune (and (>= 2.0) (< 3.0)))
   dune-configurator
   num
   (ocplib-simplex (>= 0.4))

non-regression/valid/adts/simple_0.ae

@@ -39,4 +39,4 @@ goal g_valid_7:
   b = Z(c) ->
   c = Z(d) ->
   d = Z(a) ->
-  false
+  false

src/bin/common/parse_command.ml

@@ -1253,9 +1253,9 @@ let main =
     Arg.(value & pos ~rev:true 0 (some string) None & i) in
 
   let doc = "Execute Alt-Ergo on the given file." in
-  let exits = Term.default_exits in
-  let to_exit = Term.(exit_info ~doc:"on timeout errors" ~max:142 142) in
-  let dft_errors = Term.(exit_info ~doc:"on default errors" ~max:1 1) in
+  let exits = Cmd.Exit.defaults in
+  let to_exit = Cmd.Exit.info ~doc:"on timeout errors" ~max:142 142 in
+  let dft_errors = Cmd.Exit.info ~doc:"on default errors" ~max:1 1 in
   let exits = to_exit :: dft_errors :: exits in
 
   (* Specify the order in which the sections should appear
@@ -1301,20 +1301,29 @@ let main =
     ]
   in
 
-  Term.(ret (const mk_opts $
-             file $
-             parse_case_split_opt $ parse_context_opt $
-             parse_dbg_opt_spl1 $ parse_dbg_opt_spl2 $ parse_dbg_opt_spl3 $
-             parse_execution_opt $ parse_halt_opt $ parse_internal_opt $
-             parse_limit_opt $ parse_output_opt $ parse_profiling_opt $
-             parse_quantifiers_opt $ parse_sat_opt $ parse_term_opt $
-             parse_theory_opt $ parse_fmt_opt
-            )),
-  Term.info "alt-ergo" ~version:Version._version ~doc ~exits ~man
+  let term =
+    Term.(ret (const mk_opts $
+               file $
+               parse_case_split_opt $ parse_context_opt $
+               parse_dbg_opt_spl1 $ parse_dbg_opt_spl2 $ parse_dbg_opt_spl3 $
+               parse_execution_opt $ parse_halt_opt $ parse_internal_opt $
+               parse_limit_opt $ parse_output_opt $ parse_profiling_opt $
+               parse_quantifiers_opt $ parse_sat_opt $ parse_term_opt $
+               parse_theory_opt $ parse_fmt_opt
+              ))
+  in
+  let info =
+    Cmd.info "alt-ergo" ~version:Version._version ~doc ~exits ~man
+  in
+  Cmd.v info term
 
 let parse_cmdline_arguments () =
-  let r = Cmdliner.Term.(eval main) in
+  let r = Cmd.eval_value main in
   match r with
-  | `Ok false -> raise (Exit_parse_command 0)
-  | `Ok true -> ()
-  | e -> exit @@ Term.(exit_status_of_result e)
+  | Ok `Ok true -> ()
+  | Ok `Ok false -> raise (Exit_parse_command 0)
+  | Ok `Version | Ok `Help -> exit 0
+  | Error `Parse -> exit Cmd.Exit.cli_error
+  | Error `Term -> exit Cmd.Exit.internal_error
+  | Error `Exn -> exit Cmd.Exit.internal_error
+

src/lib/frontend/frontend.ml

@@ -144,6 +144,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
 
   let process_decl print_status used_context consistent_dep_stack
       ((env, consistent, dep) as acc) d =
+    Format.eprintf "@\n[COMMAND]@\n%a@." Commands.print d;
     try
       match d.st_decl with
       | Push n ->
@@ -224,19 +225,29 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
 
     with
     | SAT.Sat t ->
+      (* This case should mainly occur when a query has a non-unsat result,
+         so we want to print the status in this case. *)
       print_status (Sat (d,t)) (Steps.get_steps ());
       if get_model () then SAT.print_model ~header:true (get_fmt_mdl ()) t;
       env , consistent, dep
     | SAT.Unsat dep' ->
+      (* This case should mainly occur when a new assumption results in an unsat
+         env, in which case we do not want to print status, since the correct
+         status should be printed at the next query. *)
       let dep = Ex.union dep dep' in
       if get_debug_unsat_core () then check_produced_unsat_core dep;
-      print_status (Inconsistent d) (Steps.get_steps ());
+      (* print_status (Inconsistent d) (Steps.get_steps ()); *)
       env , false, dep
     | SAT.I_dont_know t ->
+      (* In this case, it's not clear whether we want to print the status.
+         Instead, it'd be better to accumulate in `consistent` a 3-case adt
+         and not a simple bool. *)
       print_status (Unknown (d, t)) (Steps.get_steps ());
       if get_model () then SAT.print_model ~header:true (get_fmt_mdl ()) t;
       env , consistent, dep
     | Util.Timeout as e ->
+      (* In this case, we obviously want to print the status,
+         since we exit right after  *)
       print_status (Timeout (Some d)) (Steps.get_steps ());
       raise e