[isabelle-dev] AFP/HLDE

[Makarius]

On 08/10/18 15:58, Lars Hupel wrote:
>> 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.

I've called it export_action, because it happens outside the regular
build, based on static data in the session database.

Another application of it (with different user interface) would be
document preparation: the session exports .tex files the database, some
export action produces .pdf files with pdflatex later on.


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

The current problem are files written in odd places as a side-effect of
the session build.

There is already the possibility to invoke strange things via
Isabelle_System.bash inside Isabelle/ML.


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

We need to be indeed vary of not having the evil C/C++ tool chain come
back on us. We actually do have such tendencies right now, with the
cakeml setup and also opam (it uses "make" internally).


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

I don't mind if it is possible to eliminate AFP/HLDE (theory
Diophantine_Eqns_Lin_Hom.Solver_Code) outright, and just refrain from
doing such things in AFP.

There is already "isabelle export" to export plain data, without running
anything. But then I foresee funny Makefiles showing up in AFP based on
"isabelle build" and "isabelle export" plus a shell action to run other
tools on the result.


	Makarius