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
  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 -profile devel
  make clean
  make -j4 coqide printers

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

Once the compilation is over check if
- bin/coqtop
- bin/coqide
behave as expected.


A note about rlwrap
-------------------

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

If this happens either update or use an alternate readline wrapper like "ledit".


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 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.\
                         It dispatches the control to specific functions handling different Vernacular command.
- Vernacentries.vernac_check_may_eval : This function handles the "Check ..." command.