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