Re: [isabelle] Export files generated by code_export to hard drive

On 30/04/2019 13:40, Max W. Haslbeck wrote:

> I’m using the development version of Isabelle and I’m doing a lot of code exporting to Haskell these days.
> When using the following code
> -----------------------------------------
> theory Scratch
> imports Main
> begin
> export_code binomial in Haskell
> end
> -----------------------------------------
> Isabelle generates 6 .hs files in the virtual "isabelle-export:" directory. Is there a way to quickly export all of these to a non-virtual folder on my hard drive? 

> Right now I open all of these in Isabelle/jedit and use "Save as" from
the "File" menu. My use case has a number of .hs files which change
frequently, so using "Save as" every time is rather tedious.

No, as far as I understand the IO model of jEdit this is a remaining
inconvenience of the VFS approach. I wonder if jEdit has multi-file or
directory operations somewhere that still need to be (re)discovered.

Since export_code uses Generated_Files internally (apart from Export),
you could experiment with Generated_Files.write_file or better use the
command 'compile_generated_files' to turn the individual sources into
some derived artifact. Thus the shell programming happens in Isabelle/ML.

Side-remark: When you say "hard drive" (or "disk") to mean the
"file-system", it is a verbal violation of OS abstractions that are
common-place since 1980. That is particular odd today, since most
machines don't even have a hard drive anymore, and a solid state "disk"
(SSD) is not a disk either.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.