[isabelle-dev] HOL-ODE-Numerics FAILED
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)
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)
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)
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)
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
