[isabelle-dev] Orphaned theory src/HOL/Library/Sum_of_Squares_Remote
makarius at sketis.net
Fri Sep 13 23:02:03 CEST 2013
On Fri, 13 Sep 2013, Florian Haftmann wrote:
> This theory brands itself as »Examples with remote CSDP« and contains
> nothing beyond some sos invocations. It should be moved to HOL/ex.
I've made this in c6e679443adc as a reduced version of the examples from
Sum_of_Squares.thy. Files Sum_of_Squares.thy and
Sum_of_Squares_Remote.thy being adjacent in that directory reminds of the
semi-formal connection of the sources.
The remote version has to be a separate theory in order to allow the use
of "condition = ISABELLE_FULL_TEST" in the session ROOT.
This arrangement is semi-finished, e.g. we've recently had instabilities
of the CSDP server access again. (It had also revealed mistakes in the
use of parser combinators in the ML part, but I did not investigate
I don't mind if Sum_of_Squares is further brushed up, but there should be
a particular plan behind it, for example to support CSDP tools routinely
as Isabelle component.
More information about the isabelle-dev