Flambda compilation instructions

FLAMBDA.md

@@ -0,0 +1,88 @@
+# FLAMBDA
+
+This document describes how to install Alt-Ergo with FLAMBDA 1 and 2 with opam.
+Note that the FLAMBDA 2 instructions are incomplete: feel free to fix them if
+you manage to install alt-ergo with it.
+
+We first describe how to set up an opam switch with flambda, then how to
+configure the compilation procedure with flambda
+
+## Install with FLAMBDA
+
+### FLAMBDA 1
+
+First, create a fresh empty switch and install the base
+
+```
+$ opam switch create flambda1 --empty
+$ eval $(opam env)
+$ opam install ocaml-variants.4.14.1+options ocaml-option-flambda
+$ opam switch set-invariant ocaml.4.14.1
+```
+
+If alt-ergo depends on a specific version of dolmen, do not forget about pinning
+the right dolmen version before installing the dependencies.
+
+`$ opam install . --deps-only`
+
+Finally, you can build with `m bin`.
+
+### FLAMBDA 2
+
+OCAMLPARAM='_,rounds=3,O3=1,inline=20,inline-max-unroll=5' opam install ocaml-variants.4.14.1+options ocaml-option-flambda
+
+To install Alt-Ergo with FLambda, you first need to have:
+- ocaml.4.14.1 installed on your current opam switch;
+- [opam-custom-install](https://gitlab.ocamlpro.com/louis/opam-custom-install) installed on any switch.
+
+Create a new switch in which we will install the compiler:
+
+```
+$ opam switch create flambda-backend --empty --repositories=flambda2=git+https://github.com/ocaml-flambda/flambda2-opam.git,default
+$ opam switch THE_4.14.1_SWITCH
+```
+
+Fetch the `flambda-backend` repository:
+
+```
+$ git clone https://github.com/ocaml-flambda/flambda-backend.git
+$ cd flambda-backend
+```
+
+Once in the flambda directory, configure the build directory:
+
+```
+$ autoconf
+$ ./configure --prefix=PATH_TO_THE_EMPTY_FLAMBDA_SWITCH --enable-middle-end=flambda2 --enable-legacy-library-layout
+```
+
+The last option `--enable-legacy-library-layout` is required for projects on the
+4.14.1 OCaml version (and probably 4.14.0 too) because of the `Unix` module
+dependency. Then, you can build the project and install it on the
+flambda-backend switch.
+
+```
+$ make _install
+$ opam switch flambda-backend
+$ opam custom-install ocaml-variants.4.14.1+flambda2 -- make install_for_opam
+$ opam reinstall --forget-pending
+$ opam install ocaml.4.14.1
+```
+
+## Build with flambda
+
+When you build alt-ergo, you can set compilation options through the
+`OCAMLPARAM` variable. Here is an example on how to set options to the
+compiler to build alt-ergo with extreme optimization:
+
+```
+$OCAMLPARAM='_,rounds=5,O3=1,inline=100,inline-max-unroll=5' make bin
+```
+
+You can find an exhaustive documentation
+[here](https://v2.ocaml.org/manual/flambda.html).
+You may also want to use `ulimit` if you plan to use your computer while
+compiling.
+
+NB: this variable can also be set to the `opam install` commands installing the
+dependencies to optimize them as well.

alt-ergo-lib.opam

@@ -25,14 +25,11 @@ depends: [
   "seq"
   "fmt" {>= "0.9.0"}
   "stdlib-shims"
-  "ppx_blob" {>= "0.7.2"}
   "camlzip" {>= "1.07"}
   "odoc" {with-doc}
-  "ppx_deriving"
   "stdcompat"
 ]
 conflicts: [
-  "ppxlib" {< "0.30.0"}
   "result" {< "1.5"}
 ]
 build: [

dune-project

@@ -85,14 +85,11 @@ See more details on http://alt-ergo.ocamlpro.com/"
   seq
   (fmt (>= 0.9.0))
   stdlib-shims
-  (ppx_blob (>= 0.7.2))
   (camlzip (>= 1.07))
   (odoc :with-doc)
-  ppx_deriving
   stdcompat
  )
  (conflicts
-  (ppxlib (< 0.30.0))
   (result (< 1.5))
  )
 )

src/bin/common/solving_loop.ml

@@ -27,7 +27,6 @@
 (*     More details can be found in the directory licenses/               *)
 (*                                                                        *)
 (**************************************************************************)
-
 open AltErgoLib
 open D_loop
 

src/lib/dune

@@ -26,8 +26,6 @@
     fmt
     stdcompat
   )
-  (preprocess (pps ppx_blob ppx_deriving.show ppx_deriving.enum ppx_deriving.fold))
-  (preprocessor_deps (glob_files ../preludes/*.ae))
 
   ; .mli only modules *also* need to be in this field
   (modules_without_implementation matching_types sig sig_rel)

src/lib/reasoners/th_util.ml

@@ -36,7 +36,13 @@ type theory =
   | Th_adt
   | Th_arrays
   | Th_UF
-[@@deriving show]
+
+let pp_theory fmt t = Fmt.string fmt @@ match t with
+  | Th_arith -> "Th_arith"
+  | Th_sum -> "Th_sum"
+  | Th_adt -> "Th_adt"
+  | Th_arrays -> "Th_arrays"
+  | Th_UF -> "Th_UF"
 
 type limit_kind =
   | Above

src/lib/reasoners/th_util.mli

@@ -36,7 +36,8 @@ type theory =
   | Th_adt
   | Th_arrays
   | Th_UF
-[@@deriving show]
+
+val pp_theory : Format.formatter -> theory -> unit
 
 type limit_kind =
   | Above