From c8976261ded274e12ac15f2fa8ca656c4752b96c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 18 Jan 2024 11:03:29 +0100
Subject: [PATCH] [wp] server activity detection (gui mode)
---
src/plugins/wp/Cache.ml | 3 ++-
src/plugins/wp/register.ml | 4 ++--
src/plugins/wp/wp_parameters.ml | 16 ++++++++--------
src/plugins/wp/wp_parameters.mli | 1 +
4 files changed, 13 insertions(+), 11 deletions(-)
diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml
index 5e7988978a2..13abb8a0a55 100644
--- a/src/plugins/wp/Cache.ml
+++ b/src/plugins/wp/Cache.ml
@@ -37,7 +37,8 @@ let get_miss () = !miss
let get_removed () = !removed
let mark_cache ~mode hash =
- if mode = Cleanup || Fc_config.is_gui then Hashtbl.replace cleanup hash ()
+ if mode = Cleanup || Wp_parameters.is_interactive () then
+ Hashtbl.replace cleanup hash ()
module CACHEDIR = WpContext.StaticGenerator(Datatype.Unit)
(struct
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index f34d944f7d8..da4a68995e9 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -389,7 +389,7 @@ let do_wpo_success ~shell ~cache goal success =
Wp_parameters.feedback ~ontty:`Silent
"[Generated] Goal %s (%a)" (Wpo.get_gid goal) VCS.pp_prover prover
else
- let gui = Frama_c_very_first.Gui_init.is_gui in
+ let gui = Wp_parameters.is_interactive () in
let smoke = Wpo.is_smoke_test goal in
let cstats = ProofEngine.consolidated ~computing:false goal in
let success = Wpo.is_passed goal in
@@ -874,7 +874,7 @@ let () = Cmdline.run_after_setting_files
let () = Cmdline.run_after_configuring_stage Why3Provers.configure
let do_prover_detect () =
- if not Fc_config.is_gui && Wp_parameters.Detect.get () then
+ if Wp_parameters.Detect.get () && not @@ Wp_parameters.is_interactive () then
let provers = Why3Provers.provers () in
if provers = [] then
Wp_parameters.result "No Why3 provers detected."
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index fa160ed4b0a..4ee4f2b30c9 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -45,6 +45,10 @@ let on_reset f = resetdemon := f :: !resetdemon
let reset () = List.iter (fun f -> f ()) !resetdemon
let has_dkey (k:category) = is_debug_key_enabled k
+let server = ref false
+let () = Server.Main.once (fun () -> server := true)
+let is_interactive () = Fc_config.is_gui || !server
+
(* ------------------------------------------------------------------------ *)
(* --- WP Generation --- *)
(* ------------------------------------------------------------------------ *)
@@ -1206,17 +1210,13 @@ let base_output () =
let output =
let dir = OutputDir.get () in
if Fc_Filepath.Normalized.is_empty dir then
- if Fc_config.is_gui
+ if is_interactive ()
then make_gui_dir ()
else make_tmp_dir ()
- else begin
- make_output_dir dir ;
- dir
- end
- in
+ else
+ ( make_output_dir dir ; dir ) in
base_output := Some output;
- Fc_Filepath.(add_symbolic_dir "WPOUT" output) ;
- output
+ Fc_Filepath.add_symbolic_dir "WPOUT" output ; output
| Some output -> output
let get_output () =
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index ee692cfe9f0..d67f4b9cff3 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -24,6 +24,7 @@ include Plugin.S
val reset : unit -> unit
val hypothesis : 'a Log.pretty_printer
+val is_interactive : unit -> bool
(** {2 Function Selection} *)
--
GitLab