Re: [isabelle] Problem with command-line version



On Thu, 12 Nov 2009, René Thiemann wrote:

  fix a :: int
  have "∃ b. a = a * b ∧ b > 0" by auto
  then obtain b where "a = a * b" and "b > 0" by auto
  hence "∃ c. b = c + (1 :: int) ∧ c ≥ 0" by arith
  hence True by simp

When stepping through the proof interactively, everything works fine. However, when using isabelle-process (Isabelle 2009), I get the following error message for the proof step where arith is applied.

Batch mode is a bit more thorough by default, in particular quick_and_dirty is disabled. Apparently the crash is caused by the full version of the Cooper procedure, not the oracle version.

It seems that Sasche Böhme has already fixed the problem recently: see http://isabelle.in.tum.de/repos/isabelle/raw-rev/40a0760a00ea You can direct paste this text into stdin of "patch -p 1", to modify Isabelle2009 accordingly.

Alternatively you can make yourself an alpha/beta tester of the next release, and use one of the many development snapshots. (We are approaching the next official release already.)


	Makarius


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