Re: [isabelle] Different behavior in Jedit and Emacs

I tried it myself as well on the development version (changeset 693d8d7bc3cd - the current tip): It works if you switch on quick_and_dirty, but it fails if you switch it off.

This succeeds:

ML {* quick_and_dirty := true *}
datatype 'a dtype  = constr "'a tree"

But this fails:

ML {* quick_and_dirty := false *}
datatype 'a dtype  = constr "'a tree"

Just a short explanation, why this differs:
In quick-and-dirty mode, we actually skip proofs, which are automatically generated by packages, and just provide the theorems
without proof.
Switching it off, the package will actually perform the proof, but in the case mentioned here, this proof method fails.

It seems that your default settings actually differ on the two interfaces, JEdit and Emacs.

We will have to investigate why the proof method actually breaks down in this case.


On 01/20/2012 04:30 PM, Tobias Nipkow wrote:
Just as another data point: I tried the development version with emacs
and it works.


Am 20/01/2012 16:09, schrieb Björn Bartels:
Hi all,
we just came across  the following problem when using the datatype command. The following datatype definition works when using Jedit but does not work when using Emacs as interface. In the previous distribution the example used to work with Emacs as well.

theory test
imports Main

datatype 'a tree =
            leaf "'a"
          | node "nat \<Rightarrow>  'a tree"

datatype 'a dtype  = constr "'a tree"


When using Emacs, we get the following error message:

*** Proof failed.
*** dtype_size fa (constr tree) = 0
***  1. Suc 0 = 0
*** 1 unsolved goal(s)!
*** The error(s) above occurred for the goal statement:
*** dtype_size fa (constr tree) = 0

Thanks for any suggestions!

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.