Seung Hoon Park (Sep 09 2022 at 10:57): Seung Hoon Park (Sep 09 2022 at 10:57):Hi,
I was wondering if there was a way to generate code produced by export_code by invoking a command line option.
For example, if I have a theory file of the following:
theory Scratch
imports Main
begin
export_code concat in OCaml file_prefix foo
end
I would like to be able to run something like isabelle ... Scratch.thy that generates the file foo.ocaml afterwards. Is there a way to achieve this?
Lukas Stevens (Sep 09 2022 at 11:00):I think you are searching for isabelle export. See Section 2.5 in the system manual.
Seung Hoon Park (Sep 09 2022 at 11:17):Cheers! I was able to generate the file using isabelle export.
Alex Weisberger (Sep 12 2022 at 01:14):How did you invoke isabelle export? I've been trying all kinds of invocations, and can't get it to work.
Alex Weisberger (Sep 12 2022 at 01:32):I was able to get it to work with:
isabelle export -x "*:**" -d . tapl
where tapl is a session that i'm working on
Seung Hoon Park (Sep 13 2022 at 08:27):Apologies for the late response. Yes, that's also how I invoked isabelle export. Perhaps I should have added how I achieved it when I wrote it was working.
Last updated: Dec 21 2024 at 12:33 UTC