From ef2c7a04c54b9ce0c8851a41729cbaaa3b50de38 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Tue, 6 Feb 2024 16:59:57 +0100 Subject: [PATCH] update README (fix #1046) --- README.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 5e32021f9..4204a7dbb 100644 --- a/README.md +++ b/README.md @@ -91,12 +91,14 @@ You can get the sources using `git` as follows: git clone https://github.com/Deducteam/lambdapi.git ``` -Dependencies are described in `lambdapi.opam`. The command `why3 config detect` -must be run for Why3 to know the available provers. +Dependencies are described in `lambdapi.opam`. The command `why3 +config detect` must be run for Why3 to know the available provers for +the `why3` tactic. Using Opam, a suitable OCaml environment can be setup as follows: ```bash -opam install dune bindlib timed sedlex menhir pratter yojson cmdliner why3 alcotest alt-ergo odoc +cd lambdapi +opam install . why3 config detect ```