mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-07 11:45:41 -05:00
chore: move to dune
This commit is contained in:
parent
cba9f9592d
commit
2fb51d8082
18 changed files with 97 additions and 112 deletions
21
Makefile
21
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
|
||||
|
|
|
|||
1
dune-project
Normal file
1
dune-project
Normal file
|
|
@ -0,0 +1 @@
|
|||
(lang dune 1.1)
|
||||
10
src/backend/dune
Normal file
10
src/backend/dune
Normal file
|
|
@ -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)
|
||||
)
|
||||
|
||||
|
|
@ -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))
|
||||
))
|
||||
|
||||
9
src/core/dune
Normal file
9
src/core/dune
Normal file
|
|
@ -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)
|
||||
)
|
||||
|
|
@ -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))
|
||||
))
|
||||
11
src/main/dune
Normal file
11
src/main/dune
Normal file
|
|
@ -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)
|
||||
)
|
||||
|
|
@ -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))
|
||||
))
|
||||
12
src/mcsat/dune
Normal file
12
src/mcsat/dune
Normal file
|
|
@ -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)
|
||||
)
|
||||
|
||||
|
||||
|
|
@ -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))
|
||||
))
|
||||
|
||||
|
||||
12
src/sat/dune
Normal file
12
src/sat/dune
Normal file
|
|
@ -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)
|
||||
)
|
||||
|
||||
|
||||
|
|
@ -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))
|
||||
))
|
||||
|
||||
|
||||
12
src/smt/dune
Normal file
12
src/smt/dune
Normal file
|
|
@ -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)
|
||||
)
|
||||
|
||||
|
||||
|
|
@ -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))
|
||||
))
|
||||
|
||||
|
||||
11
src/solver/dune
Normal file
11
src/solver/dune
Normal file
|
|
@ -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)
|
||||
)
|
||||
|
||||
|
|
@ -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))
|
||||
))
|
||||
|
||||
10
src/tseitin/dune
Normal file
10
src/tseitin/dune
Normal file
|
|
@ -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)
|
||||
)
|
||||
|
||||
|
|
@ -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))
|
||||
))
|
||||
|
||||
Loading…
Add table
Reference in a new issue