Commit 53cbbc6d authored by MARCHE Claude's avatar MARCHE Claude

Merge branch '174-reloading-should-interrupt-running-provers' into 'master'

Resolve "Reloading should interrupt running provers"

Closes #174

See merge request !36
parents 4c518b2d 0334be9d
......@@ -513,6 +513,12 @@ let query_call = function
if pid = 0 then NoUpdates else
ProverFinished (editor_result ret)
let interrupt_call = function
| ServerCall id ->
Prove_client.send_interrupt ~id
| EditorCall pid ->
(try Unix.kill pid Sys.sigkill with Unix.Unix_error _ -> ())
let rec wait_on_call = function
| ServerCall id as pc ->
begin match query_result_buffer id with
......@@ -551,5 +557,3 @@ let call_editor ~command fin =
let pid = Unix.create_process exec argarray fd_in Unix.stdout Unix.stderr in
if use_stdin then Unix.close fd_in;
EditorCall pid
let interrupt_call id = Prove_client.send_interrupt ~id
......@@ -177,7 +177,8 @@ val query_call : prover_call -> prover_update
(** non-blocking function that reports any new updates
from the server related to a given prover call. *)
val interrupt_call : prover_call -> unit
(** non-blocking function that asks for prover interruption *)
val wait_on_call : prover_call -> prover_result
(** blocking function that waits until the prover finishes. *)
val interrupt_call : int -> unit
......@@ -170,6 +170,7 @@ let send_interrupt ~id =
Buffer.clear send_buf;
Buffer.add_string send_buf "interrupt;";
Buffer.add_string send_buf (string_of_int id);
Buffer.add_char send_buf '\n';
let s = Buffer.contents send_buf in
send_request_string s
......
......@@ -11,6 +11,7 @@
#include <stdio.h>
#include <stdlib.h>
#include <stdarg.h>
#include "logging.h"
#include "options.h"
......@@ -22,24 +23,21 @@ void init_logging() {
}
}
void log_msg(char* s) {
void log_msg(char* fmt, ...) {
if (logging) {
fprintf (logfile, "%s\n", s);
fflush (logfile);
}
}
void log_msg_len(char* s, int len) {
if (logging) {
fprintf (logfile, "%.*s\n", len, s);
fflush (logfile);
va_list va;
va_start(va, fmt);
vfprintf(logfile, fmt, va);
fprintf(logfile, "\n");
fflush (logfile);
va_end(va);
}
}
void logging_shutdown(char* s) {
if (logging) {
log_msg(s);
fclose(logfile);
log_msg("%s",s);
fclose(logfile);
}
exit(1);
}
......@@ -14,9 +14,7 @@
void init_logging();
void log_msg(char* s);
void log_msg_len(char* s, int len);
void log_msg(char* s, ...) __attribute__ ((format (printf, 1, 2)));
void logging_shutdown(char* s);
#endif
......@@ -64,8 +64,7 @@ prequest parse_request(char* str_req, int len, int key) {
char* tmp;
bool runstdin = false;
log_msg("received query");
log_msg_len(str_req, len);
log_msg("received query %.*s",len,str_req);
semic = count_semicolons(str_req, len);
if (semic == 0) {
......
......@@ -523,6 +523,7 @@ void handle_msg(pclient client, int key) {
break;
case REQ_INTERRUPT:
// removes all occurrences of r->id from the queue
log_msg("Why3 server: removing id '%s' from queue",r->id);
remove_from_queue(r->id);
kill_processes(r->id);
free_request(r);
......
......@@ -402,7 +402,7 @@ void run_request (prequest r) {
NULL,
&si,
&pi)) {
log_msg(cmd);
log_msg("%s",cmd);
CloseHandle(outfilehandle);
CloseHandle(ghJob);
send_msg_to_client(client,
......
......@@ -505,7 +505,10 @@ let timeout_handler () =
let interrupt () =
(* Interrupt provers *)
Hashtbl.iter (fun _k e -> e.tp_callback Interrupted)
Hashtbl.iter
(fun call e ->
Call_provers.interrupt_call call;
e.tp_callback Interrupted)
prover_tasks_in_progress;
Hashtbl.clear prover_tasks_in_progress;
(* Do not interrupt editors
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment