Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code generation in batch mode?

Email Gateway (Sep 17 2022 at 07:47):

From: Sólrún Einarsdóttir <slrn@chalmers.se>
Hi,

I'm doing an experiment that involves loading some theories from the AFP in batch mode.

I run into problems when the theory files contain calls to export_code, generating error messages like this one:

*** exception Protocol_Message
*** [("function", "invoke_scala"), ("name", "make_directory"), ("id", "4")] raised (line 124 of "General/output.ML")
*** At command "export_code" (line 508 of "$AFP/Separation_Logic_Imperative_HOL/Examples/Union_Find.thy")

Is there a flag I could use to work around this, by for example turning off code generation or ignoring calls to export_code?

Or is there a way of getting code generation to work in batch mode?

Thanks!

Sólrún Einarsdóttir

Email Gateway (Sep 17 2022 at 09:43):

From: Makarius <makarius@sketis.net>
On 15/09/2022 16:34, Sólrún Einarsdóttir wrote:

I'm doing an experiment that involves loading some theories from the AFP in
batch mode.

What exactly do you mean by "batch mode"?

There are two ways to process Isabelle theories:

(1) Interactively with the full PIDE protocol.

(2) In batch mode via the build tool, which also includes a minimal PIDE
protocol.

You can also do (1) under program control, as demonstrated by the "isabelle
dump" tool.

I run into problems when the theory files contain calls to export_code,
generating error messages like this one:

*** exception Protocol_Message
***   [("function", "invoke_scala"), ("name", "make_directory"), ("id", "4")]
raised (line 124 of "General/output.ML")
*** At command "export_code" (line 508 of
"$AFP/Separation_Logic_Imperative_HOL/Examples/Union_Find.thy")

This looks like you are working with "isabelle process" or "isabelle console".
Both are for experimentation in restricted situation, and not a proper run of
Isabelle.

Makarius

Last updated: Jan 04 2025 at 20:18 UTC