From 175ba9c7f0bdf257a5e3e60ed7f8a2c0e7eff2b3 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Thu, 26 Oct 2023 15:22:41 +0200 Subject: [PATCH] Mention how to compile exercises with make --- README.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 0233f9e..7464344 100644 --- a/README.md +++ b/README.md @@ -21,7 +21,7 @@ Now proceed to install the dependencies: ``` cd semantics-2023 -# We create a new "switch" to install the dependencies in. Switches are independent +# We create a new "switch" to install the dependencies in. Switches are independent # installation prefixes with their own set of installed packages. opam switch create semantics ocaml-base-compiler.4.14.1 # We tell opam to automatically enable the switch `semantics` in this directory @@ -49,6 +49,8 @@ make -j4 ``` **IMPORTANT:** You will have to compile to interactively do proofs. You will have to recompile if the dependencies of the file your editing change. +By default, the exercise proofs won't be compiled by the above command. +You can still work on them interactively, but if you want `make` to check them, you will need to append their path to the `_CoqProject` file. ## Editing the Coq code To edit the Coq code and complete the exercises, you will need an editor. We recommend you use [CoqIDE](https://coq.inria.fr/refman/practical-tools/coqide.html) or [VsCoq](https://github.com/coq-community/vscoq) ([VSCode](https://code.visualstudio.com/)).