On 14/03/2021 22:19, Makarius wrote: > > And here is the actual implementation in Isabelle/Scala (using HTTP POST > requests): > > https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/HOL/Tools/ATP/system_on_tptp.scala;e92f2e44e4d8
For completeness, this is the underlying HTTP module in Isabelle/Scala: https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/Pure/General/http.scala;69d449f0ca04 More than 10 years ago, I was promoting the use of perl as "universal system glue". Now we can do it more concisely in Isabelle/Scala, without external dependencies, and with fine points adjusted to Isabelle standards. The above is < 10Kb for client and server, which is used for isabelle.preview in Isabelle/jEdit. It is still too early to ask the canonical question about "any remaining uses of perl": there are still quite a lot in small scripts that are not incorporated in Isabelle/Scala yet, e.g. "isabelle latex". Makarius _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
