= Nunchaku :toc: macro :source-highlighter: pygments
image::https://github.com/nunchaku-inria/nunchaku/workflows/build/badge.svg[Build status on github]
A counter-example finder for higher-order logic, designed to be used from various proof assistants. A spiritual successor to Nitpick. Documentation at https://nunchaku-inria.github.io/nunchaku/.
Nunchaku requires http://cvc4.cs.nyu.edu/web/[CVC4] 1.5 or later. Alternatively, it can use other backends:
We have https://github.com/nunchaku-inria/nunchaku-problems[a set of problems] for tests and regressions, that can also be helpful to grasp the input syntax and see how to use the constructs of Nunchaku.
toc::[]
== Basic Usage
After installing nunchaku (see <
A list of options can be obtained by calling nunchaku --help
. A few
particularly useful options are:
--help
for listing options.--timeout <n>
(or -t <n>
): maximal amount of seconds before returning "unknown"j <n>
for controlling the number of backend solvers active at the
same time.--solvers s1,s2
(or -s s1,s2
) for using only the listed solvers.--debug <n>
(where n=1,2,…5
) to enable debug printing.
The maximal verbosity level is 5, and it is very verbose. Consider
using nunchaku --debug 5 foo.nun | less -R
to not drown
in pages of text.--pp-all
(and each --pp-<pass>
) for printing the problem
after each transformation.-nc
to disable colored output if your terminal does not support it..== Contact
There is a dedicated mailing list at nunchaku-users@lists.gforge.inria.fr (https://lists.gforge.inria.fr/mailman/listinfo/nunchaku-users[register]). The https://github.com/nunchaku-inria/nunchaku/issues[issue tracker] can be used for reporting bugs.
== Documentation
See the website https://nunchaku-inria.github.io/nunchaku/ and link:/docs/index.adoc[the documentation sources].
[[install]] == Build/Install
To build Nunchaku, there are several ways.
=== Released versions
Releases can be found on https://gforge.inria.fr/projects/nunchaku .
=== Opam
The easiest way is to use http://opam.ocaml.org/[opam], the package manager for
OCaml. Once opam is installed (don't forget to run eval
opam config env``
when you want to use opam), the following should suffice:
opam pin add -k git nunchaku https://github.com/nunchaku-inria/nunchaku.git#master
then opam should propose to install nunchaku and its dependencies. To upgrade:
opam update
opam upgrade nunchaku
Note that the binary is called 'nunchaku.native' until is it installed.
=== Manually
You need to install the dependencies first, namely:
Once you have entered the source directory, type:
make
== License
Free software under the BSD license. See file 'LICENSE' for more details.
[[supported-formats]] == Input/Output/Solvers
Supported input formats are:
.nun
).p
).smt2
)Supported solver backends:
opam install smbc
)=== How to make a release
udpate the repository itself
nunchaku.opam
to change version numbergit commit --amend
to update the commitgit tag 0.42
git push origin stable --tags
make an archive:
git archive --prefix=nunchaku/ 0.42 -o nunchaku-0.42.tar.gz
git archive --prefix=nunchaku/ 0.42 -o nunchaku-0.42.zip
upload the archive on gforge, write some release notes, send a mail.