[isabelle-dev] Isabelle/jEdit: non-trivial theory merge

[Makarius]

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