From 3be7cb90d01d64d9845a7488f1b5d9d662279702 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Fri, 24 Nov 2023 15:20:34 +0100
Subject: [PATCH] Support project-local ini files

EasyCrypt now reads project-local files for getting its configuration
settings. This configuration file takes precedence over the
system-level configuration file.

The project-local configuration file is named 'easycrypt.project'.  It
is identical to the system-level configuration file.

When compiling a file, the configuration file is searched upward from
the target file directory. When ran in interactive mode, the
configuration file is searched upward from the current working
directory.

Note that when ProofGeneral starts EasyCrypt, the working directory is
set to the directory of the focused file.
---
 src/ec.ml         |  68 +++++++++++++++---
 src/ecOptions.ml  | 173 ++++++++++++++++++++++++++++++++++++++--------
 src/ecOptions.mli |  11 ++-
 3 files changed, 211 insertions(+), 41 deletions(-)

diff --git a/src/ec.ml b/src/ec.ml
index 3fe4ce3152..4a76f5eb94 100644
--- a/src/ec.ml
+++ b/src/ec.ml
@@ -27,6 +27,7 @@ let psep = match Sys.os_type with "Win32" -> ";" | _ -> ":"
 
 (* -------------------------------------------------------------------- *)
 let confname    = "easycrypt.conf"
+let projname    = "easycrypt.project"
 let why3dflconf = Filename.concat XDG.home "why3.conf"
 
 (* -------------------------------------------------------------------- *)
@@ -121,17 +122,64 @@ let main () =
             if Sys.file_exists conffile then Some conffile else None) in
       List.Exceptionless.hd (Option.to_list localini @ xdgini) in
 
-    let ini =
-      Option.bind conffile (fun ini ->
-        try  Some (EcOptions.read_ini_file ini)
-        with
-        | Sys_error _ -> None
-        | EcOptions.InvalidIniFile (lineno, file) ->
-            Format.eprintf "%s:%l: cannot read INI file@." file lineno;
-            exit 1
-      )
+    let projfile (path : string option) =
+      let rec find (path : string) : string option =
+        let projfile = Filename.concat path projname in
+        if Sys.file_exists projfile then
+          Some projfile
+        else
+          if Filename.dirname path = path then
+            None
+          else
+            find (Filename.dirname path)
+      in
+
+      let root =
+        match path with
+        | Some path ->
+           Filename.dirname path
+        | None ->
+           Unix.getcwd () in
+
+      let root =
+        if   Filename.is_relative root
+        then Filename.concat (Unix.getcwd ()) root
+        else root in
+
+      find root in
+
+    let read_ini_file ini =
+      try  Some (EcOptions.read_ini_file ini)
+      with
+      | Sys_error _ -> None
+      | EcOptions.InvalidIniFile (lineno, file) ->
+          Format.eprintf "%s:%l: cannot read INI file@." file lineno;
+          exit 1
+    in
 
-    in (conffile, EcOptions.parse_cmdline ?ini Sys.argv) in
+    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)
+        )
+      in
+
+      let iniproj =
+        Option.bind (projfile path) (fun conffile ->
+          Option.map
+            (fun ini -> {
+               inic_ini  = ini;
+               inic_root = Some (Filename.dirname conffile);
+            })
+            (read_ini_file conffile)
+        )
+      in
+
+      List.filter_map identity [iniproj; inisys] in
+
+    (conffile, EcOptions.parse_cmdline ~ini:getini Sys.argv) in
 
   (* Execution of eager commands *)
   begin
diff --git a/src/ecOptions.ml b/src/ecOptions.ml
index e214abef5d..22605e2c5a 100644
--- a/src/ecOptions.ml
+++ b/src/ecOptions.ml
@@ -70,6 +70,94 @@ type ini_options = {
   ini_rdirs    : (string option * string) list;
 }
 
+type ini_context = {
+  inic_ini  : ini_options;
+  inic_root : string option;
+}
+
+(* -------------------------------------------------------------------- *)
+module Ini : sig
+  (* ------------------------------------------------------------------ *)
+  val get_ppwidth : ini_context -> int option
+
+  val get_why3 : ini_context -> string option
+
+  val get_ovrevict : ini_context -> string list
+
+  val get_provers : ini_context -> string list
+
+  val get_idirs : ini_context -> (string option * string) list
+
+  val get_rdirs : ini_context -> (string option * string) list
+
+  (* ------------------------------------------------------------------ *)
+  val get_all_ppwidth : ini_context list -> int option
+
+  val get_all_why3 : ini_context list -> string option
+
+  val get_all_ovrevict : ini_context list -> string list
+
+  val get_all_provers : ini_context list -> string list
+
+  val get_all_idirs : ini_context list -> (string option * string) list
+
+  val get_all_rdirs : ini_context list -> (string option * string) list
+end = struct
+  (* ------------------------------------------------------------------ *)
+  let absolute ?(root : string option) (filename : string) =
+    match root with
+    | None ->
+       filename
+    | Some root ->
+       if Filename.is_relative filename then
+         Filename.concat root filename
+       else
+         filename
+
+  let get_ppwidth (ini : ini_context) =
+    ini.inic_ini.ini_ppwidth
+
+  let get_why3 (ini : ini_context) =
+    Option.map
+      (absolute ?root:ini.inic_root)
+      (ini.inic_ini.ini_why3)
+
+  let get_ovrevict (ini : ini_context) =
+    ini.inic_ini.ini_ovrevict
+
+  let get_provers (ini : ini_context) =
+    ini.inic_ini.ini_provers
+
+  let get_idirs (ini : ini_context) =
+    List.map
+      (snd_map (absolute ?root:ini.inic_root))
+      ini.inic_ini.ini_idirs
+
+  let get_rdirs (ini : ini_context) =
+    List.map
+      (snd_map (absolute ?root:ini.inic_root))
+      ini.inic_ini.ini_rdirs
+
+  (* ------------------------------------------------------------------ *)
+  let get_all_ppwidth (ini : ini_context list) =
+    List.find_map_opt get_ppwidth ini
+
+  let get_all_why3 (ini : ini_context list) =
+    List.find_map_opt get_why3 ini
+
+  let get_all_ovrevict (ini : ini_context list) =
+    List.flatten (List.map get_ovrevict ini)
+
+  let get_all_provers (ini : ini_context list) =
+    List.flatten (List.map get_provers ini)
+
+  let get_all_idirs (ini : ini_context list) =
+    List.flatten (List.map get_idirs ini)
+
+  let get_all_rdirs (ini : ini_context list) =
+    List.flatten (List.map get_rdirs ini)
+end
+
 (* -------------------------------------------------------------------- *)
 type xoptions = {
   xp_globals  : xspec list;
@@ -327,43 +415,42 @@ let dirs_of_env =
   | s -> parse_ecpath s
 
 (* -------------------------------------------------------------------- *)
-let ldr_options_of_values ?ini values =
+let ldr_options_of_values ?(ini = []) values =
   if get_flag "boot" values then
     { ldro_idirs = []; ldro_boot = true; }
   else
     let add_rec (fl : bool) ((nm, x) : string option * string) =
       (nm, x, fl) in
 
-    let idirs   = omap_dfl (fun x -> x.ini_idirs) [] ini in
-    let idirs = idirs @ dirs_of_env "EC_IDIRS" in
+    let idirs   = Ini.get_all_idirs ini in
+    let idirs   = idirs @ dirs_of_env "EC_IDIRS" in
     let idirs   = List.map (add_rec false) idirs in
     let idirs_I = List.map (add_rec false) (List.map parse_idir (get_strings "I" values)) in
-    let rdirs   = omap_dfl (fun x -> x.ini_rdirs) [] ini in
-    let rdirs = rdirs @ dirs_of_env "EC_RDIRS" in
+    let rdirs   = Ini.get_all_rdirs ini in
+    let rdirs   = rdirs @ dirs_of_env "EC_RDIRS" in
     let rdirs   = List.map (add_rec true) rdirs in
     let idirs_R = List.map (add_rec true)  (List.map parse_idir (get_strings "R" values)) in
 
     { ldro_idirs = idirs @ idirs_I @ rdirs @ idirs_R;
       ldro_boot  = false; }
 
-let glb_options_of_values ?ini values =
+let glb_options_of_values ini values =
   let why3 =
     match get_string "why3" values with
-    | None -> obind (fun x -> x.ini_why3) ini
+    | None -> Ini.get_all_why3 ini
     | why3 -> why3 in
 
-  let ovrevict = omap_dfl (fun x -> x.ini_ovrevict) [] ini in
+  let ovrevict = Ini.get_all_ovrevict ini in
 
   { o_why3     = why3;
     o_reloc    = get_flag "reloc" values;
     o_ovrevict = ovrevict @ (get_strings "no-evict" values);
-    o_loader   = ldr_options_of_values ?ini values; }
+    o_loader   = ldr_options_of_values ~ini values; }
 
-let prv_options_of_values ?ini values =
+let prv_options_of_values ini values =
   let provers =
     let provers =
-      (omap_dfl (fun x -> x.ini_provers) [] ini) @
-      (get_strings "p" values)
+      (Ini.get_all_provers ini) @ (get_strings "p" values)
     in match provers with [] -> None | provers -> Some provers
   in
     { prvo_maxjobs   = odfl 4 (get_int "max-provers" values);
@@ -373,7 +460,7 @@ let prv_options_of_values ?ini values =
       prvo_pragmas   = get_string_list "pragmas" values;
       prvo_ppwidth   = begin
         match get_int "pp-width" values with
-        | None -> obind (fun x -> x.ini_ppwidth) ini
+        | None -> Ini.get_all_ppwidth ini
         | Some i -> Some i
       end;
       prvo_checkall   = get_flag "check-all" values;
@@ -382,54 +469,79 @@ let prv_options_of_values ?ini values =
       prvo_why3server = get_string "why3server" values;
     }
 
-let cli_options_of_values ?ini values =
+let cli_options_of_values ini values =
   { clio_emacs   = get_flag "emacs" values;
-    clio_provers = prv_options_of_values ?ini values; }
+    clio_provers = prv_options_of_values ini values; }
 
-let cmp_options_of_values ?ini values input =
+let cmp_options_of_values ini values input =
   { cmpo_input   = input;
-    cmpo_provers = prv_options_of_values ?ini values;
+    cmpo_provers = prv_options_of_values ini values;
     cmpo_gcstats = get_flag "gcstats" values;
     cmpo_tstats  = get_string "tstats" values;
     cmpo_noeco   = get_flag "no-eco" values;
     cmpo_script  = get_flag "script" values; }
 
 (* -------------------------------------------------------------------- *)
-let parse ?ini argv =
+let parse getini argv =
   let (command, values, anons) = parse specs argv in
-  let command =
+  let command, ini =
     match command with
     | "compile" -> begin
         match anons with
-        | [input] -> `Compile (cmp_options_of_values ?ini values input)
-        | _ -> raise (Arg.Bad "this command takes a single argument")
+        | [input] ->
+           let ini = getini (Some input) in
+           let cmd = `Compile (cmp_options_of_values ini values input) in
+           (cmd, ini)
+
+        | _ ->
+           raise (Arg.Bad "this command takes a single argument")
     end
 
     | "cli" ->
         if not (List.is_empty anons) then
           raise (Arg.Bad "this command does not take arguments");
-        `Cli (cli_options_of_values ?ini values)
+
+        let ini = getini None in
+        let cmd = `Cli (cli_options_of_values ini values) in
+
+        (cmd, ini)
 
     | "config" ->
         if not (List.is_empty anons) then
           raise (Arg.Bad "this command does not take arguments");
-        `Config
+
+        let ini = getini None in
+        let cmd = `Config in
+
+        (cmd, ini)
 
     | "runtest" -> begin
         match anons with
-        | runo_input :: runo_scenarios -> `Runtest { runo_input; runo_scenarios; }
-        | _ -> raise (Arg.Bad "this command expects at least one positional argument")
+        | runo_input :: runo_scenarios ->
+           let ini = getini None in
+           let cmd = `Runtest { runo_input; runo_scenarios; } in
+
+           (cmd, ini)
+
+        | _ ->
+           raise (Arg.Bad "this command expects at least one positional argument")
       end
 
     | "why3config" ->
         if not (List.is_empty anons) then
           raise (Arg.Bad "this command does not take arguments");
-        `Why3Config
+
+        let ini = getini None in
+        let cmd = `Why3Config in
+
+        (cmd, ini)
 
     | _ -> assert false
-  in
-    { o_options = glb_options_of_values ?ini values;
-      o_command = command; }
+
+  in {
+    o_options = glb_options_of_values ini values;
+    o_command = command;
+  }
 
 (* -------------------------------------------------------------------- *)
 let parse_cmdline ?ini argv =
@@ -464,7 +576,8 @@ let parse_cmdline ?ini argv =
          | 1 -> cmd
          | i -> argv.(i-1))
   in
-    try parse ?ini argv
+    try
+      parse (Option.value ~default:(fun _ -> []) ini) argv
     with
     | Arg.Bad  msg -> print_usage ~msg specs; exit 1
     | Arg.Help _   -> print_usage specs; exit 1
diff --git a/src/ecOptions.mli b/src/ecOptions.mli
index b12f113919..937865ba44 100644
--- a/src/ecOptions.mli
+++ b/src/ecOptions.mli
@@ -66,8 +66,17 @@ type ini_options = {
   ini_rdirs    : (string option * string) list;
 }
 
+type ini_context = {
+  inic_ini  : ini_options;
+  inic_root : string option;
+}
+
 (* -------------------------------------------------------------------- *)
 exception InvalidIniFile of (int * string)
 
 val read_ini_file : string -> ini_options
-val parse_cmdline : ?ini:ini_options -> string array -> options
+
+val parse_cmdline :
+     ?ini:(string option -> ini_context list)
+  -> string array
+  -> options