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
|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Util
(** * Command-line parsing *)
type prefix = RelocatableInstall | Prefix of string
type nativecompiler = NativeYes | NativeNo | NativeOndemand
module Prefs = struct
type t = {
prefix : prefix option;
quiet : bool;
interactive : bool;
libdir : string option;
configdir : string option;
datadir : string option;
mandir : string option;
docdir : string option;
arch : string option;
natdynlink : bool;
browser : string option;
bytecodecompiler : bool;
nativecompiler : nativecompiler;
coqwebsite : string;
debug : bool;
}
end
open Prefs
let default_prefs = {
prefix = None;
quiet = false;
interactive = true;
libdir = None;
configdir = None;
datadir = None;
mandir = None;
docdir = None;
arch = None;
natdynlink = true;
browser = None;
bytecodecompiler = true;
nativecompiler = NativeNo;
coqwebsite = "http://rocq-prover.org/";
debug = false;
}
let get_bool = function
| "true" | "yes" | "y" | "all" -> true
| "false" | "no" | "n" -> false
| s -> raise (Arg.Bad ("boolean argument expected instead of "^s))
let get_native = function
| "yes" -> NativeYes
| "no" -> NativeNo
| "ondemand" -> NativeOndemand
| s -> raise (Arg.Bad ("(yes|no|ondemand) argument expected instead of "^s))
let prefs = ref default_prefs
let arg_bool f = Arg.String (fun s -> prefs := f !prefs (get_bool s))
let arg_string f = Arg.String (fun s -> prefs := f !prefs s)
let arg_string_option f = Arg.String (fun s -> prefs := f !prefs (Some s))
let arg_set f = Arg.Unit (fun () -> prefs := f !prefs)
let arg_native f = Arg.String (fun s -> prefs := f !prefs (get_native s))
(* TODO : earlier any option -foo was also available as --foo *)
let warn_warn_error () =
Format.eprintf "****** the -warn-error option is deprecated, \
warnings are not set in the config section of the \
corresponding build tool [coq_makefile, dune]@\n%!"
let make_prefix path =
if Filename.is_relative path then
Prefix (Sys.getcwd() ^ "/" ^ path)
else Prefix path
let args_options = Arg.align [
"-prefix", arg_string (fun p prefix -> { p with prefix = Some (make_prefix prefix) }),
"<dir> Set installation directory to <dir>";
"-relocatable", arg_set (fun p -> { p with prefix = Some RelocatableInstall } ),
" Make a relocatable installation";
"-quiet", arg_set (fun p -> { p with quiet = true }),
" Don't print variables during configure";
"-no-ask", arg_set (fun p -> { p with interactive = false }),
" Don't ask questions during configure [questions will be filled with defaults]";
"-libdir", arg_string_option (fun p libdir -> { p with libdir }),
"<dir> Where to install lib files";
"-configdir", arg_string_option (fun p configdir -> { p with configdir }),
"<dir> Where to install config files";
"-datadir", arg_string_option (fun p datadir -> { p with datadir }),
"<dir> Where to install data files";
"-mandir", arg_string_option (fun p mandir -> { p with mandir }),
"<dir> Where to install man files";
"-docdir", arg_string_option (fun p docdir -> { p with docdir }),
"<dir> Where to install doc files";
"-arch", arg_string_option (fun p arch -> { p with arch }),
"<arch> Specifies the architecture";
"-natdynlink", arg_bool (fun p natdynlink -> { p with natdynlink }),
"(yes|no) Use dynamic loading of native code or not";
"-browser", arg_string_option (fun p browser -> { p with browser }),
"<command> Use <command> to open URL %s";
"-bytecode-compiler", arg_bool (fun p bytecodecompiler -> { p with bytecodecompiler }),
"(yes|no) Enable Rocq's bytecode reduction machine (VM)";
"-native-compiler", arg_native (fun p nativecompiler -> { p with nativecompiler }),
"(yes|no|ondemand) Compilation to native code for conversion and normalization
yes: -native-compiler option of coqc will default to 'yes', stdlib will be precompiled
no (default): no native compilation available at all
ondemand: -native-compiler option of coqc will default to 'ondemand', stdlib will not be precompiled";
"-warn-error", arg_bool (fun p _warn_error -> warn_warn_error (); p),
" Deprecated option: warnings are now adjusted in the corresponding build tool.";
"-coqwebsite", arg_string (fun p coqwebsite -> { p with coqwebsite }),
" URL of the rocq website";
"-debug", arg_set (fun p -> { p with debug = true }), " Enable debug information for package detection"
]
let parse_args () =
Arg.parse
args_options
(fun s -> raise (Arg.Bad ("Unknown option: "^s)))
"Available options for configure are:";
!prefs
(* Support don't ask *)
let cprintf prefs x =
if not prefs.quiet
then cprintf x
else Printf.ifprintf stdout x
|
