From 867d056efcf4647629c14821d4482e2fafbae6c6 Mon Sep 17 00:00:00 2001 From: Dominique Unruh Date: Mon, 8 Jul 2024 11:10:12 +0200 Subject: [PATCH] Fixed startup code to work with Isabelle2024. --- .../Scala_Isabelle_Master_Control_Program.thy | 35 ++++++++++++++++++- .../isabelle/control/control_isabelle.ml | 20 +++++------ .../control/control_isabelle_logged.ml | 20 +++++------ 3 files changed, 54 insertions(+), 21 deletions(-) diff --git a/src/main/resources/de/unruh/isabelle/control/Scala_Isabelle_Master_Control_Program.thy b/src/main/resources/de/unruh/isabelle/control/Scala_Isabelle_Master_Control_Program.thy index 4b12234..34775b2 100644 --- a/src/main/resources/de/unruh/isabelle/control/Scala_Isabelle_Master_Control_Program.thy +++ b/src/main/resources/de/unruh/isabelle/control/Scala_Isabelle_Master_Control_Program.thy @@ -2,6 +2,39 @@ theory Scala_Isabelle_Master_Control_Program imports Pure begin +(* run_one_of_these_ml will try to compile and execute all the given ML fragments + until one of them successfully compiles and executes. *) +ML \ +fun run_one_of_these_ml mls = let + val errors = Unsynchronized.ref [] + fun run_single ml = + Context.>> (Local_Theory.touch_ml_env #> ML_Context.exec (fn () => + ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) ml) #> + Local_Theory.propagate_ml_env) + fun run [] = raise ERROR ("Could not run any of the ML codes. Errors were:\n" ^ + String.concatWith "\n" (!errors)) + | run (ml::mls) = run_single ml + handle ERROR e => (errors := e :: !errors; run mls) +in + run mls +end +\ + +(* Define compatibility aliases for Mutex.mutex and friends. + For use in control_isabelle.ml only *) +ML \ +run_one_of_these_ml [ + \type mcp_mutex = Mutex.mutex val mcp_mutex = Mutex.mutex val mcp_mutex_lock = Mutex.lock val mcp_mutex_unlock = Mutex.unlock\, + \type mcp_mutex = Thread.Mutex.mutex val mcp_mutex = Thread.Mutex.mutex val mcp_mutex_lock = Thread.Mutex.lock val mcp_mutex_unlock = Thread.Mutex.unlock\] +\ + +(* Do the equivalent of `declare [[ML_catch_all = true]]`, but without error if it fails *) +ML \ +run_one_of_these_ml [\Context.>> (Context.map_theory (Config.put_global ML_Compiler.ML_catch_all true))\, + \\] +\ + + ML_file "control_isabelle.ml" ML \ @@ -9,7 +42,7 @@ let val path = File.platform_path (Path.explode "WORKING_DIRECTORY") in OS.FileSys.chDir path - handle OS.SysErr (msg,_) => error ("Could set Isabelle working directory as " ^ path ^ ": " ^ msg) + handle OS.SysErr (msg,_) => error ("Could not set Isabelle working directory as " ^ path ^ ": " ^ msg) end \ diff --git a/src/main/resources/de/unruh/isabelle/control/control_isabelle.ml b/src/main/resources/de/unruh/isabelle/control/control_isabelle.ml index 5eafbe0..65edc3b 100644 --- a/src/main/resources/de/unruh/isabelle/control/control_isabelle.ml +++ b/src/main/resources/de/unruh/isabelle/control/control_isabelle.ml @@ -26,7 +26,7 @@ structure Control_Isabelle : sig exception E_ToplevelState of Toplevel.state exception E_Transition of Toplevel.transition exception E_Keywords of Thy_Header.keywords - exception E_Mutex of Mutex.mutex + exception E_Mutex of mcp_mutex exception E_Proofterm of Proofterm.proof exception E_Data of data @@ -62,7 +62,7 @@ exception E_Position of Position.T exception E_ToplevelState of Toplevel.state exception E_Transition of Toplevel.transition exception E_Keywords of Thy_Header.keywords -exception E_Mutex of Mutex.mutex +exception E_Mutex of mcp_mutex exception E_Proofterm of Proofterm.proof exception E_Data of data @@ -75,11 +75,11 @@ val (inSecret, outSecret) = SECRETS (* val outStream = BinIO.openOut outputPipeName *) (* Any sending of data, and any adding of data to the object store must use this mutex *) -val mutex = Mutex.mutex () +val mutex = mcp_mutex () fun withMutex f x = let - val _ = Mutex.lock mutex - val result = f x handle e => (Mutex.unlock mutex; Exn.reraise e) - val _ = Mutex.unlock mutex + val _ = mcp_mutex_lock mutex + val result = f x handle e => (mcp_mutex_unlock mutex; Exn.reraise e) + val _ = mcp_mutex_unlock mutex in result end val objectsMax = Unsynchronized.ref 0 @@ -260,12 +260,12 @@ fun runAsync seq f = (* Context for compiling ML code in. Can be mutated when declaring new ML symbols *) val ml_compilation_context = Unsynchronized.ref (Context.Theory \<^theory>) (* Mutex for updating the context above *) -val ml_compilation_mutex = Mutex.mutex () +val ml_compilation_mutex = mcp_mutex () fun update_ml_compilation_context f = let - val _ = Mutex.lock ml_compilation_mutex + val _ = mcp_mutex_lock ml_compilation_mutex val _ = (ml_compilation_context := f (!ml_compilation_context)) - handle e => (Mutex.unlock ml_compilation_mutex; Exn.reraise e) - val _ = Mutex.unlock ml_compilation_mutex + handle e => (mcp_mutex_unlock ml_compilation_mutex; Exn.reraise e) + val _ = mcp_mutex_unlock ml_compilation_mutex in () end (* Executes ML code in the namespace of context, and updates that namespace (side effect) *) fun executeML_update (ml:string) = let diff --git a/src/main/resources/de/unruh/isabelle/control/control_isabelle_logged.ml b/src/main/resources/de/unruh/isabelle/control/control_isabelle_logged.ml index 588a023..b8c52b8 100644 --- a/src/main/resources/de/unruh/isabelle/control/control_isabelle_logged.ml +++ b/src/main/resources/de/unruh/isabelle/control/control_isabelle_logged.ml @@ -37,7 +37,7 @@ structure Control_Isabelle : sig exception E_ToplevelState of Toplevel.state exception E_Transition of Toplevel.transition exception E_Keywords of Thy_Header.keywords - exception E_Mutex of Mutex.mutex + exception E_Mutex of mcp_mutex exception E_Proofterm of Proofterm.proof exception E_Data of data @@ -74,7 +74,7 @@ exception E_Position of Position.T exception E_ToplevelState of Toplevel.state exception E_Transition of Toplevel.transition exception E_Keywords of Thy_Header.keywords -exception E_Mutex of Mutex.mutex +exception E_Mutex of mcp_mutex exception E_Proofterm of Proofterm.proof exception E_Data of data @@ -174,11 +174,11 @@ fun logSendReplyData seq data = (* val outStream = BinIO.openOut outputPipeName *) (* Any sending of data, and any adding of data to the object store must use this mutex *) -val mutex = Mutex.mutex () +val mutex = mcp_mutex () fun withMutex f x = let - val _ = Mutex.lock mutex - val result = f x handle e => (Mutex.unlock mutex; Exn.reraise e) - val _ = Mutex.unlock mutex + val _ = mcp_mutex_lock mutex + val result = f x handle e => (mcp_mutex_unlock mutex; Exn.reraise e) + val _ = mcp_mutex_unlock mutex in result end val objectsMax = Unsynchronized.ref 0 @@ -373,12 +373,12 @@ fun runAsync seq f = (* Context for compiling ML code in. Can be mutated when declaring new ML symbols *) val ml_compilation_context = Unsynchronized.ref (Context.Theory \<^theory>) (* Mutex for updating the context above *) -val ml_compilation_mutex = Mutex.mutex () +val ml_compilation_mutex = mcp_mutex () fun update_ml_compilation_context f = let - val _ = Mutex.lock ml_compilation_mutex + val _ = mcp_mutex_lock ml_compilation_mutex val _ = (ml_compilation_context := f (!ml_compilation_context)) - handle e => (Mutex.unlock ml_compilation_mutex; Exn.reraise e) - val _ = Mutex.unlock ml_compilation_mutex + handle e => (mcp_mutex_unlock ml_compilation_mutex; Exn.reraise e) + val _ = mcp_mutex_unlock ml_compilation_mutex in () end (* Executes ML code in the namespace of context, and updates that namespace (side effect) *) fun executeML_update (ml:string) = let