From 80c4b67b2c82d8a8dbacd3e2ec16841ec1a63a00 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 1 Jul 2024 09:58:30 +0200
Subject: [PATCH] [kernel] add user directories
---
configurator.ml | 25 ++++-
src/kernel_internals/runtime/macos_dirs.ml | 17 ++++
.../runtime/system_config.ml.in | 4 +
.../runtime/system_config.mli | 12 +++
src/kernel_internals/runtime/unix_dirs.ml | 20 ++++
src/kernel_internals/runtime/win_dirs.ml | 13 +++
.../plugin_entry_points/kernel.ml | 32 ++++++-
.../plugin_entry_points/kernel.mli | 10 ++
.../plugin_entry_points/plugin.ml | 93 +++++++++++++------
.../plugin_entry_points/plugin.mli | 34 ++++++-
src/plugins/gui/gtk_helper.ml | 2 +-
src/plugins/gui/gui_parameters.ml | 2 +
src/plugins/gui/gui_parameters.mli | 2 +
13 files changed, 232 insertions(+), 34 deletions(-)
create mode 100644 src/kernel_internals/runtime/macos_dirs.ml
create mode 100644 src/kernel_internals/runtime/unix_dirs.ml
create mode 100644 src/kernel_internals/runtime/win_dirs.ml
diff --git a/configurator.ml b/configurator.ml
index 5e4c11ec982..87bb3e182bb 100644
--- a/configurator.ml
+++ b/configurator.ml
@@ -234,6 +234,27 @@ module Fc_version = struct
"s|@MINOR_VERSION@|%s|" version.minor
end
+module OS = struct
+ type t = Windows | MacOS | OtherUnix
+
+ let get configurator =
+ match C.ocaml_config_var_exn configurator "os_type" with
+ | "Win32" -> Windows
+ | _ ->
+ match C.ocaml_config_var_exn configurator "system" with
+ | "macosx" -> MacOS
+ | _ -> OtherUnix
+
+ let pp_sed fmt t =
+ let module_dirs = match t with
+ | Windows -> "Win_dirs"
+ | MacOS -> "Macos_dirs"
+ | OtherUnix -> "Unix_dirs"
+ in
+ Format.fprintf fmt
+ "s|@FRAMAC_TARGET_SYSTEM_CONFIG_INCLUDE@|%s|" module_dirs
+end
+
let python_available configurator =
let result = C.Process.run configurator "python3" ["--version"] in
if result.exit_code <> 0 then false
@@ -256,9 +277,11 @@ let python_available configurator =
let configure configurator =
let version = Fc_version.get configurator in
let cpp = Cpp.get configurator in
+ let os = OS.get configurator in
let config_sed = open_out "config.sed" in
let fmt = Format.formatter_of_out_channel config_sed in
- Format.fprintf fmt "%a\n%a\n" Fc_version.pp_sed version Cpp.pp_sed cpp ;
+ Format.fprintf fmt "%a\n%a\n%a\n"
+ Fc_version.pp_sed version Cpp.pp_sed cpp OS.pp_sed os ;
close_out config_sed ;
let python = open_out "python-3.7-available" in
Printf.fprintf python "%b" (python_available configurator) ;
diff --git a/src/kernel_internals/runtime/macos_dirs.ml b/src/kernel_internals/runtime/macos_dirs.ml
new file mode 100644
index 00000000000..042dc2beb92
--- /dev/null
+++ b/src/kernel_internals/runtime/macos_dirs.ml
@@ -0,0 +1,17 @@
+let home () =
+ match Sys.getenv "HOME" with
+ | "" -> raise Not_found
+ | s -> Filepath.Normalized.of_string s
+
+let env_or_default env default =
+ let open Filepath.Normalized in
+ match Sys.getenv_opt env with
+ | Some s when s <> "" -> concat (of_string s) "frama-c"
+ | _ -> concats (home ()) default
+
+let cache () =
+ env_or_default "XDG_CACHE_HOME" [ "Library" ; "Caches" ; "frama-c"]
+let config () =
+ env_or_default "XDG_CONFIG_HOME" [ "Application Support" ; "frama-c" ; "config" ]
+let state () =
+ env_or_default "XDG_STATE_HOME" [ "Application Support" ; "frama-c" ; "state" ]
diff --git a/src/kernel_internals/runtime/system_config.ml.in b/src/kernel_internals/runtime/system_config.ml.in
index fbf4944d659..028fd90f61d 100644
--- a/src/kernel_internals/runtime/system_config.ml.in
+++ b/src/kernel_internals/runtime/system_config.ml.in
@@ -91,3 +91,7 @@ module Preprocessor = struct
let supported_arch_options = [@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@]
end
+
+module User_dirs = struct
+ include @FRAMAC_TARGET_SYSTEM_CONFIG_INCLUDE@
+end
diff --git a/src/kernel_internals/runtime/system_config.mli b/src/kernel_internals/runtime/system_config.mli
index ccceae39226..b0eb095867a 100644
--- a/src/kernel_internals/runtime/system_config.mli
+++ b/src/kernel_internals/runtime/system_config.mli
@@ -112,6 +112,18 @@ module Preprocessor : sig
*)
end
+(** Default user directories *)
+module User_dirs : sig
+ val cache: unit -> Filepath.Normalized.t
+ (** Where Frama-C should read/write cached files. *)
+
+ val config: unit -> Filepath.Normalized.t
+ (** Where Frama-C should read/write config files. *)
+
+ val state: unit -> Filepath.Normalized.t
+ (** Where Frama-C should read/write state files *)
+end
+
val is_gui: bool
(** Is the Frama-C GUI running? *)
diff --git a/src/kernel_internals/runtime/unix_dirs.ml b/src/kernel_internals/runtime/unix_dirs.ml
new file mode 100644
index 00000000000..3ac63d6ef4f
--- /dev/null
+++ b/src/kernel_internals/runtime/unix_dirs.ml
@@ -0,0 +1,20 @@
+let home () =
+ match Sys.getenv "HOME" with
+ | "" -> raise Not_found
+ | s -> Filepath.Normalized.of_string s
+
+let env_or_default env default =
+ let open Filepath.Normalized in
+ let location =
+ match Sys.getenv_opt env with
+ | Some env when env <> "" -> of_string env
+ | _ -> concats (home ()) default
+ in
+ concat location "frama-c"
+
+let cache () =
+ env_or_default "XDG_CACHE_HOME" [ ".cache" ]
+let config () =
+ env_or_default "XDG_CONFIG_HOME" [ ".config" ]
+let state () =
+ env_or_default "XDG_STATE_HOME" [ ".local" ; "state" ]
diff --git a/src/kernel_internals/runtime/win_dirs.ml b/src/kernel_internals/runtime/win_dirs.ml
new file mode 100644
index 00000000000..a8bf5c510e5
--- /dev/null
+++ b/src/kernel_internals/runtime/win_dirs.ml
@@ -0,0 +1,13 @@
+let env_or_default env default sub =
+ let open Filepath.Normalized in
+ match Sys.getenv_opt env, sub with
+ | Some s, _ (* ignored *) when s <> "" -> concat (of_string s) "frama-c"
+ | _, Some sub -> concats (of_string default) [ "frama-c" ; sub ]
+ | _, None -> concat (of_string default) "frama-c"
+
+let cache () =
+ env_or_default "XDG_CACHE_HOME" (Sys.getenv "TEMP") None
+let config () =
+ env_or_default "XDG_CONFIG_HOME" (Sys.getenv "LOCALAPPDATA") (Some "config")
+let state () =
+ env_or_default "XDG_STATE_HOME" (Sys.getenv "LOCALAPPDATA") (Some "state")
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 11f898a7554..50962dcf303 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -973,6 +973,21 @@ module Session_dir =
let () = Plugin.session_is_set_ref := Session_dir.is_set
let () = Plugin.session_ref := Session_dir.get
+let () = Parameter_customize.set_cmdline_stage Cmdline.Extending
+let () = Parameter_customize.set_group saveload
+let () = Parameter_customize.do_not_projectify ()
+module Cache_dir =
+ P.Filepath
+ (struct
+ let option_name = "-cache"
+ let arg_name = "path"
+ let existence = Filepath.Indifferent
+ let file_kind = "directory"
+ let help = "directory in which cache files are stored"
+ end)
+let () = Plugin.cache_is_set_ref := Cache_dir.is_set
+let () = Plugin.cache_ref := Cache_dir.get
+
let () = Parameter_customize.set_cmdline_stage Cmdline.Extending
let () = Parameter_customize.set_group saveload
let () = Parameter_customize.do_not_projectify ()
@@ -983,11 +998,26 @@ module Config_dir =
let arg_name = "path"
let existence = Filepath.Indifferent
let file_kind = "directory"
- let help = "directory in which configuration files are searched"
+ let help = "directory in which configuration files are stored"
end)
let () = Plugin.config_is_set_ref := Config_dir.is_set
let () = Plugin.config_ref := Config_dir.get
+let () = Parameter_customize.set_cmdline_stage Cmdline.Extending
+let () = Parameter_customize.set_group saveload
+let () = Parameter_customize.do_not_projectify ()
+module State_dir =
+ P.Filepath
+ (struct
+ let option_name = "-state"
+ let arg_name = "path"
+ let existence = Filepath.Indifferent
+ let file_kind = "directory"
+ let help = "directory in which state files are stored"
+ end)
+let () = Plugin.state_is_set_ref := State_dir.is_set
+let () = Plugin.state_ref := State_dir.get
+
(* ************************************************************************* *)
(** {2 Parsing} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 13e35743a12..861c22d2901 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -418,12 +418,22 @@ module Session_dir: Parameter_sig.Filepath
@before 23.0-Vanadium parameter type was string instead of Filepath.
*)
+module Cache_dir: Parameter_sig.Filepath
+(** Directory in which cache files are searched.
+ @since Frama-C+dev
+*)
+
module Config_dir: Parameter_sig.Filepath
(** Directory in which config files are searched.
@since Neon-20140301
@before 23.0-Vanadium parameter type was string instead of Filepath.
*)
+module State_dir: Parameter_sig.Filepath
+(** Directory in which state files are searched.
+ @since Frama-C+dev
+*)
+
(* this stop special comment does not work as expected (and as explained in the
OCamldoc manual, Section 15.2.2. It just skips all the rest of the file
instead of skipping until the next stop comment...
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 7d0e44b8cbd..7731ea1766c 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -27,8 +27,12 @@ let empty_string = ""
let positive_debug_ref = ref 0
let session_is_set_ref = Extlib.mk_fun "session_is_set_ref"
let session_ref = Extlib.mk_fun "session_ref"
+let cache_is_set_ref = Extlib.mk_fun "cache_is_set_ref"
+let cache_ref = Extlib.mk_fun "cache_ref"
let config_is_set_ref = Extlib.mk_fun "config_is_set_ref"
let config_ref = Extlib.mk_fun "config_ref"
+let state_is_set_ref = Extlib.mk_fun "state_is_set_ref"
+let state_ref = Extlib.mk_fun "state_ref"
(* ************************************************************************* *)
(** {2 Signatures} *)
@@ -40,7 +44,9 @@ module type S_no_log = sig
module Debug: Parameter_sig.Int
module Share: Parameter_sig.Specific_dir
module Session: Parameter_sig.Specific_dir
- module Config: Parameter_sig.Specific_dir
+ module Cache_dir () : Parameter_sig.Specific_dir
+ module Config_dir () : Parameter_sig.Specific_dir
+ module State_dir () : Parameter_sig.Specific_dir
val help: Cmdline.Group.t
val messages: Cmdline.Group.t
val add_plugin_output_aliases:
@@ -82,8 +88,12 @@ let is_share_visible () = share_visible_ref := true
let session_visible_ref = ref false
let is_session_visible () = session_visible_ref := true
+let cache_visible_ref = ref false
+let is_cache_visible () = cache_visible_ref := true
let config_visible_ref = ref false
let is_config_visible () = config_visible_ref := true
+let state_visible_ref = ref false
+let is_state_visible () = state_visible_ref := true
let plugin_subpath_ref = ref None
let plugin_subpath s = plugin_subpath_ref := Some s
@@ -94,7 +104,9 @@ let reset_plugin () =
kernel := false;
share_visible_ref := false;
session_visible_ref := false;
+ cache_visible_ref := false;
config_visible_ref := false;
+ state_visible_ref := false;
plugin_subpath_ref := None;
default_msg_keys_ref := [];
;;
@@ -466,36 +478,61 @@ struct
let visible_ref = !session_visible_ref
end)
- module Config =
- Make_specific_dir
+ module type User_dir_input = sig
+ val name: string
+ val getter: unit -> Fc_Filepath.Normalized.t
+ val visible_ref: bool ref
+ val kernel_get: unit -> Fc_Filepath.Normalized.t
+ val kernel_is_set: unit -> bool
+ end
+
+ module User_dir (I: User_dir_input) = struct
+ include Make_specific_dir
+ (struct
+ let option_name = I.name
+ let arg_name = "dir"
+ let help = Format.asprintf
+ "set the plug-in %s directory to <dir> \
+ (may be used on systems with no default user directory)"
+ I.name
+ end)
+ (struct
+ let dirs () = [
+ let var = "FRAMAC_" ^ (Stdlib.String.uppercase_ascii I.name) in
+ if I.kernel_is_set () then I.kernel_get ()
+ else match Sys.getenv_opt var with
+ | Some p when p <> "" -> Fc_Filepath.Normalized.of_string p
+ | _ -> I.getter ()
+ ]
+ let visible_ref = !I.visible_ref
+ end)
+ end
+
+ module Cache_dir () = User_dir
(struct
- let option_name = "config"
- let arg_name = "dir"
- let help = "set the plug-in config directory to <dir> \
- (may be used on systems with no default user directory)"
+ let name = "cache"
+ let getter = System_config.User_dirs.cache
+ let visible_ref = cache_visible_ref
+ let kernel_get () = !cache_ref ()
+ let kernel_is_set () = !cache_is_set_ref ()
end)
+
+ module Config_dir () = User_dir
(struct
- let dirs () = [
- let to_path = Fc_Filepath.Normalized.of_string in
- let d, vis =
- if !config_is_set_ref () then !config_ref (), false
- else
- try to_path (Sys.getenv "FRAMAC_CONFIG"), false
- with Not_found ->
- try to_path (Sys.getenv "USERPROFILE"), false (* Win32 *)
- with Not_found ->
- (* Unix like *)
- try to_path (Sys.getenv "XDG_CONFIG_HOME"), true
- with Not_found ->
- try
- Fc_Filepath.Normalized.concat
- (to_path (Sys.getenv "HOME")) ".config", true
- with Not_found -> to_path ".", false
- in
- Fc_Filepath.Normalized.concat
- d (if vis then "frama-c" else ".frama-c")
- ]
- let visible_ref = !config_visible_ref
+ let name = "config"
+ let getter = System_config.User_dirs.config
+ let visible_ref = config_visible_ref
+ let kernel_get () = !config_ref ()
+ let kernel_is_set () = !config_is_set_ref ()
+ end)
+
+ module State_dir () = User_dir
+ (struct
+ let name = "state"
+ let getter = System_config.User_dirs.state
+ let visible_ref = state_visible_ref
+ let kernel_get () = !state_ref ()
+ let kernel_is_set () = !state_is_set_ref ()
end)
let help = add_group "Getting Information"
diff --git a/src/kernel_services/plugin_entry_points/plugin.mli b/src/kernel_services/plugin_entry_points/plugin.mli
index 887bdc5befc..58f69a3f554 100644
--- a/src/kernel_services/plugin_entry_points/plugin.mli
+++ b/src/kernel_services/plugin_entry_points/plugin.mli
@@ -51,9 +51,21 @@ module type S_no_log = sig
@since Neon-20140301 *)
module Session: Parameter_sig.Specific_dir
+ (** Handle the specific `cache' directory of the plug-in.
+ @since Frama-C+dev
+ *)
+ module Cache_dir (): Parameter_sig.Specific_dir
+
(** Handle the specific `config' directory of the plug-in.
- @since Neon-20140301 *)
- module Config: Parameter_sig.Specific_dir
+ @since Neon-20140301
+ @before Frama-C+dev this was not a functor
+ *)
+ module Config_dir (): Parameter_sig.Specific_dir
+
+ (** Handle the specific `state' directory of the plug-in.
+ @since Frama-C+dev
+ *)
+ module State_dir (): Parameter_sig.Specific_dir
val help: Cmdline.Group.t
(** The group containing option -*-help.
@@ -131,8 +143,18 @@ val is_session_visible: unit -> unit
To be called just before applying {!Register} to create plug-in services.
@since Neon-20140301 *)
+val is_cache_visible: unit -> unit
+(** Make visible to the end-user the -<plug-in>-cache-dir option.
+ To be called just before applying {!Register} to create plug-in services.
+ @since Neon-20140301 *)
+
val is_config_visible: unit -> unit
-(** Make visible to the end-user the -<plug-in>-config option.
+(** Make visible to the end-user the -<plug-in>-config-dir option.
+ To be called just before applying {!Register} to create plug-in services.
+ @since Neon-20140301 *)
+
+val is_state_visible: unit -> unit
+(** Make visible to the end-user the -<plug-in>-state-dir option.
To be called just before applying {!Register} to create plug-in services.
@since Neon-20140301 *)
@@ -178,9 +200,15 @@ val positive_debug_ref: int ref
val session_is_set_ref: (unit -> bool) ref
val session_ref: (unit -> Filepath.Normalized.t) ref
+val cache_is_set_ref: (unit -> bool) ref
+val cache_ref: (unit -> Filepath.Normalized.t) ref
+
val config_is_set_ref: (unit -> bool) ref
val config_ref: (unit -> Filepath.Normalized.t) ref
+val state_is_set_ref: (unit -> bool) ref
+val state_ref: (unit -> Filepath.Normalized.t) ref
+
(**/**)
(*
diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml
index 9879790fff9..8a622821768 100644
--- a/src/plugins/gui/gtk_helper.ml
+++ b/src/plugins/gui/gtk_helper.ml
@@ -48,7 +48,7 @@ let framac_logo, framac_icon =
module Configuration = struct
include Cilconfig
let configuration_file () =
- Gui_parameters.Config.get_file ~mode:`Create_path "frama-c-gui.config"
+ Gui_parameters.Config_dir.get_file ~mode:`Create_path "frama-c-gui.config"
let load () = loadConfiguration (configuration_file ())
let save () = saveConfiguration (configuration_file ())
let reset () = Extlib.safe_remove (configuration_file () :> string);
diff --git a/src/plugins/gui/gui_parameters.ml b/src/plugins/gui/gui_parameters.ml
index 70882c2143a..4284fb0a1a6 100644
--- a/src/plugins/gui/gui_parameters.ml
+++ b/src/plugins/gui/gui_parameters.ml
@@ -28,6 +28,8 @@ include Plugin.Register
let help = "Graphical User Interface"
end)
+module Config_dir = Config_dir ()
+
let () = Parameter_customize.do_not_projectify ()
module Project_name =
Empty_string
diff --git a/src/plugins/gui/gui_parameters.mli b/src/plugins/gui/gui_parameters.mli
index ecc785aeda0..2c665e2dc1b 100644
--- a/src/plugins/gui/gui_parameters.mli
+++ b/src/plugins/gui/gui_parameters.mli
@@ -24,6 +24,8 @@
include Plugin.S
+module Config_dir : Parameter_sig.Specific_dir
+
module Project_name: Parameter_sig.String
(** Option -gui-project. *)
--
GitLab