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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: coqinit.ml 11749 2009-01-05 14:01:04Z notin $ *)
open Pp
open System
open Toplevel
let (/) = Filename.concat
let set_debug () = Flags.debug := true
(* Loading of the ressource file.
rcfile is either $HOME/.coqrc.VERSION, or $HOME/.coqrc if the first one
does not exist. *)
let rcfile = ref (home/".coqrc")
let rcfile_specified = ref false
let set_rcfile s = rcfile := s; rcfile_specified := true
let set_rcuser s = rcfile := ("~"^s)/".coqrc"
let load_rc = ref true
let no_load_rc () = load_rc := false
let load_rcfile() =
if !load_rc then
try
if !rcfile_specified then
if file_readable_p !rcfile then
Vernac.load_vernac false !rcfile
else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
else if file_readable_p (!rcfile^"."^Coq_config.version) then
Vernac.load_vernac false (!rcfile^"."^Coq_config.version)
else if file_readable_p !rcfile then
Vernac.load_vernac false !rcfile
else ()
(*
Flags.if_verbose
mSGNL (str ("No .coqrc or .coqrc."^Coq_config.version^
" found. Skipping rcfile loading."))
*)
with e ->
(msgnl (str"Load of rcfile failed.");
raise e)
else
Flags.if_verbose msgnl (str"Skipping rcfile loading.")
let add_ml_include s =
Mltop.add_ml_dir s
(* Puts dir in the path of ML and in the LoadPath *)
let coq_add_path d s =
Mltop.add_path d (Names.make_dirpath [Nameops.coq_root;Names.id_of_string s])
let coq_add_rec_path s = Mltop.add_rec_path s (Names.make_dirpath [Nameops.coq_root])
(* By the option -include -I or -R of the command line *)
let includes = ref []
let push_include (s, alias) = includes := (s,alias,false) :: !includes
let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes
(* Because find puts "./" and the loadpath is not nicely pretty-printed *)
let hm2 s =
let n = String.length s in
if n > 1 && s.[0] = '.' && s.[1] = '/' then String.sub s 2 (n-2) else s
(* The list of all theories in the standard library /!\ order does matter *)
let theories_dirs_map = [
"theories/Unicode", "Unicode" ;
"theories/Classes", "Classes" ;
"theories/Program", "Program" ;
"theories/FSets", "FSets" ;
"theories/Reals", "Reals" ;
"theories/Strings", "Strings" ;
"theories/Sorting", "Sorting" ;
"theories/Setoids", "Setoids" ;
"theories/Sets", "Sets" ;
"theories/Lists", "Lists" ;
"theories/Wellfounded", "Wellfounded" ;
"theories/Relations", "Relations" ;
"theories/Numbers", "Numbers" ;
"theories/QArith", "QArith" ;
"theories/NArith", "NArith" ;
"theories/ZArith", "ZArith" ;
"theories/Arith", "Arith" ;
"theories/Bool", "Bool" ;
"theories/Logic", "Logic" ;
"theories/Init", "Init"
]
(* Initializes the LoadPath *)
let init_load_path () =
let coqlib = Envars.coqlib () in
let user_contrib = coqlib/"user-contrib" in
let dirs = "states" :: ["contrib"] in
(* first user-contrib *)
if Sys.file_exists user_contrib then
Mltop.add_rec_path user_contrib Nameops.default_root_prefix;
(* then states, contrib and dev *)
List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
(* developer specific directory to open *)
if Coq_config.local then coq_add_path (coqlib/"dev") "dev";
(* then standard library *)
List.iter
(fun (s,alias) -> Mltop.add_rec_path (coqlib/s) (Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root]))
theories_dirs_map;
(* then current directory *)
Mltop.add_path "." Nameops.default_root_prefix;
(* additional loadpath, given with -I -include -R options *)
List.iter
(fun (s,alias,reci) ->
if reci then Mltop.add_rec_path s alias else Mltop.add_path s alias)
(List.rev !includes)
let init_library_roots () =
includes := []
(* Initialises the Ocaml toplevel before launching it, so that it can
find the "include" file in the *source* directory *)
let init_ocaml_path () =
let coqsrc = Coq_config.coqsrc in
let add_subdir dl =
Mltop.add_ml_dir (List.fold_left (/) coqsrc dl)
in
Mltop.add_ml_dir (Envars.coqlib ());
List.iter add_subdir
[ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ];
[ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
[ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ]
|
