From 4fadbeb04daf862973103b9b02806f031892aac8 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 18 Jan 2019 18:32:23 -0600 Subject: [PATCH] chore: migrate to dune --- Makefile | 27 ++++++++++++++++----------- README.md | 2 +- dune-project | 2 ++ msat_test.opam | 22 ---------------------- sidekick.opam | 24 +++++++++++------------- src/backend/dune | 12 ++++++++++++ src/backend/jbuild | 14 -------------- src/dimacs/dune | 14 ++++++++++++++ src/dimacs/jbuild | 20 -------------------- src/main/dune | 15 +++++++++++++++ src/main/jbuild | 18 ------------------ src/main_test/dune | 9 +++++++++ src/main_test/jbuild | 10 ---------- src/sat/dune | 11 +++++++++++ src/sat/jbuild | 12 ------------ src/smt/Ast.mli | 1 + src/smt/dune | 9 +++++++++ src/smt/jbuild | 10 ---------- src/smt/th_bool/dune | 9 +++++++++ src/smt/th_bool/jbuild | 10 ---------- src/smtlib/dune | 15 +++++++++++++++ src/smtlib/jbuild | 21 --------------------- src/util/dune | 8 ++++++++ src/util/jbuild | 8 -------- tests/dune | 14 ++++++++++++++ tests/jbuild | 16 ---------------- tests/test_api.ml | 4 ++-- 27 files changed, 149 insertions(+), 188 deletions(-) create mode 100644 dune-project delete mode 100644 msat_test.opam create mode 100644 src/backend/dune delete mode 100644 src/backend/jbuild create mode 100644 src/dimacs/dune delete mode 100644 src/dimacs/jbuild create mode 100644 src/main/dune delete mode 100644 src/main/jbuild create mode 100644 src/main_test/dune delete mode 100644 src/main_test/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/smt/th_bool/dune delete mode 100644 src/smt/th_bool/jbuild create mode 100644 src/smtlib/dune delete mode 100644 src/smtlib/jbuild create mode 100644 src/util/dune delete mode 100644 src/util/jbuild create mode 100644 tests/dune delete mode 100644 tests/jbuild diff --git a/Makefile b/Makefile index ebc66e93..08a91087 100644 --- a/Makefile +++ b/Makefile @@ -7,13 +7,18 @@ J?=3 TIMEOUT?=30 OPTS= -j $(J) +dev: build-dev + +# TODO: repair tests +#dev: build-dev test + build-install: - jbuilder build $(OPTS) @install + @dune build $(OPTS) @install --profile=release build: build-install build-dev: - jbuilder build $(OPTS) --dev + @dune build $(OPTS) enable_log: cd src/core; ln -sf log_real.ml log.ml @@ -22,17 +27,19 @@ disable_log: cd src/core; ln -sf log_dummy.ml log.ml clean: - jbuilder clean + @dune clean + +test: + @dune runtest install: build-install - jbuilder install + @dune install uninstall: - jbuilder uninstall + @dune uninstall doc: - jbuilder build $(OPTS) @doc - + @dune build $(OPTS) @doc reinstall: | uninstall install @@ -48,9 +55,7 @@ reindent: ocp-indent WATCH=build watch: - while find src/ -print0 | xargs -0 inotifywait -e delete_self -e modify ; do \ - echo "============ at `date` ==========" ; \ - make $(WATCH); \ - done + @dune build @install -w + #@dune build @all -w # TODO: once tests pass .PHONY: clean doc all bench install uninstall remove reinstall enable_log disable_log bin test diff --git a/README.md b/README.md index 69933324..584a2ada 100644 --- a/README.md +++ b/README.md @@ -22,7 +22,7 @@ For the development version, use: ### Manual installation -You will need jbuilder. The command is: +You will need dune . The command is: make install diff --git a/dune-project b/dune-project new file mode 100644 index 00000000..977e7d75 --- /dev/null +++ b/dune-project @@ -0,0 +1,2 @@ +(lang dune 1.1) +(using menhir 1.0) diff --git a/msat_test.opam b/msat_test.opam deleted file mode 100644 index 29652a80..00000000 --- a/msat_test.opam +++ /dev/null @@ -1,22 +0,0 @@ -opam-version: "1.2" -name: "msat_test" -license: "Apache" -version: "dev" -author: ["Sylvain Conchon" "Alain Mebsout" "Stephane Lecuyer" "Simon Cruanes" "Guillaume Bury"] -maintainer: ["guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org"] -build: ["jbuilder" "build" "@install" "-p" name] -build-doc: ["jbuilder" "build" "@doc" "-p" name] -depends: [ - "jbuilder" {build} - "dolmen" - "msat" -] -available: [ - ocaml-version >= "4.03.0" -] -tags: [ "sat" "smt" ] -homepage: "https://github.com/Gbury/mSAT" -dev-repo: "https://github.com/Gbury/mSAT.git" -bug-reports: "https://github.com/Gbury/mSAT/issues/" - - diff --git a/sidekick.opam b/sidekick.opam index 635d9133..1198acbf 100644 --- a/sidekick.opam +++ b/sidekick.opam @@ -1,27 +1,25 @@ -opam-version: "1.2" +opam-version: "2.0" name: "sidekick" license: "Apache" +synopsis: "SMT solver based on msat, based on CDCL(T)" version: "dev" -author: ["Simon Cruanes" "Guillaume Bury" "Sylvain Conchon" "Alain Mebsout" "Stephane Lecuyer"] +author: ["Simon Cruanes" "Guillaume Bury"] maintainer: ["simon.cruanes.2007@m4x.org"] -build: ["jbuilder" "build" "@install" "-p" name] -build-doc: ["jbuilder" "build" "@doc" "-p" name] +build: [ + ["dune" "build" "@install" "-p" name "-j" jobs] + ["dune" "build" "@doc" "-p" name] {with-doc} + # ["dune" "runtest" "-p" name] {with-test} +] depends: [ - "ocamlfind" {build} - "jbuilder" {build} + "dune" {build} "containers" "sequence" "zarith" "menhir" -] -depopts: [ - "dolmen" -] -available: [ - ocaml-version >= "4.03.0" + "ocaml" { >= "4.03" } ] tags: [ "sat" "smt" ] homepage: "https://github.com/c-cube/sidekick" -dev-repo: "https://github.com/c-cube/sidekick.git" +dev-repo: "git+https://github.com/c-cube/sidekick.git" bug-reports: "https://github.com/c-cube/sidekick/issues/" diff --git a/src/backend/dune b/src/backend/dune new file mode 100644 index 00000000..dc6531eb --- /dev/null +++ b/src/backend/dune @@ -0,0 +1,12 @@ + +(library + (name Sidekick_backend) + (public_name sidekick.backend) + (synopsis "proof backends for Sidekick") + (libraries sidekick.sat) + (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string + -open Sidekick_sat -open Sidekick_util) + (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 6c703b90..00000000 --- a/src/backend/jbuild +++ /dev/null @@ -1,14 +0,0 @@ -; vim:ft=lisp: - -; main binary -(library - ((name Sidekick_backend) - (public_name sidekick.backend) - (synopsis "proof backends for Sidekick") - (libraries (sidekick.sat)) - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string - -open Sidekick_sat -open Sidekick_util)) - (ocamlopt_flags (:standard -O3 -bin-annot - -unbox-closures -unbox-closures-factor 20)) - )) - diff --git a/src/dimacs/dune b/src/dimacs/dune new file mode 100644 index 00000000..006975c2 --- /dev/null +++ b/src/dimacs/dune @@ -0,0 +1,14 @@ + +; main binary +(library + (name sidekick_dimacs) + (public_name sidekick.dimacs) + (optional) ; only if deps present + (libraries containers sidekick.util) + (flags :standard -w +a-4-42-44-48-50-58-32-60@8) + (ocamlopt_flags :standard -O3 -color always -bin-annot + -unbox-closures -unbox-closures-factor 20) + ) + +(menhir (modules Parser)) +(ocamllex (modules Lexer)) diff --git a/src/dimacs/jbuild b/src/dimacs/jbuild deleted file mode 100644 index 98cb83df..00000000 --- a/src/dimacs/jbuild +++ /dev/null @@ -1,20 +0,0 @@ -; vim:ft=lisp: - -(jbuild_version 1) - -; main binary -(library - ((name sidekick_dimacs) - (public_name sidekick.dimacs) - (optional) ; only if deps present - (libraries (containers sidekick.util)) - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8)) - (ocamlopt_flags (:standard -O3 -color always -bin-annot - -unbox-closures -unbox-closures-factor 20)) - )) - -(menhir - ((modules (Parser)))) - -(ocamllex - (Lexer)) diff --git a/src/main/dune b/src/main/dune new file mode 100644 index 00000000..81365e06 --- /dev/null +++ b/src/main/dune @@ -0,0 +1,15 @@ + +; main binary +(executable + (name main) + (public_name sidekick) + (package sidekick) + (libraries containers sequence result + sidekick.sat sidekick.smt sidekick.smtlib sidekick.backend + sidekick.dimacs) + (flags :standard -w +a-4-42-44-48-50-58-32-60@8 + -safe-string -color always -open Sidekick_util) + (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 83bf9120..00000000 --- a/src/main/jbuild +++ /dev/null @@ -1,18 +0,0 @@ -; vim:ft=lisp: - -(jbuild_version 1) - -; main binary -(executable - ((name main) - (public_name sidekick) - (package sidekick) - (libraries (containers sequence result - sidekick.sat sidekick.smt sidekick.smtlib sidekick.backend - sidekick.dimacs)) - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 - -safe-string -color always -open Sidekick_util)) - (ocamlopt_flags (:standard -O3 -color always - -unbox-closures -unbox-closures-factor 20)) - )) - diff --git a/src/main_test/dune b/src/main_test/dune new file mode 100644 index 00000000..f3ab53b5 --- /dev/null +++ b/src/main_test/dune @@ -0,0 +1,9 @@ + +(executable + (name main_test) + (libraries sidekick_sat sidekick.backend sidekick.th_sat dolmen) + (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Sidekick_sat) + (ocamlopt_flags :standard -O3 -bin-annot + -unbox-closures -unbox-closures-factor 20) + ) + diff --git a/src/main_test/jbuild b/src/main_test/jbuild deleted file mode 100644 index 7ec5a8eb..00000000 --- a/src/main_test/jbuild +++ /dev/null @@ -1,10 +0,0 @@ -; vim:ft=lisp: - -(executable - ((name main_test) - (libraries (sidekick_sat sidekick.backend sidekick.th_sat dolmen)) - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Sidekick_sat)) - (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..eb992a93 --- /dev/null +++ b/src/sat/dune @@ -0,0 +1,11 @@ + +(library + (name Sidekick_sat) + (public_name sidekick.sat) + (synopsis "core SAT solver for Sidekick") + (libraries sidekick.util) + (flags :standard -w +a-4-42-44-48-50-58-32-60@8 + -color always -safe-string -open Sidekick_util) + (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 102c2661..00000000 --- a/src/sat/jbuild +++ /dev/null @@ -1,12 +0,0 @@ -; vim:ft=lisp: - -(library - ((name Sidekick_sat) - (public_name sidekick.sat) - (synopsis "core SAT solver for Sidekick") - (libraries (sidekick.util)) - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 - -color always -safe-string -open Sidekick_util)) - (ocamlopt_flags (:standard -O3 -bin-annot - -unbox-closures -unbox-closures-factor 20)) - )) diff --git a/src/smt/Ast.mli b/src/smt/Ast.mli index 4eb14b9d..778671d3 100644 --- a/src/smt/Ast.mli +++ b/src/smt/Ast.mli @@ -172,6 +172,7 @@ val asserting : term -> term -> term val num_z : Ty.t -> Z.t -> term val num_q : Ty.t -> Q.t -> term val num_str : Ty.t -> string -> term (** parses int + {!num} *) + val arith : Ty.t -> arith_op -> term list -> term (** {2 helpers} *) diff --git a/src/smt/dune b/src/smt/dune new file mode 100644 index 00000000..9ee87676 --- /dev/null +++ b/src/smt/dune @@ -0,0 +1,9 @@ + +(library + (name Sidekick_smt) + (public_name sidekick.smt) + (libraries containers containers.data sequence sidekick.util sidekick.sat zarith) + (flags :standard -w +a-4-44-48-58-60@8 + -color always -safe-string -short-paths -open Sidekick_util) + (ocamlopt_flags :standard -O3 -color always + -unbox-closures -unbox-closures-factor 20)) diff --git a/src/smt/jbuild b/src/smt/jbuild deleted file mode 100644 index 928bcb10..00000000 --- a/src/smt/jbuild +++ /dev/null @@ -1,10 +0,0 @@ -; vim:ft=lisp: - -(library - ((name Sidekick_smt) - (public_name sidekick.smt) - (libraries (containers containers.data sequence sidekick.util sidekick.sat zarith)) - (flags (:standard -w +a-4-44-48-58-60@8 - -color always -safe-string -short-paths -open Sidekick_util)) - (ocamlopt_flags (:standard -O3 -color always - -unbox-closures -unbox-closures-factor 20)))) diff --git a/src/smt/th_bool/dune b/src/smt/th_bool/dune new file mode 100644 index 00000000..93d2e26e --- /dev/null +++ b/src/smt/th_bool/dune @@ -0,0 +1,9 @@ +(library + (name Sidekick_th_bool) + (public_name sidekick.smt.th-bool) + (libraries containers sidekick.smt) + (flags :standard -w +a-4-44-48-58-60@8 + -color always -safe-string -short-paths -open Sidekick_util) + (ocamlopt_flags :standard -O3 -color always + -unbox-closures -unbox-closures-factor 20)) + diff --git a/src/smt/th_bool/jbuild b/src/smt/th_bool/jbuild deleted file mode 100644 index 73c5e85d..00000000 --- a/src/smt/th_bool/jbuild +++ /dev/null @@ -1,10 +0,0 @@ -; vim:ft=lisp: -(library - ((name Sidekick_th_bool) - (public_name sidekick.smt.th_bool) - (libraries (containers sidekick.smt)) - (flags (:standard -w +a-4-44-48-58-60@8 - -color always -safe-string -short-paths -open Sidekick_util)) - (ocamlopt_flags (:standard -O3 -color always - -unbox-closures -unbox-closures-factor 20)))) - diff --git a/src/smtlib/dune b/src/smtlib/dune new file mode 100644 index 00000000..796f7983 --- /dev/null +++ b/src/smtlib/dune @@ -0,0 +1,15 @@ + +(library + (name sidekick_smtlib) + (public_name sidekick.smtlib) + (libraries containers zarith sidekick.smt sidekick.util + sidekick.smt.th-bool sidekick.backend) + (flags :standard -w +a-4-42-44-48-50-58-32-60@8 + -safe-string -color always -open Sidekick_util) + (ocamlopt_flags :standard -O3 -color always -bin-annot + -unbox-closures -unbox-closures-factor 20) + ) + +(menhir (modules Parser)) + +(ocamllex (modules Lexer)) diff --git a/src/smtlib/jbuild b/src/smtlib/jbuild deleted file mode 100644 index 9dbc70d5..00000000 --- a/src/smtlib/jbuild +++ /dev/null @@ -1,21 +0,0 @@ -; vim:ft=lisp: - -(jbuild_version 1) - -; main binary -(library - ((name sidekick_smtlib) - (public_name sidekick.smtlib) - (libraries (containers zarith sidekick.smt sidekick.util - sidekick.smt.th_bool sidekick.backend)) - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 - -safe-string -color always -open Sidekick_util)) - (ocamlopt_flags (:standard -O3 -color always -bin-annot - -unbox-closures -unbox-closures-factor 20)) - )) - -(menhir - ((modules (Parser)))) - -(ocamllex - (Lexer)) diff --git a/src/util/dune b/src/util/dune new file mode 100644 index 00000000..841071c4 --- /dev/null +++ b/src/util/dune @@ -0,0 +1,8 @@ +(library + (name sidekick_util) + (public_name sidekick.util) + (libraries containers sequence) + (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/util/jbuild b/src/util/jbuild deleted file mode 100644 index 66c487fa..00000000 --- a/src/util/jbuild +++ /dev/null @@ -1,8 +0,0 @@ -(library - ((name sidekick_util) - (public_name sidekick.util) - (libraries (containers sequence)) - (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/tests/dune b/tests/dune new file mode 100644 index 00000000..b105a8d4 --- /dev/null +++ b/tests/dune @@ -0,0 +1,14 @@ + +(executable + (name test_api) + (libraries sidekick.backend sidekick.sat sidekick.smt.th-bool) + (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) + ) + +(alias + (name runtest) + (action (run ./test_api.exe))) + + diff --git a/tests/jbuild b/tests/jbuild deleted file mode 100644 index e9038eb9..00000000 --- a/tests/jbuild +++ /dev/null @@ -1,16 +0,0 @@ -; vim:ft=lisp: - -(executable - ((name test_api) - (libraries (dagon cdcl.tseitin cdcl.backend cdcl.sat)) - (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)) - )) - -(alias - ((name runtest) - (deps (test_api.exe)) - (action (run ${<})))) - - diff --git a/tests/test_api.ml b/tests/test_api.ml index 566e3755..4ce25199 100644 --- a/tests/test_api.ml +++ b/tests/test_api.ml @@ -6,9 +6,9 @@ Copyright 2014 Simon Cruanes (* Tests that require the API *) -open CDCL +open Sidekick_sat -module Th = CDCL_sat.Th +module Th = Sidekick_th_sat.Th module F = CDCL_tseitin.Make(Th) let (|>) x f = f x