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 <ebe...@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 *) _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
