[isabelle-dev] Commands not in scope fail to cause errors
makarius at sketis.net
Fri Apr 17 00:40:11 CEST 2015
On Fri, 10 Apr 2015, Andreas Lochbihler wrote:
> Today, I spent quite a while to figure out why in Isabelle/e936c2828bec
> one of my theories did not process completely in Isabelle/jEdit.
> Starting with a simps_of_case command, the rest of the theory stayed in
> the orange-ish color which indicates that this part had not yet been
> processed. poly kept running with full speed on all cores, but no
> progress was visible - not even one of the purple regions was visible.
That was a bad situation of parsing non-existing commands, leading to
non-termination (no progress of the parser): I have addressed that in
Isabelle/76a8400a58d9. Later, I have made yet another round over the
error handling in Isabelle/35f626b11422. Both changes together should
cover all odd cases described on this thread so far, also by Jasmin and
Conceptually, the situation is as follows:
(1) Theory headers declare command keywords: this is important for
proper division of sources into command spans. Isabelle/jEdit has a
buffer-local syntax (which is also used for highlighting).
(2) Outer_Syntax.command (and derivatives) define command parsers in ML:
this is relevant to provide a semantic transaction to some keyword.
After the change 35f626b11422 above, any missing command parsers should be
reported clearly. Notably also commands before 'theory' and after the
A remaining potential for user confusion is a situation where keyword
declarations are totally missing. In principle, the theory imports need
to be right in order to get access to outer syntax, but there is an
old-style exception to it: the base syntax of the session is the union of
all preloaded theories. In ancient times, we've had the global union of
all keywords from all theories, but this could cause other problems.
This means, with -l HOL-Library the keyword 'simps_of_case' is already a
known keyword, but the command can only be used with the proper import.
With -l HOL it is not a known keyword, unless theory Simps_Case_Conv is
actually imported. This explains the following observation:
> Ultimately, I found out that I had forgot to import the theory
> Simps_Case_Conv which defines the simps_of_case command (my base image
> already contains this theory, so the mark-up in jEdit was as usual and the
> theory goes through with Isabelle2014, as Isabelle2014 did not support local
> command scopes).
The -l HOL-Library case might seem luck, but the theory-local keywords
reform was actually meant to make outer syntax as local as anything else,
i.e. keyword-vs-ident like const-vs-free in the term language. It won't
change for this release, though.
Hopefully the main corner cases are already covered with the above
More information about the isabelle-dev