Re: [isabelle-dev] AFP: Session AVL-Trees broken
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 timeout in Isabelle build is elapsed time and refers to each session separately. In Isabelle/aaf276a28551 the isatest wrapper script sets a timeout for the regular Isabelle sessions -- they don't have one that is statically wired as in AFP. Also note that the queue manager of isabelle build sorts jobs by the timeout, such that presumably longer ones come first. The afp test assumes it has the machine to itself and runs at 6:28 in the morning. It should be finished after about 3h. The situation is getting better, but is not resolved yet. See the other thread about HOL-Quickcheck_Benchmarks: http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg03443.html Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP: Session AVL-Trees broken
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 specifications might cause big changes in the recovery of proofs. For Z3 in particular, there is also the problem that you have to be a non-commercial user to run it. This is hypothetical at the moment, since there are no commercial Isabelle or AFP maintainers. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit: Inconsistent behaviour with skipped by-proofs
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 error message:
Failed to finish proof:
goal (4 subgoals):
{(x, w), (y, w), (w, x), (w, y)} ⊆ edges sG
1. (x, w) ∈ edges (Abs_graph (insert w (verts G), insert (x, w)
(insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y,
x)}, fst, snd))
2. (y, w) ∈ edges (Abs_graph (insert w (verts G), insert (x, w)
(insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y,
x)}, fst, snd))
3. (w, x) ∈ edges (Abs_graph (insert w (verts G), insert (x, w)
(insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y,
x)}, fst, snd))
4. (w, y) ∈ edges (Abs_graph (insert w (verts G), insert (x, w)
(insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y,
x)}, fst, snd))
The subgoals in this message are the remaining goals of a failed
qed-step earlier in this proof.
This is probably an effect of the implicit propagation of exceptions
between task groups, which is essential in batch mode to get all
exceptions together in the end. Here it gets in the way, because the
hopping of failures from one task to another duplicates them in the
document view.
I need to rethink this (again+).
Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Exception TERM in method arith
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 theory Foo imports Main begin lemma less_dvd_minus: fixes m n :: nat assumes m n shows m dvd n ⟷ m dvd (n - m) using assms apply arith oops Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Notes on the Isabelle component repository at TUM
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 here. If there is anything missing or wrong, just tell me. Information is not getting more accurate by producing diverging clones on some wiki. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Two problems
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
*** Undeclared type constructor: vname (line 12 of
/Users/blanchet/afp/thys/Jinja/Common/Decl.thy)
*** Failed to parse type
*** in type abbreviation fdecl
*** At command type_synonym (line 11 of
/Users/blanchet/afp/thys/Jinja/Common/Decl.thy)
or
*** Inner lexical error at: ⟪i:U⟫ ⊢ t : T ⟹
*** IT u ⟹ e ⊢ u : U ⟹ IT (t[u/i]) (line 91 of
~~/src/HOL/Proofs/Lambda/StrongNorm.thy)
*** Failed to parse proposition
*** At command lemma (line 90 of
~~/src/HOL/Proofs/Lambda/StrongNorm.thy)
but each of them loads fine on its own.
2. I then wanted to try in jEdit but isabelle jedit gives this error:
### Building Isabelle/jEdit ...
src/graphview_dockable.scala:45: error: object graphview is not a member of
package isabelle
new
isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph)) {
^
src/graphview_dockable.scala:45: error: too many arguments for constructor
Object: ()java.lang.Object
new
isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph)) {
^
src/graphview_dockable.scala:53: error: value peer is not a member of
AnyRef{def make_tooltip(parent: javax.swing.JComponent,x: Int,y: Int,body:
isabelle.XML.Body): String}
graphview.add(panel.peer, BorderLayout.CENTER)
^
three errors found
Failed to compile sources
From what I recall, isabelle jedit worked fine on my machine (Mac OS X 10.6)
just one or two weeks ago.
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Two problems
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 begin I investigated some more, and this problem is clearly related to the existence of two theories called Type.thy -- which one gets picked up depends on luck. So I guess that's a known issue. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Exception TERM in method arith
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 available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Two problems
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Two problems
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 upgrade that resulted from my invocation of this very command yesterday night. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Two problems
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 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
