Email Gateway (Feb 13 2021 at 16:20): Email Gateway (Feb 13 2021 at 16:20):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
This has occurred again and I was able to capture the files involved. I am forwarding them to you
in an off-list message. I would note that it is not necessarily repeatable on every try -- I think
it must depend on some cache state or other randomness. However, I hope that if you try it several
times you will be able to repeat what I am seeing (I included a screenshot to show it).
- Gene Stark
Email Gateway (Feb 16 2021 at 07:27):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Eugene,
Thanks for providing the files. In your example the reconstruction with
by (smt (verit) ...) works but take more time than the timeout used by
Sledgehammer.
Sadly, this is an example that I cannot fix. Sledgehammer has some
expectations on Skolemization steps that are not true for the proof
format of veriT, leading to such weird bugs. Many proofs can be fitted
to fit the expectations, but others cannot easily -- and that one cannot.
If this is a big issue for you, the solution is to remove veriT from the
provers used by Sledgehammer.
Sorry for the inconveniance,
Mathias
Email Gateway (Feb 16 2021 at 10:18):From: Makarius <makarius@sketis.net>
Thank you for looking into it: for me the main conclusion is that I
don't have to worry about it for the final Isabelle2021 release (to
appear towards the end of the week).
Makarius
Email Gateway (Feb 16 2021 at 12:19):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Thanks for looking into this. However, I guess I am a little bit confused, as the issue was not that the reconstruction
by verit failed, but rather than an Isar "proof" with no "shows" was suggested. Are these somehow related?
- Gene Stark
Email Gateway (Feb 16 2021 at 13:30):From: Mathias Fleury <mathias.fleury12@gmail.com>
Sorry for the confusing message.
On 16/02/2021 13:19, Eugene W. Stark wrote:
Thanks for looking into this. However, I guess I am a little bit confused, as the issue was not that the reconstruction
by verit failed,
(it times out, but succeeds if you wait a little longer)
but rather than an Isar "proof" with no "shows" was suggested. Are these somehow related?
That is where the Sledgehammer assumption on the proof produced by veriT
quicks in.
Are these somehow related?
No. Both approach use veriT and parsing is shared, but everything else
is different.
Mathias
- Gene Stark
On 2/16/21 2:26 AM, Mathias Fleury wrote:
Hi Eugene,
Thanks for providing the files. In your example the reconstruction with by (smt (verit) ...) works but take more time
than the timeout used by Sledgehammer.Sadly, this is an example that I cannot fix. Sledgehammer has some expectations on Skolemization steps that are not true
for the proof format of veriT, leading to such weird bugs. Many proofs can be fitted to fit the expectations, but others
cannot easily -- and that one cannot.If this is a big issue for you, the solution is to remove veriT from the provers used by Sledgehammer.
Sorry for the inconveniance,
Mathias
On 13/02/2021 17:20, Eugene W. Stark wrote:
This has occurred again and I was able to capture the files involved. I am forwarding them to you
in an off-list message. I would note that it is not necessarily repeatable on every try -- I think
it must depend on some cache state or other randomness. However, I hope that if you try it several
times you will be able to repeat what I am seeing (I included a screenshot to show it).- Gene Stark
On 1/31/21 8:27 AM, Eugene W. Stark wrote:
I apologize. I tried to "git stash" to save what I had done since posting, but Isabelle auto-reloaded
the theory I was working on and nuked the undo history. I am finding it impossible now to work back
to the place where I observed the problem.If it occurs again, I will make a better effort to capture a context for you. Thanks.
On 1/31/21 7:47 AM, Eugene W. Stark wrote:
It is part of a context of something like 3K lines of code. Is that useful to you?
On 1/31/21 7:43 AM, Mathias Fleury wrote:
Hi Eugene,
Can you also provide the lemma?
The conversion from proofs generated by veriT to Isar proofs is very complicated, but I cannot fix it without being
the
context to reproduce it…Thanks,
Mathias
On 31/01/2021 13:31, Eugene W. Stark wrote:
The following has happened to me twice now. I have never seen this type of failure before.
Using "try", I get the following suggestion:Trying "solve_direct", "quickcheck", "try0", "sledgehammer", and "nitpick"...
"verit": Sledgehammer ("verit") found a proof: by (smt (verit) "1" R.coinitial_ide_is_con R.comp_def
R.composite_of_def R.conI R.con_comp R.cong_reflexive R.has_composites' R.join_of_join R.join_of_unique_upto
R.join_src R.null_is_zero(1) R.pre_rts_axioms R.pre_rts_with_joins_axioms R.prfx_implies_con R.resid_reflects_con
R.residuation_axioms R.rts_axioms R.rts_with_composites_axioms R.src_eqI calculation commutative_square_def
comp_null(1) null_char pre_rts.prfx_implies_con pre_rts_with_joins.has_joins residuation.arrI residuation.con_def
residuation.con_iff_arr_resid residuation.con_sym rts.composite_comp(2) rts.extensional rts.resid_comp(1)
rts.resid_comp(2) rts.resid_join(1) rts.resid_join(2) rts.resid_join(3) rts_with_composites.comp_assoc seqI
seq_char)
(> 1.0 s, timed out)Isar proof (4 ms):
proof -
have "h ▹ f ≠ h ▹ null ∨ null ≠ h ▹ null ∨ null ≠ R.null ∨ h ▹ f = R.null"
by auto
qed
The Isar proof is not workable, for obvious reasons.
Last updated: Apr 20 2024 at 04:19 UTC