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 , 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: customize-group merlin 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 . If you want to jump back, type: If you want to learn the type of the value at current cursor's position, type: Enabling auto-completion in emacs --------------------------------- In Emacs, type: list-packages 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 . 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 "") 'ocamldebug-break) (global-set-key (kbd "") 'ocamldebug-run) (global-set-key (kbd "") 'ocamldebug-next) (global-set-key (kbd "") 'ocamldebug-step) (global-set-key (kbd "") 'ocamldebug-finish) (global-set-key (kbd "") 'ocamldebug-print) (global-set-key (kbd "") '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: ../bin/coqtop.byte ../dev/ocamldebug-coq 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 you set a breakpoint to the cursor's position. 6. By pressing you start the bin/coqtop process. 7. Then you can: - step over function calls: - step into function calls: - or finish execution of the current function until it returns: . 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.