1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
|
-*- 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") ***
* Ergonomy
** 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.
* 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
** How do I enable three windows mode by default?
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?
Put this in your configuration file:
(setq proof-splash-enable nil)
** How do I enable the "compile before require" mode by default?
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))
|
