[isabelle-dev] NEWS: export_code with formally generated files

[Makarius]

On 30/03/2019 21:16, Makarius wrote:
> On 30/03/2019 20:00, Julian Brunner wrote:
>>
>> At the moment, the executable merely complements a hardcoded automaton
>> and writes it to a file for testing and benchmarking purposes. It will
>> not stay like this. Once a parser for the Hanoi Omega Automata format
>> has been written, this will become a generic command-line
>> complementation tool. I am not sure what sort of test should be run on
>> such a tool as part of the regular AFP build.
> 
> For now it is sufficient to have some sanity check of the existing
> material. I will put it into better shape following the hints below ...

See now Isabelle/a8142ac5e4b6 + AFP/c17c654f6bb6. The MLton test works
and is properly checked for errors.

Isabelle/jEdit provides various possibilities to get to exported
artifacts, even regular hyperlinks on "export_code ... file_prefix" or
various \<^path_binding> antiquotations in the ML setup of
thys/Buchi_Complementation/Complementation_Build.thy

This is how to spill exports into the session source tree (directory
thys/Buchi_Complementation/code):

  isabelle build -e -d '$AFP' Buchi_Complementation


Note that there is a formal condition on ISABELLE_MLTON. We don't have
anything for mlprof: my impression is that this is merely required for
experimentation / development.  The exported mlmon.out hardly contains
any information.


	Makarius