diff options
Diffstat (limited to 'dev/doc/setup.txt')
| -rw-r--r-- | dev/doc/setup.txt | 40 |
1 files changed, 10 insertions, 30 deletions
diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt index 1b016a4e..c48c2d5d 100644 --- a/dev/doc/setup.txt +++ b/dev/doc/setup.txt @@ -12,7 +12,7 @@ How to compile Coq Getting build dependencies: - sudo apt-get install make opam git mercurial darcs + sudo apt-get install make opam git opam init --comp 4.02.3 # Then follow the advice displayed at the end as how to update your ~/.bashrc and ~/.ocamlinit files. @@ -41,17 +41,15 @@ Building coqtop: cd ~/git/coq git checkout trunk make distclean - ./configure -annotate -with-doc no -local -debug -usecamlp5 + ./configure -profile devel make clean make -j4 coqide printers -The "-annotate" option is essential when one wants to use Merlin. +The "-profile devel" enables all options recommended for developers (like +warnings, support for Merlin, etc). Moreover Coq is configured so that +it can be run without installing it (i.e. from the current directory). -The "-local" option is useful if one wants to run the coqtop and coqide binaries without running make install - -The "-debug" option is essential if one wants to use ocamldebug with the coqtop binary. - -Then check if +Once the compilation is over check if - bin/coqtop - bin/coqide behave as expected. @@ -60,30 +58,12 @@ behave as expected. A note about rlwrap ------------------- -Running "coqtop" under "rlwrap" is possible, but there is a catch. If you try: - - cd ~/git/coq - rlwrap bin/coqtop - -you will get an error: +When using "rlwrap coqtop" make sure the version of rlwrap is at least +0.42, otherwise you will get rlwrap: error: Couldn't read completions from /usr/share/rlwrap/completions/coqtop: No such file or directory -This is a known issue: - - https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=779692 - -It was fixed upstream in version 0.42, and in a Debian package that, at the time of writing, is not part of Debian stable/testing/sid archives but only of Debian experimental. - - https://packages.debian.org/experimental/rlwrap - -The quick solution is to grab it from there, since it installs fine on Debian stable (jessie). - - cd /tmp - wget http://ftp.us.debian.org/debian/pool/main/r/rlwrap/rlwrap_0.42-1_amd64.deb - sudo dpkg -i rlwrap_0.42-1_amd64.deb - -After that, "rlwrap" works fine with "coqtop". +If this happens either update or use an alternate readline wrapper like "ledit". How to install and configure Merlin (for Emacs) @@ -281,7 +261,7 @@ You can load them by switching to the window holding the "ocamldebug" shell and Some of the functions were you might want to set a breakpoint and see what happens next --------------------------------------------------------------------------------------- -- Coqtop.start : This function is called by the code produced by "coqmktop". +- Coqtop.start : This function is the main entry point of coqtop. - Coqtop.parse_args : This function is responsible for parsing command-line arguments. - Coqloop.loop : This function implements the read-eval-print loop. - Vernacentries.interp : This function is called to execute the Vernacular command user have typed.\ |