From e69d03fdfb88930e421e3d8cdf61354650067a69 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 27 Jun 2022 15:40:40 +0200
Subject: [PATCH] [ptests] allows dependencies to ~/.why3.conf
---
ptests/ptests.ml | 14 +++++++++++++-
src/plugins/wp/tests/why3/test_config_qualif | 1 +
2 files changed, 14 insertions(+), 1 deletion(-)
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index aa26cc7bb18..8dbd21f6383 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -1242,9 +1242,20 @@ module Fmt = struct
let var_libavailable pr fmt s = Format.fprintf fmt "%%{lib-available:%a.core}" pr s
let package_as_deps pr fmt s = Format.fprintf fmt "(package %a)" pr s
end
+
+let home_regexp = Str.regexp "^\\(~\\|[$]HOME\\|[$]\\{HOME\\}\\)\\(/.*\\)"
+let get_home_env () =
+ try
+ Unix.getenv "HOME"
+ with Not_found -> "~"
+
let pp_list_deps fmt l =
List.iter (fun s ->
let s = Filename.sanitize_with_space s in
+ let s = match str_string_match2 home_regexp s 0 with
+ | None -> s
+ | Some (_,subdir) -> (get_home_env ()) ^ subdir
+ in
if String.contains s '*' then
Format.fprintf fmt " (glob_files %S)" s
else
@@ -1914,7 +1925,8 @@ let () =
List.iter (fun dir ->
Format.printf "Test directory: %s@." dir;
let absolute_tests_dir = Filename.dirname
- (if Filename.is_relative dir then Filename.concat absolute_cwd dir else dir)
+ (if Filename.is_relative dir
+ then Filename.concat absolute_cwd dir else dir)
in
let suites = Ptests_config.parse ~dir in
if !verbosity >= 1 then Format.printf "%% Nb config= %d@." (StringMap.cardinal suites);
diff --git a/src/plugins/wp/tests/why3/test_config_qualif b/src/plugins/wp/tests/why3/test_config_qualif
index 40a46bc821a..0e60b550835 100644
--- a/src/plugins/wp/tests/why3/test_config_qualif
+++ b/src/plugins/wp/tests/why3/test_config_qualif
@@ -1,4 +1,5 @@
FILEREG: .*\.why
+DEPS: ~/.why3.conf
CMD: why3 -L @PTEST_SHARE_DIR@/why3 prove -P alt-ergo
OPT:
COMMENT: the filter remove the information about time and steps
--
GitLab