Gbury · c-cube · Mar 11, 2026 · Mar 11, 2026 · Mar 11, 2026 · Mar 11, 2026
diff --git a/.github/workflows/fmt.yml b/.github/workflows/fmt.yml
@@ -0,0 +1,29 @@
+
+name: format
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+
+jobs:
+  format:
+    name: format
+    strategy:
+      matrix:
+        ocaml-compiler:
+            - '5.3'
+    runs-on: 'ubuntu-latest'
+    steps:
+      - uses: actions/checkout@main
+      - name: Use OCaml ${{ matrix.ocaml-compiler }}
+        uses: ocaml/setup-ocaml@v3
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          dune-cache: true
+          allow-prerelease-opam: true
+
+      - run: opam install ocamlformat.0.27.0
+      - run: opam exec -- make format-check
+
diff --git a/.ocamlformat b/.ocamlformat
@@ -0,0 +1,15 @@
+version = 0.27.0
+profile=conventional
+margin=80
+if-then-else=k-r
+parens-ite=true
+parens-tuple=multi-line-only
+sequence-style=terminator
+type-decl=sparse
+break-cases=toplevel
+cases-exp-indent=2
+field-space=tight-decl
+leading-nested-match-parens=true
+module-item-spacing=compact
+quiet=true
+ocaml-version=4.08.0
diff --git a/Makefile b/Makefile
@@ -31,15 +31,11 @@ doc:
 
 reinstall: | uninstall install
 
-ocp-indent:
-	@which ocp-indent > /dev/null || { \
-	  	echo 'ocp-indent not found; please run `opam install ocp-indent`'; \
-		exit 1 ; \
-	  }
-
-reindent: ocp-indent
-	@find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 echo "reindenting: "
-	@find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 ocp-indent -i
+format:
+	@dune build $(DUNE_OPTS) @fmt --auto-promote
+
+format-check:
+	@dune build $(DUNE_OPTS) @fmt --display=quiet
 
 WATCH=all
 watch:

diff --git a/README.md b/README.md
@@ -1,4 +1,4 @@
-# MSAT  [![Build Status](https://travis-ci.org/Gbury/mSAT.svg?branch=master)](https://travis-ci.org/Gbury/mSAT)
+# MSAT [![Build and Test](https://github.com/Gbury/mSAT/actions/workflows/main.yml/badge.svg)](https://github.com/Gbury/mSAT/actions/workflows/main.yml)
 
 MSAT is an OCaml library that features a modular SAT-solver and some
 extensions (including SMT), derived from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero).

diff --git a/dune b/dune
@@ -1,27 +1,32 @@
-
 (rule
  (alias runtest)
- (deps README.md src/core/msat.cma src/sat/msat_sat.cma (source_tree src))
+ (deps
+  README.md
+  src/core/msat.cma
+  src/sat/msat_sat.cma
+  (source_tree src))
  (locks test)
  (package msat)
- (action (progn
-          (run ocaml-mdx test README.md)
-          (diff? README.md README.md.corrected))))
+ (action
+  (progn
+   (run ocaml-mdx test README.md)
+   (diff? README.md README.md.corrected))))
 
 (env
-  (_
-    (flags
-      :standard
-      -warn-error -a
-      -w +a-4-42-44-48-50-58-32-60-70@8
-      -color always
-      -safe-string
-    )
-    (ocamlopt_flags
-      :standard
-      -O3
-      -bin-annot
-      -unbox-closures -unbox-closures-factor 20
-    )
-  )
-)
+ (_
+  (flags
+   :standard
+   -warn-error
+   -a
+   -w
+   +a-4-42-44-48-50-58-32-60-70@8
+   -color
+   always
+   -safe-string)
+  (ocamlopt_flags
+   :standard
+   -O3
+   -bin-annot
+   -unbox-closures
+   -unbox-closures-factor
+   20)))
diff --git a/dune-project b/dune-project
@@ -1 +1,39 @@
 (lang dune 3.0)
+
+(generate_opam_files true)
+
+(package
+ (name msat)
+ (synopsis "Library containing a SAT solver that can be parametrized by a theory")
+ (version "0.9.1")
+ (license "Apache-2.0")
+ (authors "Simon Cruanes" "Guillaume Bury")
+ (maintainers "guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org")
+ (tags ("sat" "smt" "cdcl" "functor"))
+ (homepage "https://github.com/Gbury/mSAT")
+ (source (github Gbury/mSAT))
+ (bug_reports "https://github.com/Gbury/mSAT/issues/")
+ (depends
+  (ocaml (>= 4.03))
+  (dune (>= 3.0))
+  (iter (>= 1.2))
+  (containers (and :with-test (>= 2.8.1) (< 4.0)))
+  (mdx :with-test)))
+
+(package
+ (name msat-bin)
+ (synopsis "SAT solver binary based on the msat library")
+ (version "0.9.1")
+ (license "Apache-2.0")
+ (authors "Simon Cruanes" "Guillaume Bury")
+ (maintainers "guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org")
+ (tags ("sat"))
+ (homepage "https://github.com/Gbury/mSAT")
+ (source (github Gbury/mSAT))
+ (bug_reports "https://github.com/Gbury/mSAT/issues/")
+ (depends
+  (ocaml (>= 4.03))
+  (dune (>= 3.0))
+  (msat (= :version))
+  (containers (and (>= 2.8.1) (< 4.0)))
+  camlzip))
diff --git a/msat-bin.opam b/msat-bin.opam
@@ -1,23 +1,33 @@
+# This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-name: "msat-bin"
-synopsis: "SAT solver binary based on the msat library"
-license: "Apache-2.0"
 version: "0.9.1"
-author: ["Simon Cruanes" "Guillaume Bury"]
+synopsis: "SAT solver binary based on the msat library"
 maintainer: ["guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org"]
-build: [
-  ["dune" "build" "@install" "-p" name "-j" jobs]
-  #["dune" "runtest" "-p" name "-j" jobs] {with-test}
-]
+authors: ["Simon Cruanes" "Guillaume Bury"]
+license: "Apache-2.0"
+tags: ["sat"]
+homepage: "https://github.com/Gbury/mSAT"
+bug-reports: "https://github.com/Gbury/mSAT/issues/"
 depends: [
-  "ocaml" { >= "4.03" }
-  "dune" { >= "3.0" }
-  "msat" { = version }
-  "containers" { >= "2.8.1" & < "4.0" }
+  "ocaml" {>= "4.03"}
+  "dune" {>= "3.0" & >= "3.0"}
+  "msat" {= version}
+  "containers" {>= "2.8.1" & < "4.0"}
   "camlzip"
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
 ]
-tags: [ "sat" ]
-homepage: "https://github.com/Gbury/mSAT"
 dev-repo: "git+https://github.com/Gbury/mSAT.git"
-bug-reports: "https://github.com/Gbury/mSAT/issues/"
-
diff --git a/msat.opam b/msat.opam
@@ -1,24 +1,34 @@
+# This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-name: "msat"
-synopsis: "Library containing a SAT solver that can be parametrized by a theory"
-license: "Apache-2.0"
 version: "0.9.1"
-author: ["Simon Cruanes" "Guillaume Bury"]
+synopsis:
+  "Library containing a SAT solver that can be parametrized by a theory"
 maintainer: ["guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org"]
-build: [
-  ["dune" "build" "@install" "-p" name "-j" jobs]
-  ["dune" "build" "@doc" "-p" name] {with-doc}
-  ["dune" "runtest" "-p" name] {with-test}
-]
+authors: ["Simon Cruanes" "Guillaume Bury"]
+license: "Apache-2.0"
+tags: ["sat" "smt" "cdcl" "functor"]
+homepage: "https://github.com/Gbury/mSAT"
+bug-reports: "https://github.com/Gbury/mSAT/issues/"
 depends: [
-  "ocaml" { >= "4.03" }
-  "dune" { >= "3.0" }
-  "iter" { >= "1.2" }
-  "containers" {with-test & >= "2.8.1" & < "4.0" }
+  "ocaml" {>= "4.03"}
+  "dune" {>= "3.0" & >= "3.0"}
+  "iter" {>= "1.2"}
+  "containers" {with-test & >= "2.8.1" & < "4.0"}
   "mdx" {with-test}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
 ]
-tags: [ "sat" "smt" "cdcl" "functor" ]
-homepage: "https://github.com/Gbury/mSAT"
 dev-repo: "git+https://github.com/Gbury/mSAT.git"
-bug-reports: "https://github.com/Gbury/mSAT/issues/"
-
diff --git a/src/backend/Backend_intf.ml b/src/backend/Backend_intf.ml
@@ -6,22 +6,18 @@ Copyright 2014 Simon Cruanes
 
 (** Backend interface
 
-    This modules defines the interface of the modules providing
-    export of proofs.
-*)
+    This modules defines the interface of the modules providing export of
+    proofs. *)
 
 module type S = sig
   (** Proof exporting
 
-      Currently, exporting a proof means printing it into a file
-      according to the conventions of a given format.
-  *)
+      Currently, exporting a proof means printing it into a file according to
+      the conventions of a given format. *)
 
   type t
   (** The type of proofs. *)
 
   val pp : Format.formatter -> t -> unit
   (** A function for printing proofs in the desired format. *)
-
 end
-