On Thu, 8 Nov 2012, Gerwin Klein wrote:
When I was testing, I was running sessions one at a time, not in
parallel, so I wouldn't have seen any issues with too many parallel jobs
or similar.
Does anyone know what the timeout measures? Elapsed real time or time
spent on that session?
The
On Thu, 8 Nov 2012, Lawrence Paulson wrote:
The long-term solution must be to deliver self-contained proof scripts,
but obviously it will be difficult.
Self-contained as a black-box binary should be possible, but then it
becomes difficult to maintain theories: slight changes in the
On Tue, 13 Nov 2012, Lars Noschinski wrote:
Hi,
sometimes, I am encountering some erraneous behaviour of qed when a
structured proof contains some facts for which the final by step failed.
Before the closing block the output buffer reads:
goal:
No subgoals!
But qed then fails with an
Fabian and I found the missing check in Cooper's algorithm
(src/HOL/Tools/Qelim). The fix can be found in the testboard
52e97a5f5e25. If it works I will push it to the Isabelle repository.
- Johannes
Am Samstag, den 01.12.2012, 22:01 +0100 schrieb Florian Haftmann:
In rev. 544764f4324d
Isabelle/2c7479865e07 has now some notes on the Isabelle component
repository at TUM in the file Admin/component_repository/README.
Since I have now managed to install various new components without any
surprises from isatest or mira, I've summarized my state of information
about that affair
Hi all,
I'd like to report two problems with Isabelle (b17b05c8d4a4) -- AFP
(40ecbad14077).
1. In Proof General:
theory Scratch
imports
$MY_AFP_DEVEL_HOME/thys/Jinja/J/TypeSafe
~~/src/HOL/Proofs/Lambda/StrongNorm
begin
nondeterministically gives either
***
Am 03.12.2012 um 22:31 schrieb Jasmin Christian Blanchette:
I'd like to report two problems with Isabelle (b17b05c8d4a4) -- AFP
(40ecbad14077).
1. In Proof General:
theory Scratch
imports
$MY_AFP_DEVEL_HOME/thys/Jinja/J/TypeSafe
~~/src/HOL/Proofs/Lambda/StrongNorm
Am 03.12.2012 14:24, schrieb Johannes Hölzl:
Fabian and I found the missing check in Cooper's algorithm
(src/HOL/Tools/Qelim). The fix can be found in the testboard
52e97a5f5e25. If it works I will push it to the Isabelle repository.
- Johannes
Thnx a lot!
Florian
--
PGP
Am 03.12.2012 um 23:08 schrieb Lawrence Paulson:
Missing components maybe?
I did isabelle components -a earlier today. In fact, the issue is likely to
be related to the big upgrade that resulted from my invocation of this very
command yesterday night.
Jasmin
Did you try starting jEdit with -f to force a fresh build?
Jasmin Blanchette jasmin.blanche...@gmail.com schrieb:
Am 03.12.2012 um 23:08 schrieb Lawrence Paulson:
Missing components maybe?
I did isabelle components -a earlier today. In fact, the issue is likely to
be related to the big
Am 04.12.2012 um 07:51 schrieb Lars Noschinski:
Did you try starting jEdit with -f to force a fresh build?
That did the trick. Thanks!
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
11 matches
Mail list logo