Re: [isabelle] Isabelle2021-RC3 New failure mode for "try"/sledgehammer



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.









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