Email Gateway (Aug 22 2022 at 17:02): Email Gateway (Aug 22 2022 at 17:02):From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
Hi all,
as information for further analysis, I can confirm that this issue
also occurs on the recent development version of Isabelle with hg id:
9c31678d2139.
Lukas
Email Gateway (Aug 22 2022 at 17:07):From: Makarius <makarius@sketis.net>
On 06/04/18 10:00, Peter Zeller wrote:
[I hope this is the right place for bug reports -- I did not find any
public issue tracker.]
Yes, definitely.
The isabelle-users mailing list is for all kinds of observations and
discussions of official Isabelle releases. Likewise the isabelle-dev
mailing list is for arbitrary repository snapshots (with indication of
the changeset id) and in particular the administrative process around it.
Thus as a user of official Isabelle2017, anything posted on
isabelle-users is the correct place.
When trying to use the smt method I am getting the error: exception
Option raised (line 82 of "General/basics.ML")Here is a minimized example where this happens:
lemma
assumes "⋀a . ∃!x. f x = [a]"
shows "∃!x. ∃!y. f x = [a] ∧ f y = [b]"
proof -
have ?thesis
using assms by smt (* exception Option raised (line 82 of
"General/basics.ML") *)
show ?thesis
using assms by metis (* works *)
qedI am using Isabelle 2017 on Linux.
Thanks for this clear example. It looks like a problem in the
post-processing of Z3 proofs by the "smt" proof method, but could be
also in Z3 itself. Included is an exception trace of the situation. The
exception is raised here
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/src/HOL/Tools/SMT/z3_proof.ML#l221
val objTs = map (the o Symtab.lookup env) bounds
with the following run-time values:
bounds = ["?1", "?0"]
env = {("?0", "'b")}
The module Z3_Proof is by Sascha Böhme -- I hope he will have an idea
what is wrong.
The error message is not very helpful, since the "the" function is
called in many places. If I want to understand this bug, what would be
the best way to debug it and find the problematic call to "the"?
By default, Poly/ML provides hardly any exception trace information --
for performance reasons. In order to figure out the above, I did the
following:
* Remove the existing HOL heap image (presumably in
$ISABELLE_HOME/heaps) and rebuild it with debugging enabled globally
(this can be slow):
isabelle build -o ML_debugger -b HOL -s
The option -s merely accommodates the typical situation for end-users
that ML heaps are built automatically inside the application directory
$ISABELLE_HOME, not the configuration directory $ISABELLE_HOME_USER.
* Start Isabelle/jEdit with session "HOL" and run the above example in
a context with declare [[ML_exception_debugger]] -- it produces a full
exception trace for all modules that have been compiled with ML_debugger
enabled.
* Optional: restarted Isabelle/jEdit with session "Pure" and
experiment directly with the relevant sources, limiting the debugging
information to the relevant module. I also tried the Isabelle/ML
source-level debugger IDE, but it turned out too awkward at this point.
Ultimately, I merely put in some print statements in the proper place:
see also the include changeset "ch" and Scratch.thy for the record.
Such tinkering with Isabelle/ML sources and the Poly/ML runtime
environment can be quite tedious. The above is merely for information,
for anybody who is interested in that.
When seeing a problem, there is no moral obligation to figure out all
its details. It is sufficient to present a clear example as you have
done above.
Makarius
exception_trace
ch
Scratch.thy
Email Gateway (Aug 22 2022 at 17:10):From: Sascha Böhme <boehmes@in.tum.de>
Hello,
The exception is caused by a problem in the proof trace produced by Z3. I’ve slightly improved the error reporting issued by the smt method. This will be contained in next Isabelle release.
I’m sorry to say that the smt method might fail to prove such goals. Prefer metis for tough problems that involve quantifiers.
Cheers,
Sascha
Von: Makarius
Gesendet: Mittwoch, 25. April 2018 14:36
An: Peter Zeller; cl-isabelle-users@lists.cam.ac.uk
Cc: Sascha Boehme
Betreff: Re: [isabelle] Bug report: Exception Option raised when using smtmethod
On 06/04/18 10:00, Peter Zeller wrote:
[I hope this is the right place for bug reports -- I did not find any
public issue tracker.]
Yes, definitely.
The isabelle-users mailing list is for all kinds of observations and
discussions of official Isabelle releases. Likewise the isabelle-dev
mailing list is for arbitrary repository snapshots (with indication of
the changeset id) and in particular the administrative process around it.
Thus as a user of official Isabelle2017, anything posted on
isabelle-users is the correct place.
When trying to use the smt method I am getting the error: exception
Option raised (line 82 of "General/basics.ML")Here is a minimized example where this happens:
lemma
assumes "⋀a . ∃!x. f x = [a]"
shows "∃!x. ∃!y. f x = [a] ∧ f y = [b]"
proof -
have ?thesis
using assms by smt (* exception Option raised (line 82 of
"General/basics.ML") *)
show ?thesis
using assms by metis (* works *)
qedI am using Isabelle 2017 on Linux.
Thanks for this clear example. It looks like a problem in the
post-processing of Z3 proofs by the "smt" proof method, but could be
also in Z3 itself. Included is an exception trace of the situation. The
exception is raised here
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/src/HOL/Tools/SMT/z3_proof.ML#l221
val objTs = map (the o Symtab.lookup env) bounds
with the following run-time values:
bounds = ["?1", "?0"]
env = {("?0", "'b")}
The module Z3_Proof is by Sascha Böhme -- I hope he will have an idea
what is wrong.
The error message is not very helpful, since the "the" function is
called in many places. If I want to understand this bug, what would be
the best way to debug it and find the problematic call to "the"?
By default, Poly/ML provides hardly any exception trace information --
for performance reasons. In order to figure out the above, I did the
following:
* Remove the existing HOL heap image (presumably in
$ISABELLE_HOME/heaps) and rebuild it with debugging enabled globally
(this can be slow):
isabelle build -o ML_debugger -b HOL -s
The option -s merely accommodates the typical situation for end-users
that ML heaps are built automatically inside the application directory
$ISABELLE_HOME, not the configuration directory $ISABELLE_HOME_USER.
* Start Isabelle/jEdit with session "HOL" and run the above example in
a context with declare [[ML_exception_debugger]] -- it produces a full
exception trace for all modules that have been compiled with ML_debugger
enabled.
* Optional: restarted Isabelle/jEdit with session "Pure" and
experiment directly with the relevant sources, limiting the debugging
information to the relevant module. I also tried the Isabelle/ML
source-level debugger IDE, but it turned out too awkward at this point.
Ultimately, I merely put in some print statements in the proper place:
see also the include changeset "ch" and Scratch.thy for the record.
Such tinkering with Isabelle/ML sources and the Poly/ML runtime
environment can be quite tedious. The above is merely for information,
for anybody who is interested in that.
When seeing a problem, there is no moral obligation to figure out all
its details. It is sufficient to present a clear example as you have
done above.
Makarius
Email Gateway (Aug 22 2022 at 17:11):From: Peter Zeller <p_zeller@cs.uni-kl.de>
Hello,
[I hope this is the right place for bug reports -- I did not find any
public issue tracker.]
When trying to use the smt method I am getting the error: exception
Option raised (line 82 of "General/basics.ML")
Here is a minimized example where this happens:
lemma
assumes "⋀a . ∃!x. f x = [a]"
shows "∃!x. ∃!y. f x = [a] ∧ f y = [b]"
proof -
have ?thesis
using assms by smt (* exception Option raised (line 82 of
"General/basics.ML") *)
show ?thesis
using assms by metis (* works *)
qed
I am using Isabelle 2017 on Linux.
The error message is not very helpful, since the "the" function is
called in many places. If I want to understand this bug, what would be
the best way to debug it and find the problematic call to "the"?
Regards,
Peter
Scratch.thy
Last updated: Apr 25 2024 at 01:08 UTC