From 644f9457aa23cebe20f1db673f0d78a175cbf8b3 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 14 Jun 2022 13:35:55 +0200
Subject: [PATCH] [doc] Update README.md.
---
README.md | 44 +++++++++++++++++++++-----------------------
1 file changed, 21 insertions(+), 23 deletions(-)
diff --git a/README.md b/README.md
index 028da13d..f170a120 100644
--- a/README.md
+++ b/README.md
@@ -9,28 +9,26 @@ TBD
### How to add a solver
Make sure the solver is installed in your system. Typically, the path to its
-binary should appear in the environment variable `$PATH`. Then,
-
-1. **Create a `solver.drv` in `config/drivers/`.**
-A driver is a series of `whyml` modules describing the theories
-the solver is able to understand as provided by `Why3`.
-Directives for letting `Why3` interpret the solver outputs should
-also be provided here.
-
-2. **Add a new record in `config/caisar-detection-data.conf`.**
-The name of the solver executable should be provided , as well as a
-command-line template that `Why3` will use for executing the solver.
-Such a template may specify several `Why3` built-in identifiers:
-
+binary should appear in the environment variable `PATH`. Then,
+
+1. **Create a `solver.drv` in `config/drivers/`.** A driver is a series of
+`whyml` modules describing the theories the solver is able to understand as
+provided by `Why3`. Directives for letting `Why3` interpret the solver outputs
+should also be provided here.
+
+2. **Add a new record in `config/caisar-detection-data.conf`.** The name of the
+solver executable should be provided , as well as a command-line template that
+`Why3` will use for executing the solver. Such a template may specify several
+`Why3` built-in identifiers:
+
* %e stands for the executable
* %f stands for a file to pass to the executable
-
-Other ustom identifiers have been added: %{nnet-onnx} and %{svm}.
-These identifiers are used for providing the solver with potential
-`{nnet, onnx}` and `svm` model filenames, respectively.
-
-3. **Write a `Why3` printer.**
-The solver should be recognized by `CAISAR` by now. However, a printer
-for the solver may be needed for transforming `Why3` specifications into
-something the solver can understand. Printers should be placed in
-`src/printers/`.
+
+Other custom identifiers have been added: %{nnet-onnx} and %{svm}. These
+identifiers are used for providing the solver with potential `{nnet, onnx}` and
+`svm` model filenames, respectively.
+
+3. **Write a `Why3` printer.** The solver should be recognized by `CAISAR` by
+now. However, a printer for the solver may be needed for transforming `Why3`
+specifications into something the solver can understand. Printers should be
+placed in `src/printers/`.
--
GitLab