Just for the record, the server was not down. This may have merely been a
timeout problem.
Tobias
On 11/09/2014 14:05, Jasmin Christian Blanchette wrote:
> Hi all,
>
> It appears that the Sum of Squares server is down. This makes the build of
> the "HOL-Library" session diverge, at least on my
Hi Florian,
Am 10.09.2014 um 10:22 schrieb Florian Haftmann
:
> when we started this hook business, the situation was as follows:
>
> a) Hook clients were all for adding type class instances, i.e.
> inherently working a the theory level.
>
> b) Hooks were a bootstrap device, e.g. after a certa
I have installed a copy of the software locally. Would be worth making this a
component?
--lcp
> On 11 Sep 2014, at 13:07, Tobias Nipkow wrote:
>
>
>
>> On 11/09/2014 14:05, Jasmin Christian Blanchette wrote:
>> Hi all,
>>
>> It appears that the Sum of Squares server is down. This makes the
On 11/09/2014 14:05, Jasmin Christian Blanchette wrote:
> Hi all,
>
> It appears that the Sum of Squares server is down. This makes the build of
> the "HOL-Library" session diverge, at least on my machine, when
> "ISABELLE_FULL_TESTS" is enabled. In addition, it appears to be at the source
>
Hi all,
It appears that the Sum of Squares server is down. This makes the build of the
"HOL-Library" session diverge, at least on my machine, when
"ISABELLE_FULL_TESTS" is enabled. In addition, it appears to be at the source
of the Isatest failures on "mac-poly-M4" and "mac-poly-M8". What's the
See now http://isabelle.in.tum.de/reports/Isabelle/rev/7f990b3d5189
which seems to do the job. There a still dark corners wrt. to base sort
inference which maybe one day will lift its ugly head but for the moment
it is OK.
Florian
On 10.09.2014 10:35, Florian Haftmann wrote:
> Hi Clemens
