path: root/coq/faq

-*- outline -*-  

This is a small FAQ for users of coq proof general.

* Configuration of coqtop

** How do I configure the options for coqtop?

*** Answer 1: Recommended way of setting coqtop options: use coq project file _CoqProject

The recommended way is to have a _CoqProject file in the root
directory of your develpment, as recommended by the coq documentation
(section "Creating a Makefile for Coq modules"). This file should
contain, among other things, lines like these:

-I foo
-R bar baz
-arg -fuo

which will be read by proofgeneral to set up the coqtop command line.
In this example it will be:

coqtop -I foo -R bar baz -fuo

The -emacs option will be added automatically too. File variables (see
below) can be used to overwrite this configuration.

*** Answer 2:  Alternative way (also allows to overwrite file project file settings)

In the case you need to configure a specific file differently than
others, or if you have only one file, you may use the "File Variables"
mechanism of emacs to set the value of the variable coq-load-path and
coq-prog-args using this syntax:

    (*
     *** Local Variables: ***
     *** coq-load-path: ("foo" ("bar" "baz")) ***
     *** coq-prog-args: ("-fuo") ***
     *** End: ***
     *)

This must be at the end of the file. See emacs documentation on File
Variables for more details. See also ProofGeneral documentation
section "Using file varaiables".

** How to configure the coqtop binary?

Add the following line to the local variables explained above to set
the binary to use for coqtop (if not in the path):

    *** coq-prog-name: ("xxx/bin/coqtop") ***

** OK I want to use a coq project file but with another name, can I?

Yes you can:

(setq coq-project-filename "myprojectfile")

or:

(setq (make-local-variable 'coq-project-filename) "myprojectfile")

If this is for a whole project, the best is probably to have a
.dir-locals.el file as explained in the section of proofgeneral manual
(section "Using file variables"). This file should contain something
like:

((coq-mode . ((coq-project-filename . "myprojectfile"))))

or equivalently:

((coq-mode
  .
  ((eval
    .
    (progn 
      (make-local-variable 'coq-project-filename)
      (setq coq-project-filename  "myprojectfile"))))))

 
* Ergonomy

** What are the shortcuts I should know?

The one for navigation:

*** C-c C-n for one step
*** C-c C-enter to go to cursor.
You may want to bind these to more convenient non-standard shortcuts.
ProofGeneral follows emacs policy: it avoids polluting the "short"
shortcuts with its bindings and let the user configure them at will
instead.

Other useful shortcuts for queries to coq:

*** C-c C-a C-i
Inserts ``intros '' and also introduces the name of the hypothesis
proposed by coq on the current goal.

*** C-c C-a C-s
Show the goal (enter for the current goal, i <enter> for the ith
goal).

IMPORTANT: Add the prefix C-u to see the answer with all pretty
printing options temporarily disable (Set Printing All).

*** C-c C-a C-c   
Prompts for ``Check '' query arguments, the default input name is built
from the identifier under the cursor.

IMPORTANT: Add the prefix C-u to see the answer with all pretty
printing options temporarily disable (Set Printing All).

*** C-c C-a C-p The same for a ``Print '' query.
*** C-c C-a C-b The same for a ``About '' query.
*** C-c C-a C-a The same for a ``SearchAbout '' query (no C-u prefix).
*** C-c C-a C-o The same for a Search ``SearchIsos'' (no C-u prefix).

** I hate menus, why do you have menus?

Indeed, very few emacs users use menus, which is understandable.
However you should have a look at Coq menu and PG menu from time to
time to see the features they propose, then remember the shortcut and
hide the menu again.

** How can I tell coq to recompile the files that need to be recompiled?

Use option Coq > Settings > Compile before Require

Each time ProofGeneral scripts a "Require" command, it will decide if
the file needs to be recompiled by computing the dependencies between
files and comparing modification dates of files. A special Thanks to
Hendrik Tews for this cool feature.

Notice that this feature will only work if the the coq load path is
the same for all files. To configure the load path, see the question
"How do I configure the options for coqtop?" in this faq.

** Why does library compilation lock up my Emacs? Can it use more than one core for compilation? 

Enable Coq > Settings > Compile Parallel in Background to use the
more recent compilation engine, which compiles in parallel (in
case your dependencies permit this) and in the background.

** How can I display the proof tree of some proof?

Install Prooftree from http://askra.de/software/prooftree/,
restart Proof General and select menu entry
Proof-General > Start/Stop Prooftree or type C-c C-d .

* Three windows mode

It has been cleaned up. Here is how it works now.

** How do I enable three windows mode?

Menu Coq > toggle 3 windows mode
or Proof-General > Quick Options > Display > Use Three Panes.

** How do I enable three windows mode by default?

Choose Proof-General > Quick Options > Save Options

Alternatively, put this in you configuration file:

(setq proof-three-window-enable t)

** What are the possible layouts in 3 windows mode

The are three layouts:
  - vertical: the 3 buffers are displayed in one column.
  - hybrid: 2 columns mode, left column displays scripting buffer
    and right column displays the 2 others.
  - horizontal: 3 columns mode, one for each buffer (script, goals,
    response).

** What is the default layout?

The default layout is a "smart" one. One of the three layouts is
chosen depending on the current width of your emacs frame. The
threshold between is given by variable split-width-threshold:

 width < split-width-threshold ===> vertical mode
 split-width-threshold <= width < 1.5 * split-width-threshold ===> hybrid mode
 width <= split-width-threshold ===> horizontal mode

** How do I change the theshold between display modes in default mode?

You can change the value of `split-width-threshold' at your will by
putting this in your emacs configuration file:

(setq split-width-threshold 140)

Note that this is a global emacs setting, that may affect the way
frames are split by other modes. See description of function
`split-window-sensibly' for details.

** I changed the size of my frame and layout did not changed, what happened?

Hit C-c C-l to refresh layout, it will adapt to the new frame width.

** I don't like the default layout of three windows mode, how can I force it?

If you want to force one layout instead of letting emacs chose it for
you (see above question "what is the default layout?"), you can set
the variable `proof-three-window-mode-policy'. The three possible
values are: 'smart (default), 'vertical, 'horizontal, 'hybrid.

For example, putting this in your configuration file will force hybrid
mode:

(setq proof-three-window-mode-policy 'hybrid)


* other interface questions

** How do I disable the splash screen?

Choose Proof-General > Customize Options and disable "Proof
Splash Enable" (at the bottom) and choose "Save for Future
Sessions" by clicking on the state button.

Alternatively, put this in your configuration file:

(setq proof-splash-enable nil)

Type M-x proof-splash-display-screen to enjoy the splash screen
once.

** How do I enable the "compile before require" mode by default? 

Choose Coq > Settings > Save Settings.

Alternatively, put this in your configuration file:

(setq coq-compile-before-require t)

** Until now hovering the mouse cursor on the locked region
   was popping up some windows showing coq output, how do I bring
   this back?

This was removed because it was considered by many as more annoying
than useful, you can bring it back by:

Menu Coq / toggle tooltips.

** Electric terminator always goes to next line, how do I change this?

You can disable this by putting this in your configuration file:

(setq coq-one-command-per-line nil)


** How do I change the color of the queue/locked region?

(custom-set-faces
 '(proof-queue-face
   ((((type x) (class color) (background light))
     (:background "darksalmon"))) t)
 '(proof-locked-face
   ((((type x) (class color) (background light)) (:background "SlateGray3"))) t))