Error Messages

From Isabelle Community Wiki
Jump to navigation Jump to search

Irritating and misleading error messages

This page collects error messages and other gotchas which are not helpful (to a beginner) for locating the error.

also or finally fails with empty result sequence

(or creates a strange result) Noschinl 13:27, 8 October 2010 (UTC)

Both commands try to apply a transitivity rule to the facts calculation and this; the error message indicates that this failed.

The most obvious reason is that there is no transitivity rule declared for your case (such rules can be declared with the "trans" attribute).

But there is also a more subtle reason, which is unfortunately a lot more confusing: For calculational reasoning, Isabelle tries to find rules which "make progress". So if you accidentally proved a <= b and ... <= b, Isabelle rules out the obvious transitivity rule which would yield a <= b. If there is no other applicable rule, this results in the aforementioned error message, otherwise a more complicated rule is applied which results in a strange, unexpected result (which may very well lead to an "empty result sequence" for the next "also".

Note that this filtering also takes place if you explicitly give a set of transitivity rules to also or finally.

exception TYPE raised in a lemma statement

Noschinl 13:27, 8 October 2010 (UTC)

exception TYPE raised (line 360 of "envir.ML"): expand_atom: ill-typed replacement

(line number may vary over version of Isabelle). This error can occur of you bind and use a pattern in a lemma statement, e.g.

lemma assumes "P foo" (is "P ?bar") shows "Q ?bar"

This is due to the fact that parsing and type inference for the whole lemma statement is done at once. Sufficiently verbose type annotations might help.

Illegal variable name: "a :: 'a" at command "definition"

When typing a definition and using the quotes at the wrong position, as in:

definition "a :: 'a" where "a = False"

Isabelle returns

Illegal variable name: "a :: 'a" At command "definition"

To the user, it is totally unclear why "a" is interpreted as a variable.

Quickcheck returns error but no error message

When using Quickcheck before it is set up properly, as in:

theory Scratch
imports Datatype
theorem "False"

there is an error, but no error message. Suggestion: No quickcheck generator is set up. To have a quickcheck generator set up, you should import Main.

Misleading variable naming in list comprehension


[ (a,y) . (a,y) <-  xs, y <- ys]

the two y after the . are distinct ie not shared. For shared variable it should be written as

[ (a,y). (a,y) <- xs, y' <- ys, y = y' ]

Suggestion: Add this information to the list theory.

Misleading variable naming in set comprehension

The expression

 {(v, v). v ∈ {''a'', ''b''}}

is actually interpreted as

 {(va∷'a, v∷char list). v ∈ {''a'', ''b''}}