[isabelle-dev] Notes on Isabelle/Scala systems programming

Makarius makarius at sketis.net
Tue Apr 29 18:51:45 CEST 2014


As everybody knows, Isabelle/Scala is the standard language for systems 
programming in Isabelle.

Their might be deep reflexes for "scripting" in perl, python, ruby etc. 
but the real gems are elsewhere.  It is an interesting experience to 
do that properly in Scala.

I've just done again to update all Isabelle + AFP ROOT files, using 
standard Isabelle functions that are already there, but also adding a few 
more bits like Isabelle_System.hg for Mercurial command line tools.

http://isabelle.in.tum.de/repos/isabelle/raw-file/23883e1879c5/src/Pure/Tools/check_source.scala 
may serve as an arbitrary example (which is only vaguely related).  It is 
not necessary to include Isabelle/Scala tools into the Pure.jar like that: 
the isabelle_scala_script wrapper allows to invoke indepdendent tools on 
the spot.  It is documented in the "system" manual.


 	Makarius


More information about the isabelle-dev mailing list