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



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


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.