Re: [isabelle] Approximation tactic for very large numbers



I forgot to attach the error message. Here it is:

Unofficial version of Isabelle/HOL (unidentified repository version)
Run out of store - interrupting threads

Run out of store - interrupting threads

Failed to recover - exiting

FATAL: exception not rethrown

standard_error terminated
standard_output terminated
Cannot read message:
Connection reset
message_output terminated
process terminated
command_input terminated
process_manager terminated
Return code: 134


On 03/03/18 14:25, Manuel Eberl wrote:
> Hallo,
> 
> I noticed that the approximation tactic behaves very poorly when the
> input is very large. For instance, attempting to prove "exp (exp 16000
> :: real) > 0" with it results in the tactic running for about a minute
> or two before. The entire Isabelle system becomes unresponsive and
> eventually stops with one of Isabelle/jEdit's "total existence failure"
> messages.
> 
> Now, obviously, I am not expecting the tactic to be able to prove this –
> it uses software floating-point numbers and the exponents here are
> staggeringly large. However, I am wondering if it is possible to make
> the tactic fail gracefully, or at least not take down the entire system.
> Otherwise it is highly problematic to use this tactic as a solver in the
> background, which I intend to do.
> 
> Manuel
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.