Get rid of the legacy frontend finally!

This PR removes:
- the deprecated legacy frontend (parser and typechecker),
- the deprecated AB-Why3 plugin which depends on the legacy parser,
- the associated opam packages and dependencies (including `shell.nix`
  and our Makefile),
- all the reference in the documentation to these bastards,
- simplify `gentest` and rename the tag `dolmen` into `cdcl` in `tests/`,
- the option `frontend` in `Options`.

I also update the `Lib_usage` example because we now use the Dolmen.

We keep the `--frontend` option but now it is a no op command and we
output an appropriate message if users still use it.

This PR cannot be merged before fixing OCamlPro#1243.

CHANGES.md

@@ -1,3 +1,9 @@
+## unreleased
+
+### SMT-LIB support
+
+  - Remove the legacy frontend (#)
+
 ## v2.6.0
 
 ### Command-line interface

Makefile

@@ -43,7 +43,7 @@ SPHINXBUILD = sphinx-build
 # This excludes:
 # - .ml files generated by menhir or ocamllex
 #   (since they reside in dune specific directory)
-GENERATED_LINKS=alt-ergo alt-ergo.js alt-ergo-worker.js AB-Why3-plugin.cma AB-Why3-plugin.cmxs fm-simplex-plugin.cma fm-simplex-plugin.cmxs
+GENERATED_LINKS=alt-ergo alt-ergo.js alt-ergo-worker.js fm-simplex-plugin.cma fm-simplex-plugin.cmxs
 GENERATED=$(GENERATED_LINKS)
 
 
@@ -62,8 +62,7 @@ clean: generated-clean dune-clean ocamldot-clean
 distclean: makefile-distclean release-distclean
 
 # declare these aliases as phony
-.PHONY: world conf clean distclean alt-ergo-lib \
-	alt-ergo-parsers alt-ergo
+.PHONY: world conf clean distclean alt-ergo-lib alt-ergo
 
 # =================
 # Build rules (dev)
@@ -83,10 +82,6 @@ fm-simplex:
 	$(DUNE) build $(DUNE_FLAGS) @$(PLUGINS_DIR)/fm-simplex/all
 	$(DUNE) build $(DUNE_FLAGS) @install
 
-AB-Why3:
-	$(DUNE) build $(DUNE_FLAGS) @$(PLUGINS_DIR)/AB-Why3/all
-	$(DUNE) build $(DUNE_FLAGS) alt-ergo-plugin-ab-why3.install
-
 plugins:
 	$(DUNE) build $(DUNE_FLAGS) @$(PLUGINS_DIR)/all
 
@@ -99,7 +94,7 @@ all:
 
 # declare these targets as phony to avoid name clashes with existing directories,
 # particularly the "plugins" target
-.PHONY: lib bin fm-simplex AB-Why3 plugins all
+.PHONY: lib bin fm-simplex plugins all
 
 # =====================
 # Build rules (release)
@@ -241,7 +236,7 @@ lock:
 		./alt-ergo-lib.opam.locked
 
 dev-switch:
-	opam switch create . --deps-only --ignore-constraints-on alt-ergo-lib,alt-ergo-parsers
+	opam switch create . --deps-only --ignore-constraints-on alt-ergo-lib
 
 js-deps:
 	opam install \
@@ -295,7 +290,6 @@ FILES_DEST=public-release/$(PUBLIC_RELEASE)
 	tests \
 	alt-ergo.opam \
 	alt-ergo-lib.opam \
-	alt-ergo-parsers.opam \
 	dune-project \
 	Makefile \
 	README.md \

alt-ergo.opam

@@ -15,7 +15,6 @@ depends: [
   "ocaml" {>= "4.08.1"}
   "dune" {>= "3.14"}
   "alt-ergo-lib" {= version}
-  "alt-ergo-parsers" {= version}
   "menhir"
   "dune-site"
   "cmdliner" {>= "1.1.0"}

default.nix

@@ -27,27 +27,14 @@ let
     ];
   };
 
-  alt-ergo-parsers = ocamlPackages.buildDunePackage rec {
-    pname = "alt-ergo-parsers";
-    inherit version src;
-
-    minimalOCamlVersion = "4.08";
-    duneVersion = "3";
-
-    nativeBuildInputs = [ ocamlPackages.menhir ];
-    propagatedBuildInputs = [ alt-ergo-lib ] ++ (with ocamlPackages; [
-      psmt2-frontend
-    ]);
-  };
-
   alt-ergo = ocamlPackages.buildDunePackage {
     pname = "alt-ergo";
     inherit version src;
 
     minimalOCamlVersion = "4.08";
     duneVersion = "3";
 
-    buildInputs = [ alt-ergo-parsers ] ++ (with ocamlPackages; [
+    buildInputs = (with ocamlPackages; [
       cmdliner
       dune-site
     ]);

docs/sphinx_docs/Install/index.md

@@ -7,7 +7,7 @@ Alt-ergo is available on [opam], the ocaml package manager with the following co
 opam install alt-ergo
 ```
 
-This command will install the Alt-ergo library `alt-ergo-lib` and the parsers `alt-ergo-parsers`, as well as other librairies detailled in [dependencies](#dependencies).
+This command will install the Alt-ergo library `alt-ergo-lib`, as well as other librairies detailled in [dependencies](#dependencies).
 
 Since version 2.6.0, Alt-Ergo is compatible with opam 2.2 installations using both Cygwin and MSYS2 on Windows. To setup opam on Windows, please follow the instructions [here](https://ocamlpro.com/blog/2024_07_01_opam_2_2_0_releases/).
 
@@ -83,12 +83,6 @@ Note: these are somewhat obsolete; nowadays you can just use `dune`
 
   2. Install with `make install-lib`
 
-#### Alt-Ergo parsers
-
-  1. Compile with `make alt-ergo-parsers`
-
-  2. Install with `make install-parsers`
-
 #### Alt-Ergo binary
 
   1. Compile with `make alt-ergo`

docs/sphinx_docs/Plugins/index.md

@@ -24,16 +24,6 @@ be registered in the `(alt-ergo plugins)` site using
 to be available as an option to `--inequalities-plugin`.
 ```
 
-## AB why3 plugin (**deprecated**)
-
-```{warning}
-The AB Why3 plugin requires the use of the `--frontend legacy` option, which is
-deprecated and will be removed in the next version of Alt-Ergo.
-
-If you are using this plugin and would like it to be available in new versions
-of Alt-Ergo, please contact [the Alt-Ergo developers](mailto:[email protected]).
-```
-
 ```{toctree}
 :maxdepth: 2
 

docs/sphinx_docs/Usage/index.md

@@ -40,24 +40,6 @@ Alt-Ergo supports file extensions:
 
 See the [SMT-LIB language] and [Alt-ergo native language] sections for more information about the format of the input files.
 
-### Frontend option
-
-The `--frontend` option lets you select the frontend used to parse and type the input file. Since version 2.5.0,
-Alt-Ergo integrates two frontends:
-- The `dolmen` frontend is the default frontend, powered by the
-  [Dolmen](https://github.com/Gbury/dolmen) library.  The native and SMT-LIB
-  languages are both supported by this frontend.
-- The `legacy` frontend is the historical frontend of Alt-Ergo supporting the
-  native language. You can select it with the `--frontend legacy` option. The
-  legacy frontend is deprecated, and will be removed in a future release.
-
-```{admonition} Note
-
-The `legacy` frontend has limited support for the SMT-LIB language, but many
-SMT-LIB features will not work with the `legacy` frontend. Use the (default)
-`dolmen` frontend for SMT-LIB inputs.
-```
-
 ### Preludes
 
 Preludes can be passed to Alt-Ergo as follows:

dune-project

@@ -28,7 +28,6 @@ See more details on https://alt-ergo.ocamlpro.com/")
   (ocaml (>= 4.08.1))
   dune
   (alt-ergo-lib (= :version))
-  (alt-ergo-parsers (= :version))
   menhir
   dune-site
   (cmdliner (>= 1.1.0))
@@ -38,29 +37,6 @@ See more details on https://alt-ergo.ocamlpro.com/")
  (sites (share preludes) (lib plugins))
 )
 
-(package
- (name alt-ergo-parsers)
- (synopsis "The Alt-Ergo SMT prover parser library")
- (description "\
-This is the parser library used in the Alt-Ergo SMT solver.
-
-Alt-Ergo is an automatic theorem prover of mathematical formulas. It was developed at LRI, and is now maintained at OCamlPro.
-
-See more details on http://alt-ergo.ocamlpro.com/"
- )
- (license "LicenseRef-OcamlPro-Non-Commercial")
-
- (depends
-  (ocaml (>= 4.08.1))
-  dune
-  (alt-ergo-lib (= :version))
-  (psmt2-frontend (>= 0.4))
-  menhir
-  stdlib-shims
-  (odoc :with-doc)
- )
-)
-
 (package
  (name alt-ergo-lib)
  (synopsis "The Alt-Ergo SMT prover library")
@@ -97,18 +73,3 @@ See more details on http://alt-ergo.ocamlpro.com/"
   (result (< 1.5))
  )
 )
-
-(package
- (name alt-ergo-plugin-ab-why3)
- (synopsis "An experimental Why3 frontend for Alt-Ergo")
- (description "\
-An experimental front-end that parses a subset of Why3's logic. More
-precisely, this front-end targets proof obligations generated by the
-Atelier-B framework in Why3 format. It should be used with a prelude
-defining the B Set theory.")
- (license "LGPL-2.1-only")
-
- (depends
-  (alt-ergo (= :version))
-  (alt-ergo-lib (= :version))
-  (alt-ergo-parsers (= :version))))

examples/lib_usage.ml

@@ -55,37 +55,37 @@
 
  ****)
 
-Format.eprintf
-  "\n(* This minimal example shows how to use Alt-Ergo's lib *)\n@."
+(* Format.eprintf
+   "\n(* This minimal example shows how to use Alt-Ergo's lib *)\n@."
 
-open AltErgoLib
+   open AltErgoLib *)
 
-module PA = Parsed_interface
+(* module PA = Parsed_interface
 
-let _x = PA.mk_var_type Loc.dummy "'a"
+   let _x = PA.mk_var_type Loc.dummy "'a"
 
-let one = PA.mk_int_const Loc.dummy "1"
-let two = PA.mk_int_const Loc.dummy "2"
-let three = PA.mk_int_const Loc.dummy "3"
-let one_two = PA.mk_add Loc.dummy one two
-let eq1 = PA.mk_pred_eq Loc.dummy one_two three
-let eq2 = PA.mk_pred_eq Loc.dummy one three
+   let one = PA.mk_int_const Loc.dummy "1"
+   let two = PA.mk_int_const Loc.dummy "2"
+   let three = PA.mk_int_const Loc.dummy "3"
+   let one_two = PA.mk_add Loc.dummy one two
+   let eq1 = PA.mk_pred_eq Loc.dummy one_two three
+   let eq2 = PA.mk_pred_eq Loc.dummy one three
 
-let goal_1 = PA.mk_goal Loc.dummy "toy_1" eq1
-let goal_2 = PA.mk_goal Loc.dummy "toy_2" eq2
-let goal_3 = PA.mk_goal Loc.dummy "toy_3" (PA.mk_not Loc.dummy eq1)
+   let goal_1 = PA.mk_goal Loc.dummy "toy_1" eq1
+   let goal_2 = PA.mk_goal Loc.dummy "toy_2" eq2
+   let goal_3 = PA.mk_goal Loc.dummy "toy_3" (PA.mk_not Loc.dummy eq1)
 
-let parsed = [goal_1; goal_2; goal_3]
+   let parsed = [goal_1; goal_2; goal_3]
 
-let typed, _env = Typechecker.type_file parsed
+   let typed, _env = Typechecker.type_file parsed
 
-let pbs = Typechecker.split_goals_and_cnf typed
+   let pbs = Typechecker.split_goals_and_cnf typed
 
-module SAT = Fun_sat_frontend.Make(Theory.Main_Default)
-module FE = Frontend.Make(SAT)
+   module SAT = Fun_sat_frontend.Make(Theory.Main_Default)
+   module FE = Frontend.Make(SAT)
 
-let () =
-  List.iter
+   let () =
+   List.iter
     (fun (pb, _goal_name) ->
        let ctxt = Frontend.init_all_used_context () in
        let env = FE.init_env ctxt in
@@ -95,4 +95,4 @@ let () =
          Format.printf "unknown@."
        | `Unsat ->
          Format.printf "unsat@."
-    ) pbs
+    ) pbs *)