From c45cf997d60ea0b943d09a00f8fef32343650af3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 24 Jan 2020 19:29:29 +0100
Subject: [PATCH] [server] auto-log & server feedback
---
src/plugins/server/kernel_main.ml | 22 ++++++++++++----------
src/plugins/server/main.ml | 14 +++++++++++++-
src/plugins/server/server_parameters.ml | 4 ++--
src/plugins/server/server_parameters.mli | 2 +-
src/plugins/server/server_zmq.ml | 16 ++++------------
5 files changed, 32 insertions(+), 26 deletions(-)
diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml
index af05488f599..119ba52b5e7 100644
--- a/src/plugins/server/kernel_main.ml
+++ b/src/plugins/server/kernel_main.ml
@@ -185,12 +185,8 @@ let monitoring = ref false
let monitored = ref false
let events : Log.event Queue.t = Queue.create ()
-let monitor flag =
+let set_monitoring flag =
if flag != !monitoring then
- ( if flag then
- Senv.feedback "Start logs monitoring."
- else
- Senv.feedback "Stop logs monitoring." ) ;
monitoring := flag ;
if !monitoring && not !monitored then
begin
@@ -198,14 +194,19 @@ let monitor flag =
Log.add_listener (fun evt -> if !monitoring then Queue.add evt events)
end
-let monitor_logs () = monitor (Senv.Log.get ())
-
let monitor_server activity =
- if activity then monitor true else monitor_logs ()
+ if not (Senv.AutoLog.get ()) then set_monitoring activity
+
+let monitor_autologs () =
+ if Senv.AutoLog.get () then
+ begin
+ Senv.feedback "Auto-log started." ;
+ set_monitoring true ;
+ end
let () =
Main.on monitor_server ;
- Cmdline.run_after_configuring_stage monitor_logs
+ Cmdline.run_after_configuring_stage monitor_autologs
(* -------------------------------------------------------------------------- *)
(* --- Log Requests --- *)
@@ -214,7 +215,8 @@ let () =
let () = Request.register
~page ~kind:`SET ~name:"kernel.setLogs"
~descr:(Md.plain "Turn logs monitoring on/off")
- ~input:(module Jbool) ~output:(module Junit) monitor
+ ~input:(module Jbool) ~output:(module Junit)
+ set_monitoring
let () = Request.register
~page ~kind:`GET ~name:"kernel.getLogs"
diff --git a/src/plugins/server/main.ml b/src/plugins/server/main.ml
index 77497270548..0a829101064 100644
--- a/src/plugins/server/main.ml
+++ b/src/plugins/server/main.ml
@@ -286,8 +286,10 @@ let start server =
| Some _db -> ()
| None ->
begin
+ Senv.feedback "Server enabled." ;
let db = !Db.progress in
server.background <- Some db ;
+ signal true ;
Db.progress := do_yield server ;
end
@@ -296,11 +298,21 @@ let stop server =
| None -> ()
| Some db ->
begin
+ Senv.feedback "Server disabled." ;
server.background <- None ;
signal false ;
Db.progress := db ;
end
+let foreground server =
+ match server.background with
+ | None -> ()
+ | Some db ->
+ begin
+ server.background <- None ;
+ Db.progress := db ;
+ end
+
(* -------------------------------------------------------------------------- *)
(* --- Main Loop --- *)
(* -------------------------------------------------------------------------- *)
@@ -309,7 +321,7 @@ let run server =
try
(* TODO: remove the following line once the Why3 signal handler is not
used anymore. *)
- stop server ;
+ foreground server ;
Sys.catch_break true;
signal true ;
Senv.feedback "Server running." ;
diff --git a/src/plugins/server/server_parameters.ml b/src/plugins/server/server_parameters.ml
index 0b00960d594..8ca2d009ce3 100644
--- a/src/plugins/server/server_parameters.ml
+++ b/src/plugins/server/server_parameters.ml
@@ -53,9 +53,9 @@ module Yield = P.Int
let help = EXEC yield period (in milliseconds, default 50ms)"
end)
-module Log = P.False
+module AutoLog = P.False
(struct
- let option_name = "-server-logs"
+ let option_name = "-server-auto-log"
let help = "Start monitoring logs before server is running (default is false)"
end)
diff --git a/src/plugins/server/server_parameters.mli b/src/plugins/server/server_parameters.mli
index 9bbd8a148fd..9d3ef7e958d 100644
--- a/src/plugins/server/server_parameters.mli
+++ b/src/plugins/server/server_parameters.mli
@@ -27,7 +27,7 @@ include Plugin.General_services
module Idle : Parameter_sig.Int (** Idle waiting time (in ms) *)
module Yield : Parameter_sig.Int (** Yield time (in ms) *)
module Doc : Parameter_sig.String (** Generate documentation *)
-module Log : Parameter_sig.Bool (** Monitor logs *)
+module AutoLog : Parameter_sig.Bool (** Monitor logs *)
val wpage : warn_category (** Inconsistent page warning *)
val wkind : warn_category (** Inconsistent category warning *)
diff --git a/src/plugins/server/server_zmq.ml b/src/plugins/server/server_zmq.ml
index 05a2b23d7ec..cb940de721d 100644
--- a/src/plugins/server/server_zmq.ml
+++ b/src/plugins/server/server_zmq.ml
@@ -60,7 +60,7 @@ let zmq_context =
| Some ctxt -> ctxt
| None ->
let major,minor,patch = Zmq.version () in
- Senv.feedback "ZeroMQ %d.%d.%d" major minor patch ;
+ Senv.feedback "ZeroMQ [v%d.%d.%d]" major minor patch ;
let ctxt = Zmq.Context.create () in
at_exit (fun () -> Zmq.Context.terminate ctxt) ;
zmq := Some ctxt ; ctxt
@@ -139,23 +139,15 @@ let cmdline () =
let socket = Zmq.Socket.(create context rep) in
try
Zmq.Socket.bind socket url ;
+ Senv.feedback "ZeroMQ [%s]" url ;
let server = Main.create ~pretty ~fetch:(fetch socket) () in
background := Some server ;
at_exit begin fun () ->
- Senv.feedback "ZeroMQ [%s] stopped" url ;
+ Main.stop server ;
Zmq.Socket.close socket ;
background := None ;
end ;
- if Run.get () then
- begin
- Senv.feedback "ZeroMQ [%s] running" url ;
- Main.run server
- end
- else
- begin
- Senv.feedback "ZeroMQ [%s] started" url ;
- Main.start server
- end
+ if Run.get () then Main.run server else Main.start server ;
with exn ->
Zmq.Socket.close socket ;
raise exn
--
GitLab