Introduce a system-wide, parts-oriented configuration file

.gitignore

@@ -5,7 +5,6 @@
 
 /_build
 /result
-/etc
 /theories/attic
 
 /ec.*

dune

@@ -1,4 +1,4 @@
-(dirs 3rdparty src theories examples scripts)
+(dirs 3rdparty src etc theories examples scripts)
 
 (install
   (section (site (easycrypt commands)))

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))

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.

etc/dune

@@ -0,0 +1,7 @@
+(install
+  (section (site (easycrypt config)))
+  (files (glob_files_rec *.conf)))
+
+(install
+  (section (site (easycrypt config)))
+  (files README))

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 "  <none>@\n%!"
-  | Some f -> Format.eprintf "  %s@\n%!" f end;
+  | []    -> Format.eprintf "  <none>@\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
 

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
 
 (* -------------------------------------------------------------------- *)

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
 
 (* -------------------------------------------------------------------- *)