@@ -12,6 +12,7 @@ type t =
1212 ; path : Path .t
1313 ; vo : Path .t list
1414 ; cmxs : Path .t list
15+ ; cmxs_directories : Path .t list
1516 ; stdlib : bool
1617 }
1718
@@ -23,6 +24,8 @@ let vo t = t.vo
2324
2425let cmxs t = t.cmxs
2526
27+ let cmxs_directories t = t.cmxs_directories
28+
2629let stdlib t = t.stdlib
2730
2831let config_path_exn coq_config key =
@@ -48,98 +51,136 @@ let config_path ~default coq_config key =
4851 (* This should never happen *)
4952 Code_error. raise " key is not a path" Coq_config.Value. to_dyn path) ]
5053
51- let stdlib_plugins_dir path =
52- let open Memo.O in
53- let path = Path. relative path " plugins" in
54- let * dir_contents =
55- Fs_memo. dir_contents (Path. as_outside_build_dir_exn path)
56- in
57- match dir_contents with
58- | Error _ -> Memo. return []
59- | Ok dir_contents ->
60- let f (d , kind ) =
61- match kind with
62- | File_kind. S_DIR | S_LNK -> Some (Path. relative path d)
63- | _ -> None
64- in
65- Memo. return
66- (List. filter_map ~f (Fs_cache.Dir_contents. to_list dir_contents))
67-
68- let build_user_contrib ~cmxs ~vo ~subpath ~name =
69- let path = subpath in
70- { name; path; cmxs; vo; stdlib = false }
54+ let build_user_contrib ~cmxs ~cmxs_directories ~vo ~path ~name =
55+ { name; path; cmxs; cmxs_directories; vo; stdlib = false }
7156
7257(* Scanning todos: blacklist? *)
73- let scan_vo_cmxs ~path dir_contents =
58+ let scan_vo_cmxs ~dir dir_contents =
7459 let f (d , kind ) =
7560 match kind with
76- (* Skip some directories as Coq does, for now '-' and '. ' *)
61+ (* Skip some files as Coq does, for now files with '- ' *)
7762 | _ when String. contains d '-' -> List. Skip
78- | _ when String. contains d '.' -> Skip
7963 | (File_kind. S_REG | S_LNK ) when Filename. check_suffix d " .cmxs"
80- Left (Path. relative path d)
64+ Left (Path. relative dir d)
8165 | (File_kind. S_REG | S_LNK ) when Filename. check_suffix d " .vo"
82- Right (Path. relative path d)
66+ Right (Path. relative dir d)
8367 | _ -> Skip
8468 in
8569 List. filter_partition_map ~f dir_contents
8670
8771(* Note this will only work for absolute paths *)
8872let retrieve_vo_cmxs cps =
89- (List. concat_map ~f: cmxs cps, List. concat_map ~f: vo cps)
73+ ( List. concat_map ~f: cmxs cps
74+ , List. concat_map ~f: cmxs_directories cps
75+ , List. concat_map ~f: vo cps )
76+
77+ module Scan_action = struct
78+ type ('prefix, 'res) t =
79+ dir :Path .t
80+ -> prefix :'prefix
81+ -> subresults :'res list
82+ -> (Filename .t * File_kind .t ) list
83+ -> 'res list Memo .t
84+ end
85+
86+ (* * [scan_path ~f ~acc ~prefix ~dir dir_contents] Given
87+ [f ~dir
88+ ~prefix ~subresults dir_contents], [scan_path] will call [f]
89+ forall the subdirs of [dir] with [dir] set to the subpath, [prefix] set to
90+ [acc prefix d] for each subdirectory [d] and [subresults] the results of the
91+ scanning of children directories *)
92+ let rec scan_path ~(f : ('prefix, 'res) Scan_action.t ) ~acc ~prefix ~dir
93+ dir_contents : 'a list Memo.t =
94+ let open Memo.O in
95+ let f (d , kind ) =
96+ match kind with
97+ (* We skip directories starting by . , this is mainly to avoid
98+ .coq-native *)
99+ | (File_kind. S_DIR | S_LNK ) when d.[0 ] = '.' -> Memo. return []
100+ (* Need to check the link resolves to a directory! *)
101+ | File_kind. S_DIR | S_LNK -> (
102+ let dir = Path. relative dir d in
103+ let * dir_contents =
104+ Fs_memo. dir_contents (Path. as_outside_build_dir_exn dir)
105+ in
106+ match dir_contents with
107+ | Error _ -> Memo. return []
108+ | Ok dir_contents ->
109+ let dir_contents = Fs_cache.Dir_contents. to_list dir_contents in
110+ let prefix = acc prefix d in
111+ let * subresults = scan_path ~f ~acc ~prefix ~dir dir_contents in
112+ f ~dir ~prefix ~subresults dir_contents)
113+ | _ -> Memo. return []
114+ in
115+ Memo.List. concat_map ~f dir_contents
90116
91- (* * [scan_user_path ~prefix path] Note that we already have very similar
92- functionality in [Dir_status] *)
93- let rec scan_path ~f ~acc ~prefix path : 'a list Memo.t =
117+ let scan_path ~f ~acc ~prefix dir =
94118 let open Memo.O in
95119 let * dir_contents =
96- Fs_memo. dir_contents (Path. as_outside_build_dir_exn path )
120+ Fs_memo. dir_contents (Path. as_outside_build_dir_exn dir )
97121 in
98122 match dir_contents with
99123 | Error _ -> Memo. return []
100124 | Ok dir_contents ->
101125 let dir_contents = Fs_cache.Dir_contents. to_list dir_contents in
102- let f (d , kind ) =
103- match kind with
104- | File_kind. S_DIR | S_LNK ->
105- let subpath = Path. relative path d in
106- let prefix = acc prefix d in
107- let * subpaths = scan_path ~f ~acc ~prefix subpath in
108- f ~path ~prefix ~subpath ~subpaths dir_contents
109- | _ -> Memo. return []
126+ scan_path ~f ~acc ~prefix ~dir dir_contents
127+
128+ (* * Scan the plugins in stdlib, returns list of cmxs + list of directories with
129+ cmxs *)
130+ let scan_stdlib_plugins coqcorelib : (Path.t list * Path.t) list Memo.t =
131+ let f ~dir ~prefix :() ~subresults dir_contents =
132+ let cmxs, _ = scan_vo_cmxs ~dir dir_contents in
133+ let res =
134+ match cmxs with
135+ | [] -> subresults
136+ | _ :: _ -> (cmxs, dir) :: subresults
110137 in
111- Memo.List. concat_map ~f dir_contents
112-
113- let scan_user_path path =
114- let f ~path ~prefix ~subpath ~subpaths dir_contents =
115- let cmxs, vo = scan_vo_cmxs ~path dir_contents in
116- let cmxs_r, vo_r = retrieve_vo_cmxs subpaths in
117- let cmxs, vo = (cmxs @ cmxs_r, vo @ vo_r) in
118- Memo. return (build_user_contrib ~cmxs ~vo ~subpath ~name: prefix :: subpaths)
138+ Memo. return res
139+ in
140+ let pluginsdir = Path. relative coqcorelib " plugins" in
141+ let acc _ _ = () in
142+ scan_path ~f ~acc ~prefix: () pluginsdir
143+
144+ (* * [scan_user_path path] Note that we already have very similar functionality
145+ in [Dir_status] *)
146+ let scan_user_path root_path =
147+ let f ~dir ~prefix ~subresults dir_contents =
148+ let cmxs, vo = scan_vo_cmxs ~dir dir_contents in
149+ let cmxs_directories = if not (List. is_empty cmxs) then [ dir ] else [] in
150+ let cmxs_r, cdir_r, vo_r = retrieve_vo_cmxs subresults in
151+ let cmxs, cmxs_directories, vo =
152+ (cmxs @ cmxs_r, cmxs_directories @ cdir_r, vo @ vo_r)
153+ in
154+ Memo. return
155+ (build_user_contrib ~cmxs ~cmxs_directories ~vo ~path: dir ~name: prefix
156+ :: subresults)
119157 in
120- scan_path path ~f ~acc: Coq_lib_name. append ~prefix: Coq_lib_name. empty
158+ scan_path ~f ~acc: Coq_lib_name. append ~prefix: Coq_lib_name. empty root_path
121159
122- let scan_vo path =
123- let f ~path ~prefix :_ ~ subpath : _ ~ subpaths dir_contents =
124- let _, vo = scan_vo_cmxs ~path dir_contents in
125- Memo. return (vo @ subpaths )
160+ let scan_vo root_path =
161+ let f ~dir ~prefix :() ~ subresults dir_contents =
162+ let _, vo = scan_vo_cmxs ~dir dir_contents in
163+ Memo. return (vo @ subresults )
126164 in
127165 let acc _ _ = () in
128- scan_path path ~f ~acc ~prefix: ()
166+ scan_path ~f ~acc ~prefix: () root_path
129167
130168let of_coq_install coqc =
131169 let open Memo.O in
132170 let * coq_config = Coq_config. make ~coqc: (Ok coqc) in
133171 (* Now we query for coqlib *)
134172 let coqlib_path = config_path_exn coq_config " coqlib" in
135173 let coqcorelib = config_path coq_config " coqcorelib" ~default: coqlib_path in
136- let * cmxs = stdlib_plugins_dir coqcorelib in
174+ let * stdlib_plugs = scan_stdlib_plugins coqcorelib in
137175 let * vo = scan_vo coqlib_path in
176+ let cmxs, cmxs_directories = List. split stdlib_plugs in
177+ let cmxs = List. concat cmxs in
138178 let stdlib =
139179 { name = Coq_lib_name. stdlib
140180 ; path = Path. relative coqlib_path " theories"
141181 ; vo
142182 ; cmxs
183+ ; cmxs_directories
143184 ; stdlib = true
144185 }
145186 in
0 commit comments