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



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.