[isabelle-dev] AFP/HLDE

[Florian Haftmann]

Dear all,

> It seems to deliver an executable tool for later use elsewhere, but the
> implementation is very fragile.
> 
> We could take it as a model to get such a task right.

the situation wrt. generated code is indeed somehow baroque.

I am aware of the following layers / approaches:

a) Plain code generation to the file system (export_code … in … …); the
most basic use case.

b) Integration of code generation with the Isabelle/ML runtime; this
refers to evaluation and computations, and has reached a quite
satisfactory state.

c) Simple ad-hoc compilation checks (export_code … checking …) as
./src/HOL/Codegenerator_Test; this has always been mere device to check
that nothing utterly wrong has happended to the code generator.

d) Evaluation beyond Isabelle/ML (in src/HOL/Library/Code_Test.thy);
some kind of generalization of c).

What we have in $AFP/Diophantine_Eqns_Lin_Hom/Solver_Code.thy is
another, not-yet well integrated issue:

e) Using generated code in bigger integrative processes to derive build
results from it.  Also some kind of generalization of c).

There is indeed need for more »cultivation«, but IMHO we should resist
the temptation to put more and more programming language environment
interfaces into Isabelle: that would lead to mimic their divergent and
sophisticated concepts inside our environment (the reason why c) is
comparably simple to achieve is that out of 4 implemented target
languages Scala and SML are already well-integrated into Isabelle).

What about the other way round, i.e. integrating Isabelle into specific
programming language environments? It could work roughtly as follows:
* Generated code is a resource that can be exported from a session.
* Hence arbitrary programming language environment can use Isabelle to
obtain generated code.
* Its integration and compilation than happens just by existing tools of
that programming language environment, without burdening Isabelle at all.
* We would still need a way to integrate such constructs into our build
and session system, to express such things as »run this session, take
those results, put them into that programm call, expect the following
result and continue with …«; but this can maybe done by having a
construct in ROOT files which does not denote a regular theory session
but a operational logic implemented by a piece of Scala running in a
dedicated environment.

So far a few raw thoughts.

Cheers,
	Florian


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20181006/f98915ed/attachment.sig>