Use dune as build system

.gitignore

@@ -1,46 +1,26 @@
-.depend
+# Metadata files
 .gitignore
 META
-alt-ergo/Makefile.configurable
-Makefile.configurable
-config.status
+
+# Generated source files
+*.merlin
+sources/Makefile.config
+sources/lib/util/config.ml
+
+# Generated installation files
+sources/*.install
+
+# Generated build artifacts
+sources/_build
+
+# Generated release files
+public-release
+
+# Generated tmp files
 *.make.revision
-*.annot
-*.cmi
-*.cmo
-*.cmx*
-*.o
-*.output
-*.cmxs
-*.cma
-alt-ergo.opt
-alt-ergo.byte
-altgr-ergo.opt
-altgr-ergo.byte
-ctrl-alt-ergo.byte
-ctrl-alt-ergo.opt
-altErgo.cmo
-altErgo.cmx
-altErgo.cmi
-altErgo.o
-*.log
 *~
-essentiel*
-configure
-autom4te*
 archi.*
 mlw
 tmp/
 *.tmp
 alt-ergo/tmp/
-*.cmt
-*.cmti
-*.conflicts
-*.automaton
-sources/lib/util/config.ml
-sources/parsers/why/why_lexer.ml
-sources/parsers/why/why_parser.ml
-sources/parsers/why/why_parser.mli
-sources/plugins/AB-Why3/why3_lexer.ml
-sources/plugins/AB-Why3/why3_parser.ml
-sources/plugins/AB-Why3/why3_parser.mli

.travis.yml

@@ -14,9 +14,10 @@ before_install:
 - git status
 
 install:
-- wget -qq https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin system
+- sudo wget -O /usr/local/bin/opam https://github.com/ocaml/opam/releases/download/2.0.1/opam-2.0.1-x86_64-linux
+- sudo chmod a+x /usr/local/bin/opam
 - export OPAMYES=1
-- opam init --comp system
+- opam init --disable-sandboxing --bare
 
 script:
 - sh ./travis.sh

non-regression/main_script.sh

@@ -28,7 +28,7 @@ cpt=0
 COLS=$(tput cols)
 limit=""
 while [ $cpt -lt $COLS ]; do
-    cpt=`expr $cpt + 1`        
+    cpt=`expr $cpt + 1`
     limit=`echo -n $limit-`
 done
 

non-regression/non-regression.sh

@@ -18,9 +18,10 @@ echo "[ with Tableaux-CDCL ]"
 echo "===============================================================================================";
 ./main_script.sh "-sat-solver Tableaux-CDCL"
 
-echo "===============================================================================================\c";
+echo "===============================================================================================";
 echo "===============================================================================================";
 echo "[ WITH FM-SIMPLEX ]"
-echo "===============================================================================================\c";
 echo "===============================================================================================";
-./main_script.sh "-inequalities-plugin `pwd`/../sources/fm-simplex-plugin.cmxs"
+echo "===============================================================================================";
+./main_script.sh "-inequalities-plugin `pwd`/../sources/_build/install/default/share/plugins/fm-simplex-plugin.cmxs"
+

sources/Makefile

@@ -1,3 +1,220 @@
-include Makefile.configurable
-include Makefile.users
-include Makefile.developers
+
+# ====================================
+# Variable Definitions & Configuration
+# ====================================
+
+NAME=alt-ergo
+
+# Include configuration makefile
+# Since there is a rule to create/update this makefile, make
+# should automatically run it and reload/restart if needed
+include Makefile.config
+
+# Some variables to help with adding
+# flags and/or renaming the dune binary
+DUNE=dune
+DUNE_FLAGS=
+
+# List the files:
+# - generated by rules in this makefile,
+# - used by the build process
+#
+# This excludes:
+# - .ml files generated by menhir or ocamllex
+#   (since they reside in dune specific directory)
+GENERATED=lib/util/config.ml
+
+
+# =======
+# Aliases
+# =======
+
+# IMPORTANT: this is the first rules, and as such the default
+# run when "make is called", keep it as the first rule
+world: all
+
+# Small alias to re-generate necessary files for the build
+gen: $(GENERATED)
+
+# Convenient alias for running all configuration steps
+conf: Makefile Makefile.config lib/util/config.ml
+
+# Alias for generated artifacts
+clean: dune-clean
+
+# Alias to remove all generated files
+distclean: makefile-distclean release-distclean
+
+# declare these aliases as phony
+.PHONY: world gen conf clean distclean
+
+
+
+# ===========
+# Build rules
+# ===========
+
+# Build the alt-ergo lib
+lib: gen
+	$(DUNE) build $(DUNE_FLAGS) \
+		lib/AltErgoLib.cma \
+		lib/AltErgoLib.cmxa \
+		lib/AltErgoLib.cmxs
+
+# Build the cli/text alt-ergo bin
+bin: gen
+	$(DUNE) build $(DUNE_FLAGS) _build/install/default/bin/alt-ergo
+
+# Build the GUI
+gui: gen
+	$(DUNE) build $(DUNE_FLAGS) _build/install/default/bin/altgr-ergo
+
+# fm-simplex plugin
+fm-simplex:
+	$(DUNE) build $(DUNE_FLAGS) \
+		_build/install/default/share/alt-ergo/plugins/fm-simplex-plugin.cma \
+		_build/install/default/share/alt-ergo/plugins/fm-simplex-plugin.cmxs
+
+# Ab-Why3 plugin
+AB-Why3:
+	$(DUNE) build $(DUNE_FLAGS) \
+		_build/install/default/share/alt-ergo/plugins/AB-Why3-plugin.cma \
+		_build/install/default/share/alt-ergo/plugins/AB-Why3-plugin.cmxs
+
+# Build all plugins
+plugins:
+	$(DUNE) build $(DUNE_FLAGS) \
+		_build/install/default/share/alt-ergo/plugins/fm-simplex-plugin.cma \
+		_build/install/default/share/alt-ergo/plugins/fm-simplex-plugin.cmxs \
+		_build/install/default/share/alt-ergo/plugins/AB-Why3-plugin.cma \
+		_build/install/default/share/alt-ergo/plugins/AB-Why3-plugin.cmxs
+
+# Alias to build all targets using dune
+# Hopefully more efficient than making "all" depend
+# on "lib", "bin" and "gui", since dune can
+# parralelize more
+all: gen
+	$(DUNE) build $(DUNE_FLAGS) @install
+
+# declare these targets as phony to avoid name clashes with existing directories,
+# particularly the "plugins" target
+.PHONY: lib bin gui fm-simplex AB-Why3 plugins all
+
+
+# =====================
+# Non-regressions tests
+# =====================
+
+# Run non-regression tests using the scripts in
+# ../non-regression
+non-regression: all
+	cp _build/install/default/bin/alt-ergo ../non-regression/alt-ergo.opt
+	cd ../non-regression &&  ./non-regression.sh
+	rm ../non-regression/alt-ergo.opt
+
+.PHONY: non-regression
+
+
+# ============
+# Installation
+# ============
+
+# Installation using dune is *NOT* recommended
+# The good way to install alt-ergo is to use the alt-ergo.install
+# file generated by dune, which specifies all files that need to
+# be copied, and where they should be copied
+
+# Use dune to install the lib, bin, and gui
+install: all
+	$(DUNE) install $(DUNE_FLAGS)		\
+		--prefix $(prefix)						\
+		--libdir $(libdir)
+
+# Use dune to uninstall the lib, bin, and gui
+uninstall:
+	$(DUNE) uninstall $(DUNE_FLAGS)	\
+		--prefix $(prefix)						\
+		--libdir $(libdir)
+
+.PHONY: install uninstall
+
+
+# ========================
+# Documentation generation
+# ========================
+
+# Build the documentation
+doc:
+	$(DUNE) build $(DUNE_FLAGS) @doc
+
+# Open the generated html doc in browser
+html: doc
+	xdg-open _build/default/_doc/_html/index.html
+
+.PHONY: doc html
+
+# ========================
+# Configuration generation
+# ========================
+
+# The hand-written configure script is used to query
+# opam (or accept user spec) to set a few variables,
+# and generate the Config module, which stores information
+# about destination directories, including plugin directories
+Makefile.config lib/util/config.ml: configure configure.ml
+	./configure
+
+
+
+# ===============
+# PUBLIC RELEASES
+# ===============
+
+# Get the current commit hash and version number
+COMMIT_ID = $(shell git log -1 | grep commit | cut -d " " -f 2)
+VERSION=$(shell grep "=" lib/util/version.ml | cut -d"=" -f2 | head -n 1)
+
+# Some convenient variables
+PUBLIC_VERSION=$(VERSION)
+PUBLIC_RELEASE=alt-ergo-$(PUBLIC_VERSION)
+PUBLIC_TARGZ=$(PUBLIC_RELEASE).tar.gz
+FILES_DEST=../public-release/$(PUBLIC_RELEASE)/$(PUBLIC_RELEASE)
+
+public-release:
+	rm -rf ../public-release
+	mkdir -p $(FILES_DEST)
+	cp configure $(FILES_DEST)
+	git clean -dfx
+	cp ../License.OCamlPro ../OCamlPro-Non-Commercial-License.txt ../OCamlPro-Non-Commercial-License.pdf ../LGPL-License.txt ../Apache-License-2.0.txt $(FILES_DEST)/
+	cp ../README.md ../LICENSE.md ../COPYING.md $(FILES_DEST)/
+	cp Makefile $(FILES_DEST)/
+	cp INSTALL.md alt-ergo.opam CHANGES $(FILES_DEST)/
+	cp -rf lib tools parsers plugins preludes examples doc $(FILES_DEST)/
+	#echo "let version=\"$(PUBLIC_VERSION)\"" >> $(FILES_DEST)/lib/util/version.ml
+	echo "let release_commit = \"$(COMMIT_ID)\"" >> $(FILES_DEST)/lib/util/version.ml
+	echo "let release_date = \""`LANG=en_US; date`"\"" >> $(FILES_DEST)/lib/util/version.ml
+	cd $(FILES_DEST)/.. && tar cfz $(PUBLIC_TARGZ) $(PUBLIC_RELEASE)
+	rm -rf $(FILES_DEST)
+
+# ==============
+# Cleaning rules
+# ==============
+
+# Cleanup generated files
+generated-clean:
+	rm -rf $(GENERATED)
+
+# Clean build artifacts
+dune-clean:
+	$(DUNE) clean
+
+# Cleanup all makefile-related files
+makefile-distclean:
+	rm -rf Makefile.config
+
+# Clenaup release generated files and dirs
+release-distclean:
+	rm -rf ../public-release
+
+.PHONY: generated-clean dune-clean makefile-distclean release-distclean
+