Email Gateway (Sep 01 2020 at 15:03): Email Gateway (Sep 01 2020 at 15:03):From: Makarius <makarius@sketis.net>
On 29/05/2020 14:41, Peter Lammich wrote:
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 (?).
[I am clearing out old threads and came across this one.]
The standard way to disable linarith_split is via a declaration
[[linarith_split_limit = 0]] e.g. see
https://isabelle.sketis.net/repos/isabelle/file/Isabelle2020/src/HOL/Hoare_Parallel/Graph.thy#l171
Or do you rather want to avoid the odd tracing message produced by the tool?
It could be easily changed to print no message for limit = 0 (or maybe limit < 0)?
Makarius
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@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
Email Gateway (Sep 01 2020 at 15:35):From: Peter Lammich <lammich@in.tum.de>
On Tue, 2020-09-01 at 17:03 +0200, Makarius wrote:
On 29/05/2020 14:41, Peter Lammich wrote:
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 (?).[I am clearing out old threads and came across this one.]
The standard way to disable linarith_split is via a declaration
[[linarith_split_limit = 0]] e.g. seehttps://isabelle.sketis.net/repos/isabelle/file/Isabelle2020/src/HOL/Hoare_Parallel/Graph.thy#l171
Or do you rather want to avoid the odd tracing message produced by
the tool?
It could be easily changed to print no message for limit = 0 (or
maybe limit < 0)?
Probably both. If I'm exploring a proof, but it takes ages b/c of log
buffer congestion, and then stops to ask me if I want to see the next
10000 messages, I'll never know if my proof would run smoothly and
quickly with a reduced split limit.
What is the purpose of these trace messages anyway? If it's a condition
the user should be warned about, it should be a warning. Otherwise,
tracing should be disabled by default, and there should be a
configuration option to turn it on, similar to [[simp_trace]].
Email Gateway (Sep 01 2020 at 15:46):From: Tobias Nipkow <nipkow@in.tum.de>
The purpose is to notify you that completeness has been lost for a specific
reason. You may be able to regain completeness by increasing
linarith_split_limit. However, I can see that it causes more harm than good and
would not oject if the messages were only printed if linarith_trace is set.
Tobias
smime.p7s
Email Gateway (Sep 01 2020 at 19:31):From: Peter Lammich <lammich@in.tum.de>
On Tue, 2020-09-01 at 17:45 +0200, Tobias Nipkow wrote:
On 01/09/2020 17:34, Peter Lammich wrote:
What is the purpose of these trace messages anyway? If it's a
condition
the user should be warned about, it should be a warning. Otherwise,
tracing should be disabled by default, and there should be a
configuration option to turn it on, similar to [[simp_trace]].The purpose is to notify you that completeness has been lost for a
specific
reason. You may be able to regain completeness by increasing
linarith_split_limit. However, I can see that it causes more harm
than good and
would not oject if the messages were only printed if linarith_trace
is set.
Then why not print a single warning message per top-level method
invocation, instead of hundreds or thousands equal trace messages, that
carry no more information than an unary representation of the number of
bound-excesses.
Last updated: Jul 15 2022 at 23:21 UTC