On 06/10/18 13:22, Florian Haftmann wrote: > > a) Plain code generation to the file system (export_code … in … …); the > most basic use case.
Could we have an alternative to the file/directory interface for formal exports just now? The main operation is Export.export with a structured name (separated by slashes) and arbitrary content (bytes). This replaces Isabelle_System.mkdirs / File.write operations. The exported results could be accessed later by other tools outside the session context. > 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). The abstract application I see here is: use Isabelle to produce some executable in Haskell (or OCaml, or Scala, or SML). Thus it is related to other open questions about setting up a well-defined project build environment for these languages. Scala and SML are already somehow special to Isabelle, so it is mainly about Haskell and OCaml. After looking around very briefly, I would continue with the hypothesis that Haskell "stack" and OCaml "opam" could do this for use: provide one and only one well-defined version, independently of the underlying OS distribution. (But having "stack" and "opam" around would still allow users to do other things with them, like playing around with many different versions and packages.) > 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. I think we need a well-balanced construction that addresses our typical requirements, without imposing 16 tons weight on the platform without a real purpose (that would happen by default without looking very carefully). Presently, I am thinking in terms of Isabelle tools like "haskell_setup" and "ocaml_setup", with "stack" and "opam" at the bottom. These would provide ISABELLE_HASKELL and ISABELLE_OCAML settings. For the ROOT entry there is already 'export_files' in Isabelle2018. This could be augmented by something like: export_action NAME = SCALA with a snippet of Scala source that is a function from the resulting session build to unit. It could invoke build tools for Haskell, Ocaml, Scala, SML, even LaTeX in Isabelle/Scala. That would be clearly outside of the session context of the Isabelle/ML process: no funny shell scripts in ML, no odd files written to the source file-system (nor ISABELLE_TMP, nor ISABELLE_HOME_USER). Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev