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