Email Gateway (Aug 22 2022 at 19:30): Email Gateway (Aug 22 2022 at 19:30):From: "Max W. Haslbeck" <max.haslbeck@gmx.de>
Hi,
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.
Gruß
Max
Email Gateway (Aug 22 2022 at 19:31):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 22 2022 at 19:31):From: "Max W. Haslbeck" <max.haslbeck@gmx.de>
Thanks for the pointer. For now I use the following Isabelle/ML script:
====================
theory Scratch
imports Main
begin
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›
*)
end
====================
Email Gateway (Aug 22 2022 at 19:31):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 22 2022 at 19:31):From: "lammich@in.tum.de" <lammich@in.tum.de>
What will be exported by this? Ie what does generated files contain. All files
ever generated by the session?
Peter
Email Gateway (Aug 22 2022 at 19:31):From: Peter Lammich <lammich@in.tum.de>
I have use-cases where other tools, like the MlTon compiler or LLVM,
shall take over. They then compile the generated code together with
some other (non-generated) source file.
And I also need to integrate the Isabelle code generator into a larger
build-process controlled by a Makefile/build-script.
How do I do that sort of stuff with the new code generator?
Is there an Isabelle command line tool to "export" the generated
files from Isabelle to the real file system?
Max solution has a hard-coded target directory. This is highly non-
portable. How to export the files to a directory that is determined by
my build-script/Makefile?
Email Gateway (Aug 22 2022 at 19:46):From: Makarius <makarius@sketis.net>
All files from the current theory, unless you filter more specifically.
Makarius
Email Gateway (Aug 22 2022 at 19:47):From: Makarius <makarius@sketis.net>
On 01/05/2019 00:51, Peter Lammich wrote:
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?I have use-cases where other tools, like the MlTon compiler or LLVM,
shall take over. They then compile the generated code together with
some other (non-generated) source file.
This sounds like an application of the command 'compile_generated_files'
e.g. in Isabelle2019-RC0. You can read about it in NEWS, the isar-ref
manual, or do hypersearch for a few applications in Isabelle + AFP to
get an idea.
And I also need to integrate the Isabelle code generator into a larger
build-process controlled by a Makefile/build-script.
Most of that should no longer be required: you simply do all of the
compilation and assembly inside Isabelle/ML, and only export the final
artifacts.
See also documentation (or examples) on 'export_files' within ROOT
files. This helps to wrap up everything nicely such that only "isabelle
build -e" is required to materialize the final result in the file-system.
- Max solution has a hard-coded target directory. This is highly non-
portable. How to export the files to a directory that is determined by
my build-script/Makefile?
You can choose export names (relative to the theory), and maybe strip
some path components in the 'export_files' specification. There is no
support for general renamings: I have tried to keep things simple.
By default, the build-script/Makefile is a candidate for deletion. The
question should be: What are its remaining uses?
If there are fine points in new generated files / exported files that
still make old Makefiles necessary, we have a short time-window before
the Isabelle2019 release to sort this out.
Makarius
Email Gateway (Aug 22 2022 at 19:52):From: "Max W. Haslbeck" <max.haslbeck@gmx.de>
It’s mainly for information, so that I can setup the corresponding Haskell code correctly. We’re trying to reason about LLVM programs in Isabelle/HOL. Right now im using llvm-hs[1] to generate an AST of LLVM code which I then use with Isabelle’s generated code for small test runs. All of this is in its early stages, so it’s useful to have a way to quickly export the generated code.
Gruß
Max
[1] https://hackage.haskell.org/package/llvm-hs
Last updated: Apr 20 2024 at 08:16 UTC