Skip to content

Commit

Permalink
Support project-local ini files
Browse files Browse the repository at this point in the history 
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.
  • Loading branch information
@strub
strub committed Nov 24, 2023
1 parent 9fd429a commit 3be7cb9
Show file tree
Hide file tree
Showing 3 changed files with 211 additions and 41 deletions.
68 changes: 58 additions & 10 deletions src/ec.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"

(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -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
Expand Down
173 changes: 143 additions & 30 deletions src/ecOptions.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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);
Expand All @@ -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;
Expand All @@ -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 =
Expand Down Expand Up @@ -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
Expand Down
11 changes: 10 additions & 1 deletion src/ecOptions.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit 3be7cb9

Please sign in to comment.