path: root/dev/doc/setup.txt

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.