[isabelle-dev] HOL-ODE-Numerics FAILED

2018-05-21 Thread Florian Haftmann 
isabelle: 4acc029f69e9 tip
afp: c0882468fab2 tip

> HOL-ODE-Numerics FAILED
> (see also 
> /home/haftmann/.isabelle/heaps/polyml-5.7.1_x86_64-linux/log/HOL-ODE-Numerics)
>thm ->
>  int ->
>int ->
>  int ->
>int ->
>  (int * int * string) list ->
>string -> Proof.context -> int -> tactic
> val poincare'_bnds_tac = fn:
>thm ->
>  int ->
>int ->
>  int ->
>int ->
>  (int * int * string) list ->
>string -> Proof.context -> int -> tactic
> ### Rule already declared as elimination (elim)
> ### \(?f has_derivative ?f') ?F;
> ###  bounded_linear ?f' \ PROP ?W\
> ### \ PROP ?W
> ### theory "HOL-ODE-Numerics.Example_Utilities"
> ### 52.579s elapsed time, 113.340s cpu time, 12.052s GC time
> Loading theory "HOL-ODE-Numerics.ODE_Numerics"
> ### Introduced fixed type variable(s): 'b in "X__"
> ### theory "HOL-ODE-Numerics.ODE_Numerics"
> ### 0.056s elapsed time, 0.168s cpu time, 0.000s GC time
> *** Failed to apply initial proof method (line 985 of 
> "~/data/tum/afp/master/thys/Ordinary_Differential_Equations/Numerics/Runge_Kutta.thy"):
> *** using this:
> ***   convex (T \ X)
> ***   \x\T \ X.
> ***  ((\(t, x). f t x) has_derivative f' x)
> ***   (at x within T \ X)
> ***   \x\T \ X. onorm (f' x) \ B'
> ***   (t, x) \ T \ X
> ***   (t, y) \ T \ X
> *** goal (1 subgoal):
> ***  1. norm
> ***  ((case (t, x) of (t, x) \ f t x) -
> ***   (case (t, y) of (t, x) \ f t x))
> *** \ B' * norm ((t, x) - (t, y))
> *** At command "by" (line 985 of 
> "~/data/tum/afp/master/thys/Ordinary_Differential_Equations/Numerics/Runge_Kutta.thy")

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Cannot build HOL (again)

2018-05-21 Thread Florian Haftmann 
Do the problems persist if you remove ~/.isabelle e.g. to ~/.isabelle_tmp?

Florian

Am 21.05.2018 um 16:23 schrieb Lawrence Paulson:
> Well, it worked on the third attempt. Same as two weeks ago. My guess is that 
> it pauses to wait for some resource: when it stalls, the process is still 
> visible but only uses 0.1% of the processor.
> 
> Larry
> 
>> On 21 May 2018, at 15:13, Manuel Eberl  wrote:
>>
>> It works fine for me.
>>
>> Did you perhaps switch on ML debugging/exception tracing? HOL becomes
>> virtually impossible to build with that switched on. What is the content
>> of your ".isabelle/etc/preferences”?
> 
> (* generated by Isabelle 25-Apr-2018 17:11:02 +0100 *)
> 
> auto_methods = "true"
> auto_nitpick = "true"
> auto_time_limit = "7.0"
> auto_time_start = ".5"
> auto_try0 = "false"  (* unknown *)
> editor_output_state = "true"
> editor_prune_delay = "60.0"
> editor_skip_proofs = "false"  (* unknown *)
> jedit_macos_application = "true"  (* unknown *)
> jedit_macos_preferences = "false"  (* unknown *)
> jedit_print_mode = "brackets"
> jedit_tooltip_delay = "0.5"
> parallel_proofs_threshold = "100"  (* unknown *)
> sledgehammer_provers = "e spass vampire z3 cvc4 "
> sledgehammer_timeout = "60"
> z3_non_commercial = "yes"  (* unknown *)
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Cannot build HOL (again)

2018-05-21 Thread Lawrence Paulson 
Well, it worked on the third attempt. Same as two weeks ago. My guess is that 
it pauses to wait for some resource: when it stalls, the process is still 
visible but only uses 0.1% of the processor.

Larry

> On 21 May 2018, at 15:13, Manuel Eberl  wrote:
> 
> It works fine for me.
> 
> Did you perhaps switch on ML debugging/exception tracing? HOL becomes
> virtually impossible to build with that switched on. What is the content
> of your ".isabelle/etc/preferences”?

(* generated by Isabelle 25-Apr-2018 17:11:02 +0100 *)

auto_methods = "true"
auto_nitpick = "true"
auto_time_limit = "7.0"
auto_time_start = ".5"
auto_try0 = "false"  (* unknown *)
editor_output_state = "true"
editor_prune_delay = "60.0"
editor_skip_proofs = "false"  (* unknown *)
jedit_macos_application = "true"  (* unknown *)
jedit_macos_preferences = "false"  (* unknown *)
jedit_print_mode = "brackets"
jedit_tooltip_delay = "0.5"
parallel_proofs_threshold = "100"  (* unknown *)
sledgehammer_provers = "e spass vampire z3 cvc4 "
sledgehammer_timeout = "60"
z3_non_commercial = "yes"  (* unknown *)

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Cannot build HOL (again)

2018-05-21 Thread Manuel Eberl 
It works fine for me.

Did you perhaps switch on ML debugging/exception tracing? HOL becomes
virtually impossible to build with that switched on. What is the content
of your ".isabelle/etc/preferences"?

Manuel


On 2018-05-21 15:43, Lawrence Paulson wrote:
> I am continuing to be plagued by HOL failing to build, stalling quite 
> reproducibly after about two minutes of processor time. It's a big obstacle 
> to getting any work done, so tips would be welcome.
> 
> Larry
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Cannot build HOL (again)

2018-05-21 Thread Lawrence Paulson 
I am continuing to be plagued by HOL failing to build, stalling quite 
reproducibly after about two minutes of processor time. It's a big obstacle to 
getting any work done, so tips would be welcome.

Larry

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev