# HG changeset patch # User wenzelm # Date 1585850803 -7200 # Node ID 4d2de35214c51f9563ced83336be67dd337c340c # Parent e15ca98ffbfe4fc0e6110419cfb63ffe93f0da11 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image; diff -r e15ca98ffbfe -r 4d2de35214c5 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Thu Apr 02 13:04:24 2020 +0200 +++ b/src/Pure/PIDE/session.scala Thu Apr 02 20:06:43 2020 +0200 @@ -705,22 +705,17 @@ }) } - def send_stop() + def stop(): Process_Result = { val was_ready = - _phase.guarded_access(phase => - phase match { + _phase.guarded_access( + { case Session.Startup | Session.Shutdown => None case Session.Terminated(_) => Some((false, phase)) case Session.Inactive => Some((false, post_phase(Session.Terminated(Process_Result(0))))) case Session.Ready => Some((true, post_phase(Session.Shutdown))) }) if (was_ready) manager.send(Stop) - } - - def stop(): Process_Result = - { - send_stop() prover.await_reset() change_parser.shutdown() diff -r e15ca98ffbfe -r 4d2de35214c5 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Thu Apr 02 13:04:24 2020 +0200 +++ b/src/Pure/System/isabelle_process.ML Thu Apr 02 20:06:43 2020 +0200 @@ -7,9 +7,10 @@ signature ISABELLE_PROCESS = sig val is_active: unit -> bool + exception STOP + exception EXIT of int val protocol_command: string -> (string list -> unit) -> unit val reset_tracing: Document_ID.exec -> unit - exception EXIT of int val crashes: exn list Synchronized.var val init_options: unit -> unit val init_options_interactive: unit -> unit @@ -35,6 +36,11 @@ (* protocol commands *) +exception STOP; +exception EXIT of int; + +val is_protocol_exn = fn STOP => true | EXIT _ => true | _ => false; + local val commands = @@ -54,7 +60,9 @@ NONE => error ("Undefined Isabelle protocol command " ^ quote name) | SOME cmd => (Runtime.exn_trace_system (fn () => cmd args) - handle _ (*sic!*) => error ("Isabelle protocol command failure: " ^ quote name))); + handle exn => + if is_protocol_exn exn then Exn.reraise exn + else error ("Isabelle protocol command failure: " ^ quote name))); end; @@ -98,8 +106,6 @@ (* init protocol -- uninterruptible *) -exception EXIT of int; - val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list); local @@ -181,14 +187,15 @@ fun protocol_loop () = let - val continue = + val _ = (case Byte_Message.read_message in_stream of - NONE => false - | SOME [] => (Output.system_message "Isabelle process: no input"; true) - | SOME (name :: args) => (run_command name args; true)) - handle exn as EXIT _ => Exn.reraise exn - | exn => (Runtime.exn_system_message exn handle crash => recover crash; true); - in if continue then protocol_loop () else () end; + NONE => raise STOP + | SOME [] => Output.system_message "Isabelle process: no input" + | SOME (name :: args) => run_command name args) + handle exn => + if is_protocol_exn exn then Exn.reraise exn + else (Runtime.exn_system_message exn handle crash => recover crash); + in protocol_loop () end; fun protocol () = (Session.init_protocol_handlers (); @@ -205,9 +212,11 @@ val _ = Message_Channel.shutdown msg_channel; val _ = BinIO.closeIn in_stream; val _ = BinIO.closeOut out_stream; + in (case result of - Exn.Exn (EXIT rc) => exit rc + Exn.Exn STOP => () + | Exn.Exn (EXIT rc) => exit rc | _ => Exn.release result) end); diff -r e15ca98ffbfe -r 4d2de35214c5 src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Thu Apr 02 13:04:24 2020 +0200 +++ b/src/Pure/System/isabelle_process.scala Thu Apr 02 20:06:43 2020 +0200 @@ -70,5 +70,10 @@ case err => session.stop(); error(err) } - def join(): Process_Result = terminated.join -} \ No newline at end of file + def await_shutdown(): Process_Result = + { + val result = terminated.join + session.stop() + result + } +} diff -r e15ca98ffbfe -r 4d2de35214c5 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Thu Apr 02 13:04:24 2020 +0200 +++ b/src/Pure/Tools/build.ML Thu Apr 02 20:06:43 2020 +0200 @@ -254,13 +254,16 @@ let val args = decode_args args_yxml; val errs = - Future.interruptible_task (fn () => - (build_session args; []) handle exn => + Future.interruptible_task (fn () => (build_session args; [])) () handle exn => (Runtime.exn_message_list exn handle _ (*sic!*) => (build_session_finished ["CRASHED"]; - raise Isabelle_Process.EXIT 1))) (); + raise Isabelle_Process.EXIT 2)); val _ = build_session_finished errs; - in if null errs then () else raise Isabelle_Process.EXIT 1 end + in + if null errs + then raise Isabelle_Process.STOP + else raise Isabelle_Process.EXIT 1 + end | _ => raise Match); end; diff -r e15ca98ffbfe -r 4d2de35214c5 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Thu Apr 02 13:04:24 2020 +0200 +++ b/src/Pure/Tools/build.scala Thu Apr 02 20:06:43 2020 +0200 @@ -166,7 +166,6 @@ } catch { case ERROR(err) => List(err) } build_session_errors.fulfill(errors) - session.send_stop() true } @@ -297,8 +296,9 @@ cwd = info.dir.file, env = env).await_startup session.protocol_command("build_session", args_yxml) + val errors = handler.build_session_errors.join - val process_result = process.join + val process_result = process.await_shutdown val process_output = stdout.toString :: messages.toList ::: command_timings.toList.map(Protocol.Command_Timing_Marker.apply) ::: @@ -307,12 +307,11 @@ task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) val result = process_result.output(process_output) - handler.build_session_errors.join match { - case Nil => result - case errors => - result.error_rc.output( - errors.flatMap(s => split_lines(Output.error_message_text(s))) ::: - errors.map(Protocol.Error_Message_Marker.apply)) + if (errors.isEmpty) result + else { + result.error_rc.output( + errors.flatMap(s => split_lines(Output.error_message_text(s))) ::: + errors.map(Protocol.Error_Message_Marker.apply)) } } else {