Commit 4a41fcab authored by François Bobot's avatar François Bobot

Plugin : absolute path used, autodection added, create directory if needed

parent fbc3ed2b
......@@ -30,7 +30,8 @@ $WHY3LIB and $WHYDATA are used only when a configuration file is created"
(* let libdir = ref None *)
(* let datadir = ref None *)
let conf_file = ref None
let auto = ref false
let autoprovers = ref false
let autoplugins = ref false
let set_oref r = (fun s -> r := Some s)
......@@ -46,8 +47,10 @@ let option_list = Arg.align [
"--conf_file", Arg.String (set_oref conf_file),
"<file> use this configuration file, create it if it doesn't exist
($WHY_CONFIG), otherwise use the default one";
"--autodetect-provers", Arg.Set auto,
"--autodetect-provers", Arg.Set autoprovers,
" autodetect the provers in the $PATH";
"--autodetect-plugins", Arg.Set autoplugins,
" autodetect the plugins in the default library directories";
"--install-plugin", Arg.String add_plugin,
"install a plugin to the actual libdir";
]
......@@ -55,17 +58,35 @@ let option_list = Arg.align [
let anon_file _ = Arg.usage option_list usage_msg; exit 1
let install_plugin main p =
begin match Plugin.check_extension p with
| Plugin.Extbad -> eprintf "Unknown extension (.cmo|.cmxs) : %s@." p;exit 1
| Plugin.Extother ->
eprintf "This plugin %s will not be used with this kind of compilation@."
begin match Plugin.check_plugin p with
| Plugin.Plubad -> eprintf "Unknown extension (.cmo|.cmxs) : %s@." p;
raise Exit
| Plugin.Pluother ->
eprintf "The plugin %s will not be used with this kind of compilation \
and it has not be tested@."
p
| Plugin.Extgood -> ()
| Plugin.Plugood -> ()
| Plugin.Plufail exn -> eprintf "The plugin %s dynlink failed :@.%a@."
p Exn_printer.exn_printer exn; raise Exit
end;
let base = Filename.basename p in
let pluginsdir = Whyconf.pluginsdir main in
Sysutil.copy_file p (Filename.concat pluginsdir base);
Whyconf.add_plugin main (Filename.chop_extension base)
let plugindir = Whyconf.pluginsdir main in
if not (Sys.file_exists plugindir) then Unix.mkdir plugindir 0o777;
let target = (Filename.concat plugindir base) in
if p <> target then Sysutil.copy_file p target;
Whyconf.add_plugin main (Filename.chop_extension target)
let plugins_auto_detection config =
let main = get_main config in
let main = set_plugins main [] in
let dir = Whyconf.pluginsdir main in
let files = Sys.readdir dir in
let fold main p =
let p = Filename.concat dir p in
try eprintf "== Found %s ==@." p;
install_plugin main p with Exit -> main in
let main = Array.fold_left fold main files in
set_main config main
let () =
Arg.parse option_list anon_file usage_msg;
......@@ -81,16 +102,21 @@ let () =
!libdir in *)
(* let main = option_apply main (fun d -> {main with datadir = d})
!datadir in *)
let main = Queue.fold install_plugin main plugins in
let main = try Queue.fold install_plugin main plugins with Exit -> exit 1 in
let config = set_main config main in
let conf_file = get_conf_file config in
let conf_file_doesnt_exist = not (Sys.file_exists conf_file) in
if conf_file_doesnt_exist then
printf "Config file %s doesn't exist, \
so autodetection is automatically triggered@." conf_file;
so autodetection of provers and plugins is automatically triggered@."
conf_file;
let config =
if !auto || conf_file_doesnt_exist
if !autoprovers || conf_file_doesnt_exist
then Autodetection.run_auto_detection config
else config in
let config =
if !autoplugins || conf_file_doesnt_exist
then plugins_auto_detection config
else config in
printf "Save config to %s@." conf_file;
save_config config
......@@ -103,9 +103,8 @@ let add_plugin m p =
let pluginsdir m = Filename.concat m.private_libdir "plugins"
let load_plugins m =
let dirs = [pluginsdir m] in
let load x =
try Plugin.load ~dirs x
try Plugin.load x
with exn ->
Format.eprintf "%s can't be loaded : %a@." x
Exn_printer.exn_printer exn in
......
......@@ -6,6 +6,11 @@ let debug = Debug.register_flag "load_plugin"
exception Plugin_Not_Found of plugin * string list
let loadfile f =
Debug.dprintf debug "Plugin loaded : %s@." f;
Dynlink.loadfile_private f
let add_extension p =
if Dynlink.is_native then p^".cmxs" else p^".cmo"
......@@ -20,25 +25,27 @@ let load ?dirs p =
let f = Filename.concat d p in
if Sys.file_exists f then f else find ld in
find ld in
Debug.dprintf debug "Plugin loaded : %s" f;
Dynlink.loadfile_private f
loadfile f
type ext =
type plu =
(* not a plugin extension *)
| Extbad
| Plubad
(* good plugin extension *)
| Extgood
(* good plugin extension but not the current compilation used *)
| Extother
| Plugood
(* good plugin extension but fail to load *)
| Plufail of exn
(* good plugin extension but not tested *)
| Pluother
let check_extension f =
let check_plugin f =
let cmxs = Filename.check_suffix f ".cmxs" in
let cmo = Filename.check_suffix f ".cmo" in
if not cmxs && not cmo
then Extbad
then Plubad
else
if (if Dynlink.is_native then cmxs else cmo)
then Extgood else Extother
then try loadfile f; Plugood with exn -> Plufail exn
else Pluother
let () =
Exn_printer.register (fun fmt exn ->
......@@ -47,5 +54,5 @@ let () =
Format.fprintf fmt "The plugin %s can't be found in the directories %a"
pl (Pp.print_list Pp.space Pp.string) sl
| Dynlink.Error (error) ->
Format.fprintf fmt "Dynlink error : %s@." (Dynlink.error_message error)
Format.fprintf fmt "Dynlink error : %s" (Dynlink.error_message error)
| _ -> raise exn)
......@@ -13,12 +13,15 @@ val load : ?dirs:string list -> plugin -> unit
plugin named [plugin]. It add the extension .cmo or .cmxs to the
filename according to the compilation used for the main program *)
type ext =
(* not a plugin extension *)
| Extbad
(* good plugin extension *)
| Extgood
(* good plugin extension but not the current compilation used *)
| Extother
val check_extension : plugin -> ext
type plu =
(* not a plugin extension *)
| Plubad
(* good plugin extension *)
| Plugood
(* good plugin extension but fail to load *)
| Plufail of exn
(* good plugin extension but not tested ( other kind of compilation ) *)
| Pluother
val check_plugin : plugin -> plu
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment