From ed64e6b69d172d51dc94102c9e5beea7ff0d9a3d Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 16 Feb 2019 17:51:14 -0600
Subject: [PATCH] chore: try to fix the mdx test; cleanup makefile

---
 Makefile  | 18 ++----------------
 README.md |  6 ++++--
 dune      |  3 ++-
 3 files changed, 8 insertions(+), 19 deletions(-)

diff --git a/Makefile b/Makefile
index a8967cda..c8f09a05 100644
--- a/Makefile
+++ b/Makefile
@@ -1,17 +1,9 @@
 # copyright (c) 2014, guillaume bury
 # copyright (c) 2017, simon cruanes
 
-BIN=main.native
-TEST_BIN=tests/test_api.native
-
-NAME=msat
 J?=3
-TIMEOUT?=30
-TARGETS=src/bin/main.exe
 OPTS= -j $(J)
 
-LIB=$(addprefix $(NAME), .cma .cmxa .cmxs)
-
 build:
 	@dune build $(OPTS) @install --profile=release
 
@@ -20,16 +12,10 @@ dev: build-dev test
 build-dev:
 	@dune build $(OPTS) @install
 
-test:
+test: build-dev
 	@echo "run tests…"
 	@OCAMLRUNPARAM=b dune runtest --force --no-buffer
 
-enable_log:
-	cd src/core; ln -sf log_real.ml log.ml
-
-disable_log:
-	cd src/core; ln -sf log_dummy.ml log.ml
-
 clean:
 	@dune clean
 
@@ -59,4 +45,4 @@ WATCH=all
 watch:
 	@dune build @all -w
 
-.PHONY: clean doc all bench install uninstall remove reinstall enable_log disable_log bin test
+.PHONY: clean doc all bench install uninstall remove reinstall bin test
diff --git a/README.md b/README.md
index 4dc23a6d..a35b3d59 100644
--- a/README.md
+++ b/README.md
@@ -56,6 +56,7 @@ using the `msat.sat` library. It can be loaded
 as shown in the following code :
 
 ```ocaml
+# #require "msat";;
 # #require "msat.sat";;
 # #print_depth 0;; (* do not print details *)
 ```
@@ -147,7 +148,8 @@ it into clauses using `make_cnf`:
 The directory `src/sudoku/` contains a simple Sudoku solver that
 uses the interface `Msat.Make_cdcl_t`.
 In essence, it implements the logical theory `CDCL(Sudoku)`.
-The script `sudoku_solve.sh` compiles and runs the solver.
+The script `sudoku_solve.sh` compiles and runs the solver,
+as does `dune exec src/sudoku/sudoku_solve.exe`.
 
 It's able to parse sudoku grids denoted as 81 integers
 (see `tests/sudoku/sudoku.txt` for example).
@@ -156,7 +158,7 @@ Here is a sample grid and the output from the solver (in roughly .5s):
 
 ```sh
 $ echo '..............3.85..1.2.......5.7.....4...1...9.......5......73..2.1........4...9' > sudoku.txt
-$ ./sudoku_solve.sh sudoku.txt
+$ dune exec src/sudoku/sudoku_solve.exe -- sudoku.txt
 ...
 #########################
 solve grid:
diff --git a/dune b/dune
index 4331a5ff..18913452 100644
--- a/dune
+++ b/dune
@@ -1,7 +1,8 @@
 
 (alias
  (name runtest)
- (deps README.md ./sudoku_solve.sh)
+ (deps README.md)
+ (locks test)
  (action (progn
           (run mdx test README.md)
           (diff? README.md README.md.corrected))))