OCamlPro · Halbaroth · Oct 8, 2024 · Sep 30, 2024 · Oct 8, 2024 · Oct 8, 2024
diff --git a/CHANGES.md b/CHANGES.md
@@ -1,3 +1,9 @@
+## unreleased
+
+### SMT-LIB support
+
+  - Remove the legacy frontend and AB-Why3 plugin
+
 ## v2.6.0
 
 ### Command-line interface

diff --git a/Makefile b/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 \

diff --git a/alt-ergo-parsers.opam b/alt-ergo-parsers.opam
diff --git a/alt-ergo-parsers.opam.template b/alt-ergo-parsers.opam.template
diff --git a/alt-ergo-plugin-ab-why3.opam b/alt-ergo-plugin-ab-why3.opam
diff --git a/alt-ergo-plugin-ab-why3.opam.template b/alt-ergo-plugin-ab-why3.opam.template
diff --git a/alt-ergo.opam b/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"}

diff --git a/default.nix b/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
     ]);

diff --git a/docs/sphinx_docs/Install/index.md b/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`

diff --git a/docs/sphinx_docs/Plugins/index.md b/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:alt-ergo@ocamlpro.com).
-```
-
 ```{toctree}
 :maxdepth: 2
 

diff --git a/docs/sphinx_docs/Usage/index.md b/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:

diff --git a/dune-project b/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))))