From f74e2942a67eb9bd13445af9ac45149534e88deb Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 18 Mar 2021 16:51:08 +0100
Subject: [PATCH] Fix the way a solver's executable is found and used.
---
solver.ml | 182 +++++++++++++++++++++++++++---------------------------
1 file changed, 92 insertions(+), 90 deletions(-)
diff --git a/solver.ml b/solver.ml
index 20feb3e..2856931 100644
--- a/solver.ml
+++ b/solver.ml
@@ -62,45 +62,51 @@ let default_option_of_solver = function
let exe_path_of_solver solver =
let exe = default_exe_name_of_solver solver in
- match Sys.getenv_opt "DIR" with
- | None ->
- begin
- (* We want the complete path of [exe] in $PATH: we use `command -v [exe]'
- and retrieve the result, if any. *)
- let tmp = Filename.temp_file "caisar" "command" in
- let _retcode =
- Sys.command
- (Filename.quote_command
- ~stdout:tmp ~stderr:tmp
- "command" ["-v"; exe])
- in
- let in_channel = Stdlib.open_in tmp in
- let exe = try Stdlib.input_line in_channel with End_of_file -> exe in
- Stdlib.close_in in_channel;
- Sys.remove tmp;
- Ok exe
- end
- | Some dir ->
- (* The env variable should already provide the path to the executable: we
- first check that the path exists, refers to a directory and it is
- absolute, then we concatenate the [exe] name to it. *)
- if not (Sys.file_exists dir && Sys.is_directory dir)
- then
- Error (Format.sprintf "`%s' not exist or is not a directory." dir)
- else
- if Filename.is_relative dir
- then
+ (* We want the complete path of [exe] in $PATH: we use `command -v [exe]'
+ and retrieve the result, if any. *)
+ let tmp = Filename.temp_file "caisar" "command" in
+ let _retcode =
+ Sys.command
+ (Filename.quote_command
+ ~stdout:tmp ~stderr:tmp
+ "command" ["-v"; exe])
+ in
+ let in_channel = Stdlib.open_in tmp in
+ let found, exe =
+ try true, Stdlib.input_line in_channel
+ with End_of_file -> false, exe
+ in
+ Stdlib.close_in in_channel;
+ Sys.remove tmp;
+ if found
+ then Ok exe
+ else begin
+ match Sys.getenv_opt "DIR" with
+ | None ->
Error
- (Format.sprintf
- "`%s' is a relative path. An absolute path is required for DIR."
- dir)
- 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
+ (Format.asprintf "Cannot find the executable of `%a'." pp_solver solver)
+ | Some dir ->
+ (* The env variable should already provide the path to the executable: we
+ first check that the path exists, refers to a directory and it is
+ absolute, then we concatenate the [exe] name to it. *)
+ if not (Sys.file_exists dir && Sys.is_directory dir)
+ then
+ Error (Format.sprintf "`%s' not exist or is not a directory." dir)
+ else
+ if Filename.is_relative dir
+ then
+ Error
+ (Format.sprintf
+ "`%s' is a relative path. An absolute path is required for DIR."
+ dir)
+ 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
+ end
(* Configuration. *)
@@ -192,62 +198,58 @@ let detect_default_solvers () =
let config =
List.filter_map
~f:(fun solver ->
- (* We detect whether solver is available in $PATH, or in the
- provided path via env variable, by executing `solver
- --version' command. *)
- let tmp = Filename.temp_file "caisar" "detect" 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
- exe
- [default_option_of_solver solver]
- in
- Logs.debug
- (fun m -> m "Executing command `%s' to detect `%a'."
- cmd pp_solver solver);
- let retcode = Sys.command cmd in
- let cmd_output =
- let in_channel = Stdlib.open_in tmp in
- let buf = Buffer.create 512 in
- try
- while true do
- Stdlib.Buffer.add_channel buf in_channel 512;
- done;
- assert false
- with End_of_file ->
- Stdlib.close_in in_channel;
- Buffer.contents buf
- in
- Sys.remove tmp;
- if retcode <> 0
- then begin
- Logs.info (fun m -> m "No solver `%a' found." pp_solver solver);
+ match exe_path_of_solver solver with
+ | Error msg ->
+ Logs.info (fun m -> m "%s" msg);
None
- end
- else begin
- (* If available, we save a [config] for solver. *)
- let version = version_of_solver solver cmd_output in
- let config = { solver; exe; version; } in
- Logs.app
- (fun m -> m "Found solver `%a' `%a' (%s)."
- pp_solver solver
- pp_version version
- exe);
- Some config
- end)
+ | Ok exe ->
+ (* We detect whether solver is available in $PATH, or in the
+ provided path via env variable, by executing `solver
+ --version' command. *)
+ let tmp = Filename.temp_file "caisar" "detect" in
+ let cmd =
+ Filename.quote_command
+ ~stdout:tmp ~stderr:tmp
+ exe
+ [default_option_of_solver solver]
+ in
+ Logs.debug
+ (fun m -> m "Executing command `%s' to detect `%a'."
+ cmd pp_solver solver);
+ let retcode = Sys.command cmd in
+ let cmd_output =
+ let in_channel = Stdlib.open_in tmp in
+ let buf = Buffer.create 512 in
+ try
+ while true do
+ Stdlib.Buffer.add_channel buf in_channel 512;
+ done;
+ assert false
+ with End_of_file ->
+ Stdlib.close_in in_channel;
+ Buffer.contents buf
+ in
+ Sys.remove tmp;
+ if retcode <> 0
+ then begin
+ Logs.info (fun m -> m "No solver `%a' found." pp_solver solver);
+ None
+ end
+ else begin
+ (* If available, we save a [config] for solver. *)
+ let version = version_of_solver solver cmd_output in
+ let config = { solver; exe; version; } in
+ Logs.app
+ (fun m -> m "Found solver `%a' `%a' (%s)."
+ pp_solver solver
+ pp_version version
+ exe);
+ Some config
+ end)
defaults
in
Ok config
- with
- | Failure msg ->
- (* Must be only due to the previous use of the [ok_or_failwith]. *)
- Error msg
- | _ ->
+ with _ ->
Error "Unexpected failure."
let detect ~file =
--
GitLab