From 102562e3a20942e6c7ffb5869bf9abeb0fd2d4b7 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 9 Mar 2021 16:43:10 +0100
Subject: [PATCH] Improve detect option of config command.
- DIR must be set with absolute paths, otherwise an error is displayed.
- Create, write and close the configuration file only if no failure happens
during the detection process (note that empty detection is fine).
---
main.ml | 13 +++++++------
solver.ml | 42 ++++++++++++++++++++++++++++++------------
2 files changed, 37 insertions(+), 18 deletions(-)
diff --git a/main.ml b/main.ml
index c4f1cb2..5a7b015 100644
--- a/main.ml
+++ b/main.ml
@@ -45,8 +45,7 @@ let setup_logs =
(* Commands. *)
-let config cmd detect file_opt () =
- let file = Option.value file_opt ~default:Solver.default_config_file in
+let config cmd detect file () =
Logs.debug
(fun m -> m "Command `%s' with configuration file `%s'." cmd file);
if detect
@@ -81,7 +80,8 @@ let config_cmd =
let dirvar = "DIR" in
let envs =
[ Term.env_info
- ~doc:"Path to directory where to search for the executable of a solver."
+ ~doc:"Absolute path to the directory containing the executable \
+ of a solver."
dirvar ]
in
let detect =
@@ -95,7 +95,7 @@ let config_cmd =
let doc =
Format.sprintf "$(b,FILE) to write the %s configuration to." caisar
in
- Arg.(value & pos 0 (some string) None
+ Arg.(value & pos 0 string Solver.default_config_file
& info [] ~docv:docv_filename ~doc)
in
let doc = Format.sprintf "%s configuration." caisar in
@@ -106,10 +106,11 @@ let config_cmd =
in
Term.(ret
(const (fun cmdname detect filename _ ->
- if not detect && Option.is_none filename
+ if not detect
then `Help (`Pager, Some "config")
else
- (* TODO: Do not enable [detect] by default. *)
+ (* TODO: Do not only check for [detect], and enable it by
+ default, as soon as other options are available. *)
`Ok (config cmdname true filename ()))
$ const cmdname $ detect $ filename $ setup_logs)),
Term.info cmdname ~sdocs:Manpage.s_common_options ~envs ~exits ~doc ~man
diff --git a/solver.ml b/solver.ml
index d23c0ea..da23db8 100644
--- a/solver.ml
+++ b/solver.ml
@@ -7,6 +7,7 @@
open Base
module Format = Caml.Format
module Sys = Caml.Sys
+module Filename = Caml.Filename
(* Supported solvers. *)
type solver =
@@ -66,7 +67,6 @@ let exe_path_of_solver solver =
begin
(* We want the complete path of [exe] in $PATH: we use `command -v [exe]'
and retrieve the result, if any. *)
- let module Filename = Caml.Filename in
let tmp = Filename.temp_file "caisar" "command" in
let _retcode =
Sys.command
@@ -78,12 +78,24 @@ let exe_path_of_solver solver =
let exe = try Stdlib.input_line in_channel with End_of_file -> exe in
Stdlib.close_in in_channel;
Sys.remove tmp;
- exe
+ Ok exe
end
- | Some v ->
+ | Some dir ->
(* The env variable should already provide the path to the executable: we
- just concatenate to it the [exe] name. *)
- v ^ exe
+ first check that the path is absolute, and then concatenate the [exe]
+ name to it. *)
+ if Filename.is_relative dir
+ then
+ Error
+ "Variable DIR is set with a relative path. \
+ An absolute path is required."
+ else
+ let exe =
+ if Filename.check_suffix dir Filename.dir_sep
+ then dir ^ exe
+ else Format.sprintf "%s%s%s" dir Filename.dir_sep exe
+ in
+ Ok exe
(* Configuration. *)
@@ -169,7 +181,6 @@ let create_config_file file =
Stdlib.open_out file
let detect_default_solvers () =
- let module Filename = Caml.Filename in
try
let config =
List.filter_map
@@ -178,7 +189,11 @@ let detect_default_solvers () =
provided path via env variable, by executing `solver
--version' command. *)
let tmp = Filename.temp_file "caisar" "detect" in
- let exe = exe_path_of_solver solver in
+ let exe =
+ (* Failwith upon error case in [exe_path_of_solver] just to
+ propogate the error message to the user. *)
+ Result.ok_or_failwith (exe_path_of_solver solver)
+ in
let cmd =
Filename.quote_command
~stdout:tmp ~stderr:tmp
@@ -212,17 +227,21 @@ let detect_default_solvers () =
defaults
in
Ok config
- with _ ->
+ with
+ | Failure msg ->
+ (* Must be only due to the previous use of the [ok_or_failwith]. *)
+ Error msg
+ | _ ->
Error "Unexpected failure."
let detect ~file =
let open Result in
+ (* Detect default supported solvers in $PATH or $DIR. *)
+ detect_default_solvers () >>= fun default_full_config ->
(* Retrieve the current configuration from [file]. *)
let current_full_config = get_full_config file in
(* Create new configuration file. *)
let out_channel = create_config_file file in
- (* Detect default supported solvers in $PATH or $DIR. *)
- detect_default_solvers () >>= fun default_full_config ->
(* Build [full_config] by first appending [default_full_config] to
[current_full_config], and then deduping the result. *)
let full_config =
@@ -236,13 +255,13 @@ let detect ~file =
(* We write all solver configs in the configuration file, as JSON data. *)
let full_config_json = full_config_to_yojson full_config in
Yojson.Safe.pretty_to_channel out_channel full_config_json;
+ Stdlib.close_out out_channel;
Ok ()
(* Verification. *)
let check_availability config =
- let module Filename = Caml.Filename in
Logs.debug
(fun m -> m "Checking actual availability of `%a'."
pp_solver config.solver);
@@ -287,7 +306,6 @@ let check_compatibility config model =
Ok ()
let build_command ~raw_options confg_solver property model =
- let module Filename = Caml.Filename in
let open Result in
let solver = confg_solver.solver in
(* Format property wrt solver. *)
--
GitLab