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



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





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