diff options
Diffstat (limited to 'dev/doc/setup.txt')
| -rw-r--r-- | dev/doc/setup.txt | 289 |
1 files changed, 289 insertions, 0 deletions
diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt new file mode 100644 index 00000000..1b016a4e --- /dev/null +++ b/dev/doc/setup.txt @@ -0,0 +1,289 @@ +This document provides detailed guidance on how to: +- compile Coq +- take advantage of Merlin in Emacs +- enable auto-completion for Ocaml source-code +- use ocamldebug in Emacs for debugging coqtop +The instructions were tested with Debian 8.3 (Jessie). + +The procedure is somewhat tedious, but the final results are (still) worth the effort. + +How to compile Coq +------------------ + +Getting build dependencies: + + sudo apt-get install make opam git mercurial darcs + opam init --comp 4.02.3 + # Then follow the advice displayed at the end as how to update your ~/.bashrc and ~/.ocamlinit files. + + source ~/.bashrc + + # needed if you want to build "coqtop" target + opam install camlp5 + + # needed if you want to build "coqide" target + sudo apt-get install liblablgtksourceview2-ocaml-dev libgtk2.0-dev libgtksourceview2.0-dev + opam install lablgtk + + # needed if you want to build "doc" target + sudo apt-get install texlive-latex-recommended texlive-fonts-extra texlive-math-extra \ + hevea texlive-latex-extra latex-xcolor + +Cloning Coq: + + # Go to the directory where you want to clone Coq's source-code. E.g.: + cd ~/git + + git clone https://github.com/coq/coq.git + +Building coqtop: + + cd ~/git/coq + git checkout trunk + make distclean + ./configure -annotate -with-doc no -local -debug -usecamlp5 + make clean + make -j4 coqide printers + +The "-annotate" option is essential when one wants to use Merlin. + +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 +- bin/coqtop +- bin/coqide +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: + + 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". + + +How to install and configure Merlin (for Emacs) +----------------------------------------------- + + sudo apt-get install emacs + + opam install tuareg + # Follow the advice displayed at the end as how to update your ~/.emacs file. + + opam install merlin + # Follow the advice displayed at the end as how to update your ~/.emacs file. + +Then add this: + + (push "~/.opam/4.02.3/share/emacs/site-lisp" load-path) ; directory containing merlin.el + (setq merlin-command "~/.opam/4.02.3/bin/ocamlmerlin") ; needed only if ocamlmerlin not already in your PATH + (autoload 'merlin-mode "merlin" "Merlin mode" t) + (add-hook 'tuareg-mode-hook 'merlin-mode) + (add-hook 'caml-mode-hook 'merlin-mode) + (load "~/.opam/4.02.3/share/emacs/site-lisp/tuareg-site-file") + + ;; Do not use TABs. These confuse Merlin. + (setq-default indent-tabs-mode nil) + +to your ~/.emacs file. + +Further Emacs configuration when we start it for the first time. + +Try to open some *.ml file in Emacs, e.g.: + + cd ~/git/coq + emacs toplevel/coqtop.ml & + +Emacs display the following strange message: + + The local variables list in ~/git/coq + contains values that may be safe (*). + + Do you want to apply it? + +Just press "!", i.e. "apply the local variable list, and permanently mark these values (\*) as safe." + +Emacs then shows two windows: +- one window that shows the contents of the "toplevel/coqtop.ml" file +- and the other window that shows greetings for new Emacs users. + +If you do not want to see the second window next time you start Emacs, just check "Never show it again" and click on "Dismiss this startup screen." + +The default key-bindings are described here: + + https://github.com/the-lambda-church/merlin/wiki/emacs-from-scratch + +If you want, you can customize them by replacing the following lines: + + (define-key merlin-map (kbd "C-c C-x") 'merlin-error-next) + (define-key merlin-map (kbd "C-c C-l") 'merlin-locate) + (define-key merlin-map (kbd "C-c &") 'merlin-pop-stack) + (define-key merlin-map (kbd "C-c C-t") 'merlin-type-enclosing) + +in the file "~/.opam/4.02.3/share/emacs/site-lisp/merlin.el" with what you want. +In the text below we assume that you changed the origin key-bindings in the following way: + + (define-key merlin-map (kbd "C-n") 'merlin-error-next) + (define-key merlin-map (kbd "C-l") 'merlin-locate) + (define-key merlin-map (kbd "C-b") 'merlin-pop-stack) + (define-key merlin-map (kbd "C-t") 'merlin-type-enclosing) + +Now, when you press <Ctrl+L>, Merlin will show the definition of the symbol in a separate window. +If you prefer to jump to the definition within the same window, do this: + + <Alt+X> customize-group <ENTER> merlin <ENTER> + + Merlin Locate In New Window + + Value Menu + + Never Open In New Window + + State + + Set For Future Sessions + +Testing (Merlin): + + cd ~/git/coq + emacs toplevel/coqtop.ml & + +Go to the end of the file where you will see the "start" function. + +Go to a line where "init_toplevel" function is called. + +If you want to jump to the position where that function or datatype under the cursor is defined, press <Ctrl+L>. + +If you want to jump back, type: <Ctrl+B> + +If you want to learn the type of the value at current cursor's position, type: <Ctrl+T> + + +Enabling auto-completion in emacs +--------------------------------- + +In Emacs, type: <Alt+M> list-packages <ENTER> + +In the list that is displayed, click on "company". + +A new window appears where just click on "Install" and then answer "Yes". + +These lines: + + (package-initialize) + (require 'company) + ; Make company aware of merlin + (add-to-list 'company-backends 'merlin-company-backend) + ; Enable company on merlin managed buffers + (add-hook 'merlin-mode-hook 'company-mode) + (global-set-key [C-tab] 'company-complete) + +then need to be added to your "~/.emacs" file. + +Next time when you start emacs and partially type some identifier, +emacs will offer the corresponding completions. +Auto-completion can also be manually invoked by typing <Ctrl+TAB>. +Description of various other shortcuts is here. + + http://company-mode.github.io/ + + +Getting along with ocamldebug +----------------------------- + +The default ocamldebug key-bindings are described here. + + http://caml.inria.fr/pub/docs/manual-ocaml/debugger.html#sec369 + +If you want, you can customize them by putting the following commands: + + (global-set-key (kbd "<f5>") 'ocamldebug-break) + (global-set-key (kbd "<f6>") 'ocamldebug-run) + (global-set-key (kbd "<f7>") 'ocamldebug-next) + (global-set-key (kbd "<f8>") 'ocamldebug-step) + (global-set-key (kbd "<f9>") 'ocamldebug-finish) + (global-set-key (kbd "<f10>") 'ocamldebug-print) + (global-set-key (kbd "<f12>") 'camldebug) + +to your "~/.emacs" file. + +Let us try whether ocamldebug in Emacs works for us. +(If necessary, re-)compile coqtop: + + cd ~/git/coq + make -j4 coqide printers + +open Emacs: + + emacs toplevel/coqtop.ml & + +and type: + + <F12> ../bin/coqtop.byte <ENTER> ../dev/ocamldebug-coq <ENTER> + +As a result, a new window is open at the bottom where you should see: + + (ocd) + +i.e. an ocamldebug shell. + + 1. Switch to the window that contains the "coqtop.ml" file. + 2. Go to the end of the file. + 3. Find the definition of the "start" function. + 4. Go to the "let" keyword that is at the beginning of the first line. + 5. By pressing <F5> you set a breakpoint to the cursor's position. + 6. By pressing <F6> you start the bin/coqtop process. + 7. Then you can: + - step over function calls: <F7> + - step into function calls: <F8> + - or finish execution of the current function until it returns: <F9>. + +Other ocamldebug commands, can be typed to the window that holds the ocamldebug shell. + +The points at which the execution of Ocaml program can stop are defined here: + + http://caml.inria.fr/pub/docs/manual-ocaml/debugger.html#sec350 + + +Installing printers to ocamldebug +--------------------------------- + +There is a pretty comprehensive set of printers defined for many common data types. +You can load them by switching to the window holding the "ocamldebug" shell and typing: + + (ocd) source "../dev/db" + + +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.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.\ + It dispatches the control to specific functions handling different Vernacular command. +- Vernacentries.vernac_check_may_eval : This function handles the "Check ..." command. |