[isabelle-dev] Cannot build HOL (again)

[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 <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 *)
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180521/c85c45fb/attachment.sig>