*To*: Manuel Eberl <eberlm at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] linarith_split_limit_exceeded (current value is 9)*From*: Peter Lammich <lammich at in.tum.de>*Date*: Fri, 29 May 2020 13:41:51 +0100*In-reply-to*: <17c5b308-018e-3e7b-89f5-115d572eabec@in.tum.de>*References*: <10707178-d824-edcf-3bcd-9c5797c4d72a@in.tum.de> <27d87e06c185187d39c5c4545553298e@cam.ac.uk> <31EC4E5E-CD2D-46AA-B2DF-06C2976F9448@cam.ac.uk> <17c5b308-018e-3e7b-89f5-115d572eabec@in.tum.de>

Hi, I sometimes run into this problem too, and I would wish I could disable the splitter altogether, instead of increasing its limit. Unfortunately, this seems not to be possible (?). -- Peter On Fri, 2020-05-29 at 13:32 +0200, Manuel Eberl wrote: > I just wanted to add that just you see that message doesn't mean this > is > actually the reason why your theorem wasn't proven. In my experience, > increasing that limit when you get that message very rarely leads to > a > successful proof. > > Manuel > > > On 29/05/2020 13:27, Lawrence Paulson wrote: > > Hi Angeliki, you have a number of options for modifying this limit: > > > > At the top level of a theory file: > > > > declare [[linarith_split_limit = 15]] > > > > At the top level of a proof: > > > > note [[linarith_split_limit = 15]] > > > > Before an individual proof step: > > > > using [[linarith_split_limit = 15]] > > > > What I don’t know was how high you can take this limit before > > things fall apart. > > > > Larry > > > > > On 28 May 2020, at 12:15, Dr A. Koutsoukou-Argyraki < > > > ak2110 at cam.ac.uk> wrote: > > > > > > Hello, > > > > > > In my formalisation I'm using various very simple algebraic > > > calculations > > > as I do everything step by step > > > ( adding up factors, expanding/ getting rid of - outside > > > parentheses, showing equality of algebraic expressions etc etc.. > > > )that I > > > would expect would be solved by linarith or simp or auto. > > > > > > Very often, when I call Sledgehammer or try0 I keep getting > > > "Proof found" > > > and then repeatedly the message : > > > " > > > linarith_split_limit_exceeded (current value is 9)" > > > > > > I can see this issue has been discussed before but I'm not sure > > > how I could get rid of this problem. > > > Is there some setting/ macro/plugin I could change perhaps? > > > > > > Many thanks in advance, > > > Angeliki > > > > > > > > >

**References**:**[isabelle] AFP submission outage***From:*Manuel Eberl

**[isabelle] linarith_split_limit_exceeded (current value is 9)***From:*Dr A. Koutsoukou-Argyraki

**Re: [isabelle] linarith_split_limit_exceeded (current value is 9)***From:*Lawrence Paulson

**Re: [isabelle] linarith_split_limit_exceeded (current value is 9)***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Thm.cterm_of does not check sort constraints
- Next by Date: Re: [isabelle] [Coq-Club] In a world of perfect interoperability between proof assistants, what tools would you combine?
- Previous by Thread: Re: [isabelle] linarith_split_limit_exceeded (current value is 9)
- Next by Thread: Re: [isabelle] Visualization of partial orders in Isabelle/HOL; use of external tools in the AFP entries
- Cl-isabelle-users May 2020 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