[isabelle-dev] Remaining uses of Python?

[Makarius]

As a consequence of discontinuing the painfully slow and fragile SOS/NEOS 
server support in 71cdb885b3bb, there is presently no remaining use of 
Python in Isabelle tools.

Are there potential uses in the future?

Otherwhise I could just remove it from the list of "Dependable system 
tools" in Admin/PLATFORMS, and thus save 30 MB or 1200 files on 
Windows/Cygwin, and any further worries about it on Linux and Mac OS X. 
Python was added to the portfolio in 2009 for the sake of xmlrpc in the 
SOS/NEOS script.


The machine-learning guys have had their own experience with Python in the 
meantime, which converged to the following NEWS entry in Isabelle2014:

* Sledgehammer:
   - MaSh overhaul:
     . New SML-based learning algorithms eliminate the dependency on
       Python and increase performance and reliability.


The question about Admin/PLATFORMS is practically relevant, since we have 
discontinued the old "IKEA with missing parts" approach to system 
integration more than 5 years ago.  This means the implicit dependencies 
are made as well-defined and minimal as feasible, such that everything 
"works out of the box without further ado" (according to an ancient 
Isabelle saying).

Both Isabelle/ML and Isabelle/Scala have become quite able system 
programming languages in recent years, so the need for funny scripting 
languages is more and more diminished.


 	Makarius

----------------------------------------------------------------------------
                               http://stop-ttip.org
----------------------------------------------------------------------------