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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev