[isabelle-dev] AFP/HLDE

[Makarius]

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