diff options
Diffstat (limited to 'dev/doc/setup.txt')
| -rw-r--r-- | dev/doc/setup.txt | 269 |
1 files changed, 0 insertions, 269 deletions
diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt deleted file mode 100644 index c48c2d5d..00000000 --- a/dev/doc/setup.txt +++ /dev/null @@ -1,269 +0,0 @@ -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. |