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?

Peter


-------- Original Message --------
Subject: Re: [isabelle] Export files generated by code_export to hard drive
From: Makarius <makarius at sketis.net>
To: "Max W. Haslbeck" <max.haslbeck at gmx.de>,isabelle-users at cl.cam.ac.uk
CC:


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?


Makarius




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