Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] code_reflect and logical file system confusion

view this post on Zulip Email Gateway (Feb 10 2022 at 16:08):

From: Peter Lammich <lammich@in.tum.de>
How do I access the files generated by code_reflect, and import them
into the system runtime?

I tried

code_reflect XXX ... file_prefix foo

this logs a nice clickable link in jedit, that directs to some

isabelle-export:Draft.mythyname/code/foo

I can view that in jedit, OK. But when doing

ML_file "isabelle-export:Draft.mythyname/code/foo"

I just get:

Illegal character ":" in path element "isabelle-export:Draft.mythyname"
The error(s) above occurred in "isabelle-
export:Draft.mythyname/code/foo"

Thanks in advance for any help.
Peter

ps: the core issue that I'm trying to solve is to debug the exported
code. CTRL-Click on a reflected ML function leads to an empty jedit
buffer, so I thought iot might work if the code is in a file.

pps: the code generator tutorial is outdated: in section 8.1 it
mentions a file argument (which does not exist), and the example only
shows a file_prefix argument. Also it promises the purpose of separate
compilation is "This merely generates the referenced code to the given
file which can be
included into the system runtime later on" but lacks any documentation
or pointer to how this can be done.

view this post on Zulip Email Gateway (Feb 12 2022 at 06:57):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,

How do I access the files generated by code_reflect, and import them
into the system runtime?

there is
https://isabelle.in.tum.de/repos/isabelle/file/tip/Admin/lib/Tools/regenerate_cooper
which demonstrates
the canonical and AFAIK only example. Luckily enough most applications
of code_reflect do not need that indirection.

pps: the code generator tutorial is outdated: in section 8.1 it
mentions a file argument (which does not exist), and the example only
shows a file_prefix argument. Also it promises the purpose of separate
compilation is "This merely generates the referenced code to the given
file which can be
included into the system runtime later on" but lacks any documentation
or pointer to how this can be done.

Thanks for the hint, I streamlined this in
https://isabelle.in.tum.de/repos/isabelle/rev/78c2a92a8be4

Cheers,
Florian
OpenPGP_signature

Last updated: Jan 04 2025 at 20:18 UTC