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