Stream: General

Topic: Export code from command line


view this post on Zulip 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?

view this post on Zulip Lukas Stevens (Sep 09 2022 at 11:00):

I think you are searching for isabelle export. See Section 2.5 in the system manual.

view this post on Zulip Seung Hoon Park (Sep 09 2022 at 11:17):

Cheers! I was able to generate the file using isabelle export.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 20:16 UTC