From 2fb51d808206348365417e2af5ec76c3343658ef Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 18 Jan 2019 18:01:09 -0600 Subject: [PATCH] chore: move to dune --- Makefile | 21 +++++++++------------ dune-project | 1 + src/backend/dune | 10 ++++++++++ src/backend/jbuild | 13 ------------- src/core/dune | 9 +++++++++ src/core/jbuild | 11 ----------- src/main/dune | 11 +++++++++++ src/main/jbuild | 13 ------------- src/mcsat/dune | 12 ++++++++++++ src/mcsat/jbuild | 13 ------------- src/sat/dune | 12 ++++++++++++ src/sat/jbuild | 13 ------------- src/smt/dune | 12 ++++++++++++ src/smt/jbuild | 13 ------------- src/solver/dune | 11 +++++++++++ src/solver/jbuild | 12 ------------ src/tseitin/dune | 10 ++++++++++ src/tseitin/jbuild | 12 ------------ 18 files changed, 97 insertions(+), 112 deletions(-) create mode 100644 dune-project create mode 100644 src/backend/dune delete mode 100644 src/backend/jbuild create mode 100644 src/core/dune delete mode 100644 src/core/jbuild create mode 100644 src/main/dune delete mode 100644 src/main/jbuild create mode 100644 src/mcsat/dune delete mode 100644 src/mcsat/jbuild create mode 100644 src/sat/dune delete mode 100644 src/sat/jbuild create mode 100644 src/smt/dune delete mode 100644 src/smt/jbuild create mode 100644 src/solver/dune delete mode 100644 src/solver/jbuild create mode 100644 src/tseitin/dune delete mode 100644 src/tseitin/jbuild diff --git a/Makefile b/Makefile index f789c987..e5d6c0a7 100644 --- a/Makefile +++ b/Makefile @@ -12,17 +12,17 @@ OPTS= -j $(J) LIB=$(addprefix $(NAME), .cma .cmxa .cmxs) -all: build-dev test +dev: build-dev test build: - jbuilder build $(OPTS) @install + @dune build $(OPTS) @install --profile=release build-dev: - jbuilder build $(OPTS) @install --dev + @dune build $(OPTS) @install test: build @echo "run API tests…" - jbuilder runtest + @dune runtest @echo "run benchmarks…" # @/usr/bin/time -f "%e" ./tests/run smt @/usr/bin/time -f "%e" ./tests/run mcsat @@ -34,16 +34,16 @@ disable_log: cd src/core; ln -sf log_dummy.ml log.ml clean: - jbuilder clean + @dune clean install: build-install - jbuilder install + @dune install uninstall: - jbuilder uninstall + @dune uninstall doc: - jbuilder build $(OPTS) @doc + @dune build $(OPTS) @doc reinstall: | uninstall install @@ -60,9 +60,6 @@ reindent: ocp-indent WATCH=all watch: - while find src/ tests/ -print0 | xargs -0 inotifywait -e delete_self -e modify ; do \ - echo "============ at `date` ==========" ; \ - make $(WATCH); \ - done + @dune build @all -w .PHONY: clean doc all bench install uninstall remove reinstall enable_log disable_log bin test diff --git a/dune-project b/dune-project new file mode 100644 index 00000000..7655de07 --- /dev/null +++ b/dune-project @@ -0,0 +1 @@ +(lang dune 1.1) diff --git a/src/backend/dune b/src/backend/dune new file mode 100644 index 00000000..d9a6c6de --- /dev/null +++ b/src/backend/dune @@ -0,0 +1,10 @@ +(library + (name msat_backend) + (public_name msat.backend) + (synopsis "proof backends for msat") + (libraries msat) + (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string) + (ocamlopt_flags :standard -O3 -bin-annot + -unbox-closures -unbox-closures-factor 20) + ) + diff --git a/src/backend/jbuild b/src/backend/jbuild deleted file mode 100644 index aa2609ff..00000000 --- a/src/backend/jbuild +++ /dev/null @@ -1,13 +0,0 @@ -; vim:ft=lisp: - -; main binary -(library - ((name msat_backend) - (public_name msat.backend) - (synopsis "proof backends for msat") - (libraries (msat)) - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)) - (ocamlopt_flags (:standard -O3 -bin-annot - -unbox-closures -unbox-closures-factor 20)) - )) - diff --git a/src/core/dune b/src/core/dune new file mode 100644 index 00000000..c72f5475 --- /dev/null +++ b/src/core/dune @@ -0,0 +1,9 @@ + +(library + (name msat) + (public_name msat) + (synopsis "core data structures and algorithms for msat") + (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string) + (ocamlopt_flags :standard -O3 -bin-annot + -unbox-closures -unbox-closures-factor 20) + ) diff --git a/src/core/jbuild b/src/core/jbuild deleted file mode 100644 index 22ef52fb..00000000 --- a/src/core/jbuild +++ /dev/null @@ -1,11 +0,0 @@ -; vim:ft=lisp: - -(library - ((name msat) - (public_name msat) - (synopsis "core data structures and algorithms for msat") - (libraries ()) - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)) - (ocamlopt_flags (:standard -O3 -bin-annot - -unbox-closures -unbox-closures-factor 20)) - )) diff --git a/src/main/dune b/src/main/dune new file mode 100644 index 00000000..2c6fd9e9 --- /dev/null +++ b/src/main/dune @@ -0,0 +1,11 @@ + +; main binary +(executable + (name main) + (public_name msat_solver) + (package minismt) + (libraries msat msat.backend minismt.sat minismt.smt minismt.mcsat dolmen) + (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string) + (ocamlopt_flags :standard -O3 -color always + -unbox-closures -unbox-closures-factor 20) + ) diff --git a/src/main/jbuild b/src/main/jbuild deleted file mode 100644 index 8de51a2e..00000000 --- a/src/main/jbuild +++ /dev/null @@ -1,13 +0,0 @@ - -; vim:ft=lisp: - -; main binary -(executable - ((name main) - (public_name msat_solver) - (package minismt) - (libraries (msat msat.backend minismt.sat minismt.smt minismt.mcsat dolmen)) - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)) - (ocamlopt_flags (:standard -O3 -color always - -unbox-closures -unbox-closures-factor 20)) - )) diff --git a/src/mcsat/dune b/src/mcsat/dune new file mode 100644 index 00000000..b3556847 --- /dev/null +++ b/src/mcsat/dune @@ -0,0 +1,12 @@ + +(library + (name minismt_mcsat) + (public_name minismt.mcsat) + (libraries msat minismt minismt.smt) + (synopsis "mcsat interface") + (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat) + (ocamlopt_flags :standard -O3 -bin-annot + -unbox-closures -unbox-closures-factor 20) + ) + + diff --git a/src/mcsat/jbuild b/src/mcsat/jbuild deleted file mode 100644 index 692db5f8..00000000 --- a/src/mcsat/jbuild +++ /dev/null @@ -1,13 +0,0 @@ -; vim:ft=lisp: - -(library - ((name minismt_mcsat) - (public_name minismt.mcsat) - (libraries (msat minismt minismt.smt)) - (synopsis "mcsat interface") - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)) - (ocamlopt_flags (:standard -O3 -bin-annot - -unbox-closures -unbox-closures-factor 20)) - )) - - diff --git a/src/sat/dune b/src/sat/dune new file mode 100644 index 00000000..650ba4c3 --- /dev/null +++ b/src/sat/dune @@ -0,0 +1,12 @@ + +(library + (name minismt_sat) + (public_name minismt.sat) + (libraries msat msat.tseitin minismt dolmen) + (synopsis "sat interface") + (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat) + (ocamlopt_flags :standard -O3 -bin-annot + -unbox-closures -unbox-closures-factor 20) + ) + + diff --git a/src/sat/jbuild b/src/sat/jbuild deleted file mode 100644 index 82068bfb..00000000 --- a/src/sat/jbuild +++ /dev/null @@ -1,13 +0,0 @@ -; vim:ft=lisp: - -(library - ((name minismt_sat) - (public_name minismt.sat) - (libraries (msat msat.tseitin minismt dolmen)) - (synopsis "sat interface") - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)) - (ocamlopt_flags (:standard -O3 -bin-annot - -unbox-closures -unbox-closures-factor 20)) - )) - - diff --git a/src/smt/dune b/src/smt/dune new file mode 100644 index 00000000..c2bd637f --- /dev/null +++ b/src/smt/dune @@ -0,0 +1,12 @@ + +(library + (name minismt_smt) + (public_name minismt.smt) + (libraries msat minismt msat.tseitin dolmen) + (synopsis "smt interface") + (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat) + (ocamlopt_flags :standard -O3 -bin-annot + -unbox-closures -unbox-closures-factor 20) + ) + + diff --git a/src/smt/jbuild b/src/smt/jbuild deleted file mode 100644 index 9999f849..00000000 --- a/src/smt/jbuild +++ /dev/null @@ -1,13 +0,0 @@ -; vim:ft=lisp: - -(library - ((name minismt_smt) - (public_name minismt.smt) - (libraries (msat minismt msat.tseitin dolmen)) - (synopsis "smt interface") - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)) - (ocamlopt_flags (:standard -O3 -bin-annot - -unbox-closures -unbox-closures-factor 20)) - )) - - diff --git a/src/solver/dune b/src/solver/dune new file mode 100644 index 00000000..31c93320 --- /dev/null +++ b/src/solver/dune @@ -0,0 +1,11 @@ + +(library + (name minismt) + (public_name minismt) + (libraries msat dolmen) + (synopsis "minismt") + (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat) + (ocamlopt_flags :standard -O3 -bin-annot + -unbox-closures -unbox-closures-factor 20) + ) + diff --git a/src/solver/jbuild b/src/solver/jbuild deleted file mode 100644 index f3176323..00000000 --- a/src/solver/jbuild +++ /dev/null @@ -1,12 +0,0 @@ -; vim:ft=lisp: - -(library - ((name minismt) - (public_name minismt) - (libraries (msat dolmen)) - (synopsis "minismt") - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)) - (ocamlopt_flags (:standard -O3 -bin-annot - -unbox-closures -unbox-closures-factor 20)) - )) - diff --git a/src/tseitin/dune b/src/tseitin/dune new file mode 100644 index 00000000..a9057a53 --- /dev/null +++ b/src/tseitin/dune @@ -0,0 +1,10 @@ + +(library + (name msat_tseitin) + (public_name msat.tseitin) + (synopsis "Tseitin transformation for msat") + (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string) + (ocamlopt_flags :standard -O3 -bin-annot + -unbox-closures -unbox-closures-factor 20) + ) + diff --git a/src/tseitin/jbuild b/src/tseitin/jbuild deleted file mode 100644 index e70bd0e7..00000000 --- a/src/tseitin/jbuild +++ /dev/null @@ -1,12 +0,0 @@ -; vim:ft=lisp: - -(library - ((name msat_tseitin) - (public_name msat.tseitin) - (synopsis "Tseitin transformation for msat") - (libraries ()) - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)) - (ocamlopt_flags (:standard -O3 -bin-annot - -unbox-closures -unbox-closures-factor 20)) - )) -