[isabelle-dev] Cannot build HOL (again)

[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 <eberlm at in.tum.de> 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 *)