|
0 |
.TH COQIDE 1 "July 16, 2004"
|
|
1 |
|
|
2 |
.SH NAME
|
|
3 |
coqide \- The Coq Proof Assistant graphical interface
|
|
4 |
|
|
5 |
|
|
6 |
.SH SYNOPSIS
|
|
7 |
.B coqide
|
|
8 |
[
|
|
9 |
.B options
|
|
10 |
]
|
|
11 |
|
|
12 |
.SH DESCRIPTION
|
|
13 |
|
|
14 |
.B coqtop
|
|
15 |
is a gtk graphical interface for the Coq proof assistant.
|
|
16 |
|
|
17 |
For command-line-oriented use of Coq, see
|
|
18 |
.BR coqide (1)
|
|
19 |
; for batch-oriented use of Coq, see
|
|
20 |
.BR coqc (1).
|
|
21 |
|
|
22 |
|
|
23 |
.SH OPTIONS
|
|
24 |
|
|
25 |
.TP
|
|
26 |
.B \-h
|
|
27 |
Get the complete list of options accepted by
|
|
28 |
.BR coqide .
|
|
29 |
.TP
|
|
30 |
.BI \-I\ dir ,\ \-include\ dir
|
|
31 |
Add directory dir in the include path.
|
|
32 |
.TP
|
|
33 |
.BI \-R\ dir\ coqdir
|
|
34 |
Recursively map physical
|
|
35 |
.I dir
|
|
36 |
to logical
|
|
37 |
.IR coqdir .
|
|
38 |
.TP
|
|
39 |
.B \-src
|
|
40 |
Add source directories in the include path.
|
|
41 |
.TP
|
|
42 |
.BI \-is\ f ,\ \-inputstate\ f
|
|
43 |
Read state from
|
|
44 |
.IR f .coq.
|
|
45 |
.TP
|
|
46 |
.B \-nois
|
|
47 |
Start with an empty state.
|
|
48 |
.TP
|
|
49 |
.BI \-outputstate\ f
|
|
50 |
Write state in file
|
|
51 |
.IR f .coq.
|
|
52 |
.TP
|
|
53 |
.BI \-load\-ml\-object\ f
|
|
54 |
Load ML object file
|
|
55 |
.IR f .
|
|
56 |
.TP
|
|
57 |
.BI \-load\-ml\-source\ f
|
|
58 |
Load ML file
|
|
59 |
.IR f .
|
|
60 |
.TP
|
|
61 |
.BI \-l\ f ,\ \-load\-vernac\-source\ f
|
|
62 |
Load Coq file
|
|
63 |
.IR f .v
|
|
64 |
(Load
|
|
65 |
.IR f .).
|
|
66 |
.TP
|
|
67 |
.BI \-lv\ f ,\ \-load\-vernac\-source\-verbose\ f
|
|
68 |
Load Coq file
|
|
69 |
.IR f .v
|
|
70 |
(Load Verbose
|
|
71 |
.IR f .).
|
|
72 |
.TP
|
|
73 |
.BI \-load\-vernac\-object\ f
|
|
74 |
Load Coq object file
|
|
75 |
.IR f .vo.
|
|
76 |
.TP
|
|
77 |
.BI \-require\ f
|
|
78 |
Load Coq object file
|
|
79 |
.IR f .vo
|
|
80 |
and import it (Require
|
|
81 |
.IR f .).
|
|
82 |
.TP
|
|
83 |
.BI \-compile\ f
|
|
84 |
Compile Coq file
|
|
85 |
.IR f .v
|
|
86 |
(implies
|
|
87 |
.BR \-batch ).
|
|
88 |
.TP
|
|
89 |
.BI \-compile\-verbose\ f
|
|
90 |
Verbosely compile Coq file
|
|
91 |
.IR f .v
|
|
92 |
(implies
|
|
93 |
.BR -batch ).
|
|
94 |
.TP
|
|
95 |
.B \-opt
|
|
96 |
Run the native-code version of Coq or Coq_SearchIsos.
|
|
97 |
.TP
|
|
98 |
.B \-byte
|
|
99 |
Run the bytecode version of Coq or Coq_SearchIsos.
|
|
100 |
.TP
|
|
101 |
.B \-where
|
|
102 |
Print Coq's standard library location and exit.
|
|
103 |
.TP
|
|
104 |
.B -v
|
|
105 |
Print Coq version and exit.
|
|
106 |
.TP
|
|
107 |
.B \-q
|
|
108 |
Skip loading of rcfile.
|
|
109 |
.TP
|
|
110 |
.BI \-init\-file\ f
|
|
111 |
Set the rcfile to
|
|
112 |
.IR f .
|
|
113 |
.TP
|
|
114 |
.BI \-user\ u
|
|
115 |
Use the rcfile of user
|
|
116 |
.IR u .
|
|
117 |
.TP
|
|
118 |
.B \-batch
|
|
119 |
Batch mode (exits just after arguments parsing).
|
|
120 |
.TP
|
|
121 |
.B \-boot
|
|
122 |
Boot mode (implies
|
|
123 |
.B \-q
|
|
124 |
and
|
|
125 |
.BR \-batch ).
|
|
126 |
.TP
|
|
127 |
.B \-emacs
|
|
128 |
Tells Coq it is executed under Emacs.
|
|
129 |
.TP
|
|
130 |
.BI \-dump\-glob\ f
|
|
131 |
Dump globalizations in file
|
|
132 |
.I f
|
|
133 |
(to be used by
|
|
134 |
.BR coqdoc (1)).
|
|
135 |
.TP
|
|
136 |
.B \-impredicative\-set
|
|
137 |
Set sort Set impredicative.
|
|
138 |
.TP
|
|
139 |
.B \-dont\-load\-proofs
|
|
140 |
Don't load opaque proofs in memory.
|
|
141 |
.TP
|
|
142 |
.B \-xml
|
|
143 |
Export XML files either to the hierarchy rooted in
|
|
144 |
the directory
|
|
145 |
.B COQ_XML_LIBRARY_ROOT
|
|
146 |
(if set) or to stdout (if unset).
|
|
147 |
|
|
148 |
|
|
149 |
.SH SEE ALSO
|
|
150 |
|
|
151 |
.BR coqc (1),
|
|
152 |
.BR coqtop (1),
|
|
153 |
.BR coq-tex (1),
|
|
154 |
.BR coqdep (1).
|
|
155 |
.br
|
|
156 |
.I
|
|
157 |
The Coq Reference Manual,
|
|
158 |
.I
|
|
159 |
The Coq web site: http://coq.inria.fr,
|
|
160 |
.I
|
|
161 |
/usr/share/doc/coqide/FAQ.
|
|
162 |
|
|
163 |
.SH AUTHOR
|
|
164 |
This manual page was written by Samuel Mimram <samuel.mimram@ens-lyon.org>,
|
|
165 |
for the Debian project (but may be used by others).
|