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

What will be exported by this? Ie what does generated files contain. All files ever generated by the session?


-------- Original Message --------
Subject: Re: [isabelle] Export files generated by code_export to hard drive
From: Makarius <makarius at>
To: "Max W. Haslbeck" <max.haslbeck at>,isabelle-users at

On 30/04/2019 18:16, Max W. Haslbeck wrote:
>> Am 30.04.2019 um 14:14 schrieb Makarius :
>> 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.
> Thanks for the pointer. For now I use the following Isabelle/ML script:
> export_code binomial in Haskell
> ML ‹
> val gen_files = Generated_Files.get_files (Proof_Context.theory_of @{context})
> val output_dir = Path.explode "~/output_hs/"
> ›
> (*
> (* The next line creates output_dir and writes the files there *)
> ML ‹map (Generated_Files.write_file write_dir) gen_files›
> *)

In some sense this emulates the Isabelle2018 behaviour of export_code.

Just out of curiosity: What happens with the content of the global
~/output_hs directory? Is it just for information, our do other tools
take over the content?


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