**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/)).
