*To*: Mathias Fleury <mathias.fleury12 at gmail.com>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Isabelle2021-RC3 New failure mode for "try"/sledgehammer*From*: "Eugene W. Stark" <isabelle-users at starkeffect.com>*Date*: Sat, 13 Feb 2021 11:20:17 -0500*In-reply-to*: <79efb95e-2011-ccf9-383f-5a8f8babe8ad@starkeffect.com>*References*: <3f3f6473-2300-96ad-e22f-256d9332838a@starkeffect.com> <92db52e4-e774-b651-a94e-824d606dc18b@gmail.com> <d404fbbe-d730-fbea-038a-65212b550c64@starkeffect.com> <79efb95e-2011-ccf9-383f-5a8f8babe8ad@starkeffect.com>*Reply-to*: stark at cs.stonybrook.edu*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.10.0

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. >>>> >>>> >>> >> >> > >

**Follow-Ups**:**Re: [isabelle] Isabelle2021-RC3 New failure mode for "try"/sledgehammer***From:*Mathias Fleury

- Previous by Date: Re: [isabelle] Isabelle2021-RC5: support for Apple Silicon
- Next by Date: Re: [isabelle] Rewrites for a sublocale with UNIV as the carrier set
- Previous by Thread: Re: [isabelle] Some more polishing of the multiset theory
- Next by Thread: Re: [isabelle] Isabelle2021-RC3 New failure mode for "try"/sledgehammer
- Cl-isabelle-users February 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list