Something exceptional has happened: isatest finished successfully, without
any problems of the various (old) testing machines.
See also http://isabelle.in.tum.de/devel
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
On Mon, 13 Jul 2015, Makarius wrote:
Hopefully we can not return to isatest runs that work routinely. But we
also need to revisit the actual problem eventually.
This should read as Hopefully we can *now* return ...
Makarius
___
On Fri, 26 Jun 2015, Makarius wrote:
On Fri, 26 Jun 2015, Larry Paulson wrote:
HOL-Proofs, etc., have been failing for several days now. Last time I
checked, it was simply a timeout. Presumably some change to rewriting is
to blame. It may be similar to the AFP failure that I fixed
On Fri, 26 Jun 2015, Makarius wrote:
On Fri, 26 Jun 2015, Larry Paulson wrote:
HOL-Proofs, etc., have been failing for several days now. Last time I
checked, it was simply a timeout. Presumably some change to rewriting is
to blame. It may be similar to the AFP failure that I fixed
On Fri, 26 Jun 2015, Larry Paulson wrote:
HOL-Proofs, etc., have been failing for several days now. Last time I
checked, it was simply a timeout. Presumably some change to rewriting is
to blame. It may be similar to the AFP failure that I fixed yesterday.
Is anyone familiar with this entry?
Oops, I didn't expect my name to appear here ;-)
The changeset 894d6d863823 was a reaction to Andreas Lochbihler's report
[1]. With turned off proofs the effect was a good one.
What is special about Pure.conjunction w.r.t. proof reconstruction? Is
it something in Goal.conjunction_tac? Would
On Sat, 27 Jun 2015, Dmitriy Traytel wrote:
Oops, I didn't expect my name to appear here ;-)
The changeset 894d6d863823 was a reaction to Andreas Lochbihler's report [1].
With turned off proofs the effect was a good one.
What is special about Pure.conjunction w.r.t. proof reconstruction? Is
On Sat, 15 Oct 2011, Gerwin Klein wrote:
This may be similar to the recent AFP failure:
/mnt/home/isatest/isadist/Isabelle_15-Oct-2011/lib/scripts/run-polyml: line 77: 13186
Aborted $POLY -q $ML_OPTIONS
HOL-MicroJava FAILED
(see also
On Sat, 15 Oct 2011, Makarius wrote:
So for the moment the main obstable for switching at64-poly to 5.4.1 is
the lack of an installation in /home/polyml which I will produce soon.
See now Isabelle/22ff7e226946.
Makarius
___
isabelle-dev
On 16/10/2011, at 2:02 AM, Makarius wrote:
On Sat, 15 Oct 2011, Makarius wrote:
So for the moment the main obstable for switching at64-poly to 5.4.1 is the
lack of an installation in /home/polyml which I will produce soon.
See now Isabelle/22ff7e226946.
Thanks.
I'd have been happy to
10 matches
Mail list logo
