clojure.test integration: one assertion carrying the whole failure, and the failing trace written where a regression test can replay it.
clojure.test integration: one assertion carrying the whole failure, and the failing trace written where a regression test can replay it.
(check driver opts)Run core/check and assert the result, so a divergence fails the enclosing
deftest with the step, action, handler var, diff and reproduce line as its
message. Returns the result map, so a test may assert further on it.
A divergence also saves the failing trace with save-failure!, since that
file is what turns a random failure into a committed regression test.
:save-failure, in opts or in the driver, controls it: true (the
default) writes to default-failure-dir, a string writes to that directory,
false writes nothing.
Run `core/check` and assert the result, so a divergence fails the enclosing `deftest` with the step, action, handler var, diff and reproduce line as its message. Returns the result map, so a test may assert further on it. A divergence also saves the failing trace with `save-failure!`, since that file is what turns a random failure into a committed regression test. `:save-failure`, in `opts` or in the driver, controls it: `true` (the default) writes to `default-failure-dir`, a string writes to that directory, `false` writes nothing.
(check-run driver opts)Run core/check-run and assert the result, exactly as check does — one
assertion, and the trace saved on divergence. :test names the scripted
run in the spec.
Run `core/check-run` and assert the result, exactly as `check` does — one assertion, and the trace saved on divergence. `:test` names the scripted `run` in the spec.
Where a failing trace lands unless :save-failure names somewhere else. A
drop zone, not an archive: gitignore it, and promote the traces worth keeping
into test-resources/quint-connect/ by hand, so a failing run never dirties
the repository on its own.
Where a failing trace lands unless `:save-failure` names somewhere else. A drop zone, not an archive: gitignore it, and promote the traces worth keeping into `test-resources/quint-connect/` by hand, so a failing run never dirties the repository on its own.
(replay-file driver path)Run core/replay-file and assert the result, so a trace committed by
save-failure! is a one-line regression test. Needs no Quint. Returns the
result map.
Run `core/replay-file` and assert the result, so a trace committed by `save-failure!` is a one-line regression test. Needs no Quint. Returns the result map.
(save-failure! result)(save-failure! result {:keys [dir] fname :name})Write the failing trace of a core/check result to disk, and return the
result with the path added at [:failure :saved]. This is what gives the
trace a permanent home: the temporary directory Quint wrote it to is deleted
before check returns.
Takes the result and an options map:
:dir directory to write into, default default-failure-dir
:name file name, default <spec>-seed<seed>-trace<i>.itf.json
The default name is deterministic on purpose — the same seed and trace index
is the same spec trace, so re-running a failure rewrites one file instead of
piling up near-copies. Quint's own bytes are written verbatim. An :ok?
result is returned unchanged and nothing is written.
Throws ex-info with :quint/error :save-failed if the file cannot be
written: an unwritable directory is a mistake to fix, not something to
discover as an IOException in place of the divergence that caused it.
Write the failing trace of a `core/check` result to disk, and return the result with the path added at `[:failure :saved]`. This is what gives the trace a permanent home: the temporary directory Quint wrote it to is deleted before `check` returns. Takes the result and an options map: :dir directory to write into, default `default-failure-dir` :name file name, default `<spec>-seed<seed>-trace<i>.itf.json` The default name is deterministic on purpose — the same seed and trace index is the same spec trace, so re-running a failure rewrites one file instead of piling up near-copies. Quint's own bytes are written verbatim. An `:ok?` result is returned unchanged and nothing is written. Throws `ex-info` with `:quint/error` `:save-failed` if the file cannot be written: an unwritable directory is a mistake to fix, not something to discover as an `IOException` in place of the divergence that caused it.
(verify driver opts)Run core/verify and assert the result, so a violated invariant fails the
enclosing deftest with the counterexample and, when the implementation
disagrees with it, the diverging step. :invariant names a val in the
spec.
The counterexample is saved exactly as a divergence is, under
<spec>-<invariant>-counterexample.itf.json — and it is saved even when the
implementation matched it, because the trace that violated the invariant is
worth keeping either way.
Slow: this runs Apalache, which is downloaded on first use and can take minutes. Tag the deftest so it stays out of the fast suite.
Run `core/verify` and assert the result, so a violated invariant fails the enclosing `deftest` with the counterexample and, when the implementation disagrees with it, the diverging step. `:invariant` names a `val` in the spec. The counterexample is saved exactly as a divergence is, under `<spec>-<invariant>-counterexample.itf.json` — and it is saved even when the implementation matched it, because the trace that violated the invariant is worth keeping either way. Slow: this runs Apalache, which is downloaded on first use and can take minutes. Tag the deftest so it stays out of the fast suite.
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |