blob: 564acaee6fc834a5f490caf0619980770878f4f4 (
plain)
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
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
|
(* $Id$ *)
open Pp
open Util
open System
open Options
open States
open Toplevel
open Coqinit
let print_header () =
Printf.printf "Welcome to Coq %s (%s)\n" Coq_config.version Coq_config.date;
flush stdout
let set_batch_mode () = batch_mode := true
let remove_top_ml () = Mltop.remove ()
let inputstate = ref "initial.coq"
let set_inputstate s = inputstate:= s
let inputstate () =
if !inputstate <> "" then begin
intern_state !inputstate;
Lib.declare_initial_state()
end
let outputstate = ref ""
let set_outputstate s = outputstate:=s
let outputstate () = if !outputstate <> "" then extern_state !outputstate
let load_vernacular_list = ref ([] : string list)
let add_load_vernacular s =
load_vernacular_list := (make_suffix s ".v") :: !load_vernacular_list
let load_vernacular () =
List.iter
(fun s -> Vernac.load_vernac false s)
(List.rev !load_vernacular_list)
let load_vernacular_obj = ref ([] : string list)
let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj
let load_vernac_obj () =
List.iter
(fun s -> Library.load_module (Filename.basename s) (Some s))
(List.rev !load_vernacular_obj)
let require_list = ref ([] : string list)
let add_require s = require_list := s :: !require_list
let require () =
List.iter
(fun s -> Library.require_module None (Filename.basename s) (Some s) false)
(List.rev !require_list)
(* Parsing of the command line.
*
* We no longer use Arg.parse, in order to use share Usage.print_usage
* between coqtop and coqc. *)
let usage () =
if !batch_mode then
Usage.print_usage_coqc ()
else
Usage.print_usage_coqtop () ;
flush stderr ;
exit 1
let version () =
Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
Coq_config.version Coq_config.date;
Printf.printf "compiled on %s\n" Coq_config.compile_date;
exit 0
let parse_args () =
let rec parse = function
| [] -> ()
| ("-I"|"-include") :: d :: rem -> push_include d; parse rem
| ("-I"|"-include") :: [] -> usage ()
| "-R" :: d :: rem -> rec_include d; parse rem
| "-R" :: [] -> usage ()
| "-q" :: rem -> no_load_rc (); parse rem
| "-batch" :: rem -> set_batch_mode (); parse rem
| "-outputstate" :: s :: rem -> set_outputstate s; parse rem
| "-outputstate" :: [] -> usage ()
| "-nois" :: rem -> set_inputstate ""; parse rem
| ("-inputstate"|"-is") :: s :: rem -> set_inputstate s; parse rem
| ("-inputstate"|"-is") :: [] -> usage ()
| "-load-ml-object" :: f :: rem -> Mltop.dir_ml_load f; parse rem
| "-load-ml-object" :: [] -> usage ()
| "-load-ml-source" :: f :: rem -> Mltop.dir_ml_use f; parse rem
| "-load-ml-source" :: [] -> usage ()
| "-load-vernac-source" :: f :: rem -> add_load_vernacular f; parse rem
| "-load-vernac-source" :: [] -> usage ()
| "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem
| "-load-vernac-object" :: [] -> usage ()
| "-require" :: f :: rem -> add_require f; parse rem
| "-require" :: [] -> usage ()
| "-unsafe" :: f :: rem -> add_unsafe f; parse rem
| "-unsafe" :: [] -> usage ()
| "-debug" :: rem -> set_debug (); parse rem
| "-emacs" :: rem -> Options.print_emacs := true; parse rem
| "-where" :: _ -> print_endline Coq_config.coqlib; exit 0
| ("-quiet"|"-silent") :: rem -> Options.make_silent true; parse rem
| ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
| ("-v"|"--version") :: _ -> version ()
| "-init-file" :: f :: rem -> set_rcfile f; parse rem
| "-init-file" :: [] -> usage ()
| "-user" :: u :: rem -> set_rcuser u; parse rem
| "-user" :: [] -> usage ()
| "-notactics" :: rem -> remove_top_ml (); parse rem
| "-just-parsing" :: rem -> Vernac.just_parsing := true; parse rem
| s :: _ -> prerr_endline ("Don't know what to do with " ^ s); usage ()
in
try
parse (List.tl (Array.to_list Sys.argv))
with
| UserError(_,s) as e -> begin
try
Stream.empty s; exit 1
with Stream.Failure ->
mSGNL (Errors.explain_exn e); exit 1
end
| e -> begin mSGNL (Errors.explain_exn e); exit 1 end
(* To prevent from doing the initialization twice *)
let initialized = ref false
(* Ctrl-C is fatal during the initialisation *)
let start () =
if not !initialized then begin
initialized := true;
Sys.catch_break false;
Lib.init();
try
parse_args ();
if is_verbose() then print_header ();
init_load_path ();
inputstate ();
load_vernac_obj ();
require ();
load_rcfile();
load_vernacular ();
outputstate ()
with e ->
flush_all();
if not !batch_mode then message "Error during initialization :";
mSGNL (Toplevel.print_toplevel_error e);
exit 1
end;
if !batch_mode then (flush_all(); Profile.print_profile ();exit 0);
Toplevel.loop()
(* Coqtop.start will be called by the code produced by coqmktop *)
|
