chore: migrate to dune

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 \
+	@dune build @install -w
-		echo "============ at `date` ==========" ; \
+	#@dune build @all -w # TODO: once tests pass
-		make $(WATCH); \
-	done
 
 .PHONY: clean doc all bench install uninstall remove reinstall enable_log disable_log bin test

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
 

dune-project

@@ -0,0 +1,2 @@
+(lang dune 1.1)
+(using menhir 1.0)

msat_test.opam

@@ -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/"
-
-

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: [
-build-doc: ["jbuilder" "build" "@doc" "-p" name]
+  ["dune" "build" "@install" "-p" name "-j" jobs]
+  ["dune" "build" "@doc" "-p" name] {with-doc}
+  # ["dune" "runtest" "-p" name] {with-test}
+]
 depends: [
-  "ocamlfind" {build}
+  "dune" {build}
-  "jbuilder" {build}
   "containers"
   "sequence"
   "zarith"
   "menhir"
-]
+  "ocaml" { >= "4.03" } 
-depopts: [
-  "dolmen"
-]
-available: [
-  ocaml-version >= "4.03.0"
 ]
 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/"
 

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)
+  )
+

src/backend/jbuild

@@ -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))
-  ))
-

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))

src/dimacs/jbuild

@@ -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))

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)
+  )
+

src/main/jbuild

@@ -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))
-  ))
-

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)
+  )
+

src/main_test/jbuild

@@ -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))
-  ))
-

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)
+  )

src/sat/jbuild

@@ -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))
-  ))

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} *)

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))

src/smt/jbuild

@@ -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))))

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))
+

src/smt/th_bool/jbuild

@@ -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))))
-

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))

src/smtlib/jbuild

@@ -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))

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)
+  )

src/util/jbuild

@@ -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))
-   ))

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)))
+
+

tests/jbuild

@@ -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 ${<}))))
-
-

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