[isabelle-dev] AFP/HLDE

[Lars Hupel]

> 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.

Let's call this facility "build actions" for simplicity.

The current approach of "export_code ... checking" is, in my opinion, a
sweet spot. It can be kept working with modest effort. It doesn't test a
whole lot of things though. Making opam and stack available will help us
in the medium term by abstracting exactly what is needed for raw code
generation away from distributions.

The question about build actions is: do they solve the problem in the
AFP, e.g. with HLDE? Invoking arbitrary build tools (i.e. running
arbitrary code) is a problem for two reasons:

– A consistent environment where everything that's needed for any given
application is very hard to guarantee. The closest technologies we have
for that are currently Nix and Docker. (It's no coincidence that Nix
uses "closure" terminology.)

– What are the maintenance guarantees? If something breaks in the
generated code, violating assumptions from third-party code, who will
fix it?

As a case study, consider the "Iptables_Semantics" entry. It produces
non-trivial amounts of code that is subsequently decorated with
hand-written Haskell code that requires ~5 third-party packages.
Currently, all of this is kept in a separate repository. Assume for a
moment that this were to move into the AFP. Now, also assume evolution
of the Isabelle system (for example, some code printing). Things will
break. Furthermore, without additional efforts, this can't just build on
arbitrary machines (not even Stack fixes that fully).

But it gets worse. Let's consider another case study. Peter's GRAT
checker is currently only available in the IsaFoL repository:
<https://bitbucket.org/isafol/isafol/src/master/GRAT/>. This project
consists of an Isabelle part and a C part. The latter is built with CMake.

Again – hypothetically – assume that Peter submits this to the AFP,
using build actions. He'd write something like:

  export_action tool =
    Isabelle_System.bash("cmake . && make && make install")

This is going to be a nightmare. There's virtually nothing you can
assume about the C/C++ toolchain that's present on any given system. In
Haskell/Scala/OCaml one can at least install packages without root
privileges, but not in C.

Docker could fix that. But then we're back at the ever-looming question
of maintenance.

To summarize: The above is, at best, a weak argument against build
actions in general. But I think it is a strong argument against build
actions in the AFP.