Skip to content

Commit 3045428

Browse files
committed
Improve error message on missing solver (#424)
1 parent 5a720c9 commit 3045428

File tree

2 files changed

+25
-8
lines changed

2 files changed

+25
-8
lines changed

src/smtml/mappings.nop.ml

Lines changed: 17 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -389,14 +389,24 @@ module Nop = struct
389389
end
390390

391391
let die () =
392+
let error_s = Fmt.styled `Red (Fmt.styled `Bold Fmt.string) in
393+
let solver_s = Fmt.styled `Yellow Fmt.string in
394+
let cmd_s = Fmt.styled `Cyan Fmt.string in
395+
let link_s = Fmt.styled `Underline (Fmt.styled `Blue Fmt.string) in
396+
let note_s = Fmt.styled `Bold Fmt.string in
392397
Fmt.epr
393-
"The %s solver is not installed. You must install it through opam with \
394-
the command `opam install %s`. You could also try to use another \
395-
solver (have a look at the supported solvers here: \
396-
https://github.com/formalsec/smtml?tab=readme-ov-file#supported-solvers). \
397-
Note that installing the solver with your system package manager is \
398-
not enough, you must install it through opam."
399-
solver_name solver_package;
398+
"%a%a: The %a solver is not installed.\n\n\
399+
To install it, run the following command: %a\n\n\
400+
Alternatively, you can use a different solver.\n\
401+
See supported solvers here: %a\n\n\
402+
%a: Installing the solver with your system package manager is not \
403+
enough, you must install it through opam.\n"
404+
Fmt.set_style_renderer `Ansi_tty error_s "error" solver_s solver_name
405+
cmd_s
406+
(Fmt.str "opam install %s" solver_package)
407+
link_s "https://github.com/formalsec/smtml#supported-solvers" note_s
408+
"Note";
409+
400410
exit 1
401411

402412
module Solver = struct

test/cli/regression/test_issue_183.t

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,5 +4,12 @@ Test solver not installed error message:
44
> (assert (= x 1))
55
> (check-sat)
66
> EOF
7-
The Colibri2 solver is not installed. You must install it through opam with the command `opam install colibri2`. You could also try to use another solver (have a look at the supported solvers here: https://github.com/formalsec/smtml?tab=readme-ov-file#supported-solvers). Note that installing the solver with your system package manager is not enough, you must install it through opam.
7+
error: The Colibri2 solver is not installed.
8+
9+
To install it, run the following command: opam install colibri2
10+
11+
Alternatively, you can use a different solver.
12+
See supported solvers here: https://github.com/formalsec/smtml#supported-solvers
13+
14+
Note: Installing the solver with your system package manager is not enough, you must install it through opam.
815
[1]

0 commit comments

Comments
 (0)