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
|
.TH COQNATIVE 1
.
.SH NAME
coqnative \- native Coq compiler
.
.
.SH SYNOPSIS
.B coqnative
[
options
]
.I filename
.
.
.SH DESCRIPTION
.
.B coqnative
compiles vo files to binary files used by the native compute mechanism
of the Coq Proof Assistant.
See the
.I "Reference Manual"
for more information.
It returns with exit code 0 if all the requested tasks succeeded.
A non-zero return code means that something went wrong.
.PP
.I filename
is a Coq object file (a .vo) to compile to a native binary.
.
.SH OPTIONS
.
.TP
.BI \-Q \ dir\ coqdir
Map physical
.I dir
to logical
.I coqdir.
.
.TP
.BI \-R \ dir\ coqdir
Synonymous to
.BR \-Q .
.
.TP
.BI \-I \ dir
Ignored, for compatibility.
.
.TP
.B \-noinit
Ignored, for compatibility.
.
.TP
.B \-boot
Boot mode.
.
.TP
.BI \-coqlib \ dir
Override the default location of the standard library.
.
.TP
.BI \-nI \ dir
Add
.I dir
to the set of paths for the native files of the dependencies.
.
.TP
.BI \-native-output-dir \ dir
Output the generated files to
.I dir.
.
.TP
.BR \-h , \ \-\-help
Print list of options.
.
.SH SEE ALSO
.
.BR coqtop (1),
.BR coqc (1),
.BR coq_makefile (1),
.BR coqdep (1)
.PP
.I
The Rocq Prover Reference Manual.
.PP
The Rocq Prover website: https://rocq-prover.org
|
