Re: [isabelle-dev] Cannot build HOL (again)
> Unknown JAVA_HOME -- Java unavailable After removing .isabelle, you'll have to do the usual incantation to retrieve the components: ./bin/isabelle components -I ./bin/isabelle components -a ___ 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)
Then I get Unknown JAVA_HOME -- Java unavailable Larry > On 21 May 2018, at 18:17, Florian Haftmann > wrote: > > Do the problems persist if you remove ~/.isabelle e.g. to ~/.isabelle_tmp? ___ 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
