Re: [isabelle-dev] AFP: Session AVL-Trees broken

2012-12-03 Thread Makarius
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

Re: [isabelle-dev] AFP: Session AVL-Trees broken

2012-12-03 Thread Makarius
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

Re: [isabelle-dev] jEdit: Inconsistent behaviour with skipped by-proofs

2012-12-03 Thread Makarius
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

Re: [isabelle-dev] Exception TERM in method arith

2012-12-03 Thread 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 Am Samstag, den 01.12.2012, 22:01 +0100 schrieb Florian Haftmann: In rev. 544764f4324d

[isabelle-dev] Notes on the Isabelle component repository at TUM

2012-12-03 Thread Makarius
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

[isabelle-dev] Two problems

2012-12-03 Thread Jasmin Christian Blanchette
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 ***

Re: [isabelle-dev] Two problems

2012-12-03 Thread Jasmin Christian Blanchette
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

Re: [isabelle-dev] Exception TERM in method arith

2012-12-03 Thread Florian Haftmann
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

Re: [isabelle-dev] Two problems

2012-12-03 Thread Jasmin Blanchette
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

Re: [isabelle-dev] Two problems

2012-12-03 Thread Lars Noschinski
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

Re: [isabelle-dev] Two problems

2012-12-03 Thread Jasmin Blanchette
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