Starting Isabelle session using Isabelle/Scala · General

I have made an Isabelle/Scala project using isabelle scala_project. I am trying to start a session using Isabelle/Scala via Server_commands.Session_start. I tried:

Fabian Huch (Jan 29 2025 at 13:10):

Sorry, but from your writing I don't understand what you want to achieve, how, and what you tried. Have a look at Ch.4 of the system manual and at the implementation of the server management tools.

Milan Tom (Jan 29 2025 at 14:48):

Sorry if I was not clear about what I was intending to achieve. I would like to start an Isabelle session as can be achieved in the command line as shown below:

$ isabelle server -c -n test_server
server "test_server" = 127.0.0.1:45443 (password "0177189b-c423-453d-9cfd-d8cdea828156")
OK {"isabelle_id":"...","isabelle_name":"Isabelle2024"}

$ session_start {"session": "HOL"}
OK {"task":"..."}
...
FINISHED {"session_id":"...","tmp_dir":"/tmp/..."}

I want to start the session directly using Isabelle/Scala commands rather than using the console. Above I have listed the Isabelle/Scala commands I have tried to use to achieve this.

Fabian Huch (Jan 29 2025 at 14:54):

This shouldn't be very difficult (you can look up how the "isabelle server" scala code does it) but I suspect you need to start a Server and call Server_Commands.Session_Start.command with the right arguments, in particular with properly initialized Options (via Options.init()).

Fabian Huch (Jan 29 2025 at 14:55):

Though I don't get what you mean with no services have been instantiated. If you call Server_Commands().entries, you will find the instances

Fabian Huch (Jan 29 2025 at 14:56):

All of this of course assumes a proper Isabelle/Scala context, e.g. by registering your own Isabelle/Scala component or running some code via isabelle scala.

Milan Tom (Jan 31 2025 at 09:31):

Based on the code, I believe the correct function to call is Server_Commands.Session_Start.command_body with a Server.Context object as well. However, although I can start the server correctly, I am unable to construct a Server.Context object as its constructor is private. Calling Server_Commands.Session_Start.command directly raises an Isabelle-specific thread required error (I suspect due to not using context.make_task). Are there any workarounds that I can use?

Stream: General