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