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
|
(************************************************************************)
(* * 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 File_util
let coqc_predicates = ["native"]
module Fl_internals = struct
(** Functions not exported by findlib (XXX there is a copy in mltop, we should share them) *)
(* Fl_split.in_words is not exported *)
let fl_split_in_words s =
(* splits s in words separated by commas and/or whitespace *)
let l = String.length s in
let rec split i j =
if j < l then
match s.[j] with
| (' '|'\t'|'\n'|'\r'|',') ->
if i<j then (String.sub s i (j-i)) :: (split (j+1) (j+1))
else split (j+1) (j+1)
| _ ->
split i (j+1)
else
if i<j then [ String.sub s i (j-i) ] else []
in
split 0 0
(* simulate what fl_dynload does *)
let fl_find_plugins lib =
let base = Findlib.package_directory lib in
let archive = try Findlib.package_property coqc_predicates lib "plugin"
with Not_found ->
try fst (Findlib.package_property_2 ("plugin"::coqc_predicates) lib "archive")
with Not_found -> ""
in
fl_split_in_words archive |> List.map (Findlib.resolve_path ~base)
(* first string is the v file which triggered the error, rest is Fl_package_base.No_such_package *)
exception No_such_package of string * string * string
let () = CErrors.register_handler Pp.(function
| No_such_package(vfile,p,msg) ->
let paths = Findlib.search_path () in
Some (hov 0 (str "In file" ++ spc() ++ str vfile ++ spc() ++
str "findlib error: " ++ str p ++ str " not found in:" ++ cut () ++
v 0 (prlist_with_sep cut str paths) ++ fnl() ++ str msg))
| _ ->
None
)
end
let relative_if_dune path =
(* relativize the path if inside the current dune workspace
if we relativize paths outside the dune workspace it fails so make sure to avoid it *)
match Sys.getenv_opt "DUNE_SOURCEROOT" with
| Some dune when CString.is_prefix (Filename.concat dune "_build") path ->
normalize_path (to_relative_path path)
| _ -> normalize_path path
let findlib_resolve ~package =
let meta_file = Findlib.package_meta_file package in
let cmxss = Fl_internals.fl_find_plugins package in
let meta_file = relative_if_dune meta_file in
let cmxs_file = List.map relative_if_dune cmxss in
(meta_file, cmxs_file)
let static_libs = CString.Set.of_list Static_toplevel_libs.static_toplevel_libs
let findlib_deep_resolve ~package =
let packages = Findlib.package_deep_ancestors coqc_predicates [package] in
let packages = CList.filter (fun package ->
not (CString.Set.mem package static_libs))
packages
in
List.fold_left (fun (metas,cmxss) package ->
let meta, cmxss' = findlib_resolve ~package in
meta :: metas, cmxss' @ cmxss)
([],[])
packages
let findlib_deep_resolve ~file ~package =
try findlib_deep_resolve ~package
with Fl_package_base.No_such_package(p,m) ->
raise (Fl_internals.No_such_package (file,p,m))
module Internal = struct
let get_worker_path () =
let top = "rocqworker" in
let dir = Findlib.package_directory "rocq-runtime" in
let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in
let file = Filename.concat dir (top^exe) in
relative_if_dune file
end
|
