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

On 30/04/2019 18:16, Max W. Haslbeck wrote:
>> Am 30.04.2019 um 14:14 schrieb Makarius <makarius at>:
>> 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.