From ec5cfc1c57da00876187ebea27e4f5c14ca2feba Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Thu, 28 Aug 2025 11:43:23 +0200 Subject: [PATCH] Introduce a system-wide, parts-oriented configuration file At startup, EasyCrypt now loads all configuration files from `site:config` (default: `lib/easycrypt/config`) with a `.conf` extension. These files are processed in alphabetical order, after the main system-wide configuration file. --- .gitignore | 1 - dune | 2 +- dune-project | 2 +- etc/README | 2 ++ etc/dune | 7 +++++++ src/ec.ml | 47 +++++++++++++++++++++++++++++++++------------- src/ecRelocate.ml | 6 ++++++ src/ecRelocate.mli | 1 + 8 files changed, 52 insertions(+), 16 deletions(-) create mode 100644 etc/README create mode 100644 etc/dune diff --git a/.gitignore b/.gitignore index 099f335d44..035a94f141 100644 --- a/.gitignore +++ b/.gitignore @@ -5,7 +5,6 @@ /_build /result -/etc /theories/attic /ec.* diff --git a/dune b/dune index 7d254fcb7c..e19b69c5a5 100644 --- a/dune +++ b/dune @@ -1,4 +1,4 @@ -(dirs 3rdparty src theories examples scripts) +(dirs 3rdparty src etc theories examples scripts) (install (section (site (easycrypt commands))) diff --git a/dune-project b/dune-project index 298334722c..b285ee1756 100644 --- a/dune-project +++ b/dune-project @@ -10,7 +10,7 @@ (package (name easycrypt) - (sites (lib theories) (libexec commands)) + (sites (lib theories) (libexec commands) (lib config)) (depends (ocaml (>= 4.08.0)) (batteries (>= 3)) diff --git a/etc/README b/etc/README new file mode 100644 index 0000000000..94dc4b0889 --- /dev/null +++ b/etc/README @@ -0,0 +1,2 @@ +; All .conf files in this directory are automatically loaded by EasyCrypt at startup. +; They are processed in alphanumeric order, based on their filenames. diff --git a/etc/dune b/etc/dune new file mode 100644 index 0000000000..881dff3f9f --- /dev/null +++ b/etc/dune @@ -0,0 +1,7 @@ +(install + (section (site (easycrypt config))) + (files (glob_files_rec *.conf))) + +(install + (section (site (easycrypt config))) + (files README)) diff --git a/src/ec.ml b/src/ec.ml index 83633307c5..d61bd43292 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -33,7 +33,7 @@ let why3dflconf = Filename.concat XDG.home "why3.conf" (* -------------------------------------------------------------------- *) type pconfig = { pc_why3 : string option; - pc_ini : string option; + pc_ini : string list; pc_loadpath : (EcLoader.namespace option * string) list; } @@ -63,10 +63,17 @@ let print_config config = | Some f -> Format.eprintf " %s@\n%!" f end; (* Print EC configuration file location *) + Format.eprintf "EasyCrypt system configuration directory@\n%!"; + Format.eprintf " %s@\n%!" Sites.config; + Format.eprintf "EasyCrypt configuration file@\n%!"; begin match config.pc_ini with - | None -> Format.eprintf " @\n%!" - | Some f -> Format.eprintf " %s@\n%!" f end; + | [] -> Format.eprintf " @\n%!" + | names -> + List.iter + (fun name -> Format.eprintf " %s@\n%!" name) + names + end; (* Print list of known provers *) begin @@ -117,8 +124,8 @@ let main () = let (module Sites) = EcRelocate.sites in (* Parse command line arguments *) - let conffile, options = - let conffile = + let conffiles, options = + let sysfile = let xdgini = XDG.Config.file ~exists:true ~mode:`All ~appname:EcVersion.app @@ -131,6 +138,19 @@ let main () = if Sys.file_exists conffile then Some conffile else None) in List.Exceptionless.hd (Option.to_list localini @ xdgini) in + let partfiles = + if Sys.file_exists Sites.config then + Sys.readdir Sites.config + |> Array.to_seq + |> Seq.filter (fun name -> String.lowercase_ascii (Filename.extension name) = ".conf") + |> Seq.map (Filename.concat Sites.config) + |> Seq.filter (fun p -> Sys.file_exists p && not (Sys.is_directory p)) + |> List.of_seq + |> List.sort String.compare + else [] in + + let conffiles = List.ocons sysfile partfiles in + let projfile (path : string option) = let rec find (path : string) : string option = let projfile = Filename.concat path projname in @@ -168,11 +188,12 @@ let main () = let getini (path : string option) = let inisys = - Option.bind conffile (fun conffile -> - Option.map - (fun ini -> { inic_ini = ini; inic_root = None; }) - (read_ini_file conffile) - ) + List.filter_map + (fun conffile -> + Option.map + (fun ini -> { inic_ini = ini; inic_root = None; }) + (read_ini_file conffile)) + conffiles in let iniproj = @@ -186,9 +207,9 @@ let main () = ) in - List.filter_map identity [iniproj; inisys] in + List.ocons iniproj inisys in - (conffile, EcOptions.parse_cmdline ~ini:getini Sys.argv) in + (conffiles, EcOptions.parse_cmdline ~ini:getini Sys.argv) in (* Execution of eager commands *) begin @@ -400,7 +421,7 @@ let main () = | `Config -> let config = { pc_why3 = why3conf; - pc_ini = conffile; + pc_ini = conffiles; pc_loadpath = EcCommands.loadpath (); } in diff --git a/src/ecRelocate.ml b/src/ecRelocate.ml index 869a688785..f07cb429ab 100644 --- a/src/ecRelocate.ml +++ b/src/ecRelocate.ml @@ -23,12 +23,14 @@ let local (name : string list) : string = module type Sites = sig val commands : string val theories : string list + val config : string end (* -------------------------------------------------------------------- *) module LocalSites() : Sites = struct let commands = local ["scripts"; "testing"] let theories = [local ["theories"]] + let config = local ["etc"] end (* -------------------------------------------------------------------- *) @@ -39,6 +41,10 @@ module DuneSites() : Sites = struct let theories = EcDuneSites.Sites.theories + + let config = + Option.value ~default:"etc" + (EcUtils.List.Exceptionless.hd EcDuneSites.Sites.config) end (* -------------------------------------------------------------------- *) diff --git a/src/ecRelocate.mli b/src/ecRelocate.mli index 3ddda071f7..8600315c03 100644 --- a/src/ecRelocate.mli +++ b/src/ecRelocate.mli @@ -5,6 +5,7 @@ val sourceroot : string option module type Sites = sig val commands : string val theories : string list + val config : string end (* -------------------------------------------------------------------- *)