[isabelle-dev] Isabelle/jEdit: non-trivial theory merge
Makarius
makarius at sketis.net
Mon Mar 12 17:47:23 CET 2012
On Wed, 7 Mar 2012, Lars Noschinski wrote:
> today (57bf0cecb366) I noticed some strange behaviour in jEdit when
> bootstrapping HOL. I had HOL fully loaded (after working around the usual
> problems with newly defined commands). However, every change which causes
> FunDef.thy to be reprocessed, triggered error in later theories using the
> "fun" or "function" commands:
>
> For example, Divide.thy at line 1194:
>
> function posDivAlg :: "int ⇒ int ⇒ int × int" where
> "posDivAlg a b = (if a < b ∨ b ≤ 0 then (0, a)
> else adjust b (posDivAlg a (2 * b)))"
>
> with
>
> Attempt to perform non-trivial merge of theories:
> {..., Relation, Transitive_Closure, Partial_Function, Wellfounded,
> FunDef:33}
> {..., Equiv_Relations, Int, Nat_Numeral, Nat_Transfer, Divides:408}
>
> When I reload Divide.thy, this problem goes away. Similar problems occur at
> other uses of "function" in later theories.
>
> I recall that I was able to do changes in early HOL without such problems
> with jEdit some months ago.
There is still no proper support for redefining Isar commands in the
running session. So I would say the above is the normal consequence of
redefining 'function' in one theory while another one already reparses an
older version of it. Thus the resulting transaction is from a different
theory (different version with the same name).
Isabelle/8f3bb485f628 tries to make it a bit less erratic: commands are
always parsed dynamically. This means, once the tokenization (span
detection) is done, it should run correctly even with newer command
versions.
It is nonetheless not really right. Strange implicit effects on the
global command table are broken by design (which is from 1998). Mutable
state is the root of all evil ...
Makarius
More information about the isabelle-dev
mailing list