Re: [isabelle-dev] HOL build process hangs
On 03/05/18 15:34, Lawrence Paulson wrote: > > ISABELLE_BUILD_OPTIONS="" > > ML_PLATFORM="x86-darwin" > ML_HOME="/Users/lp15/.isabelle/contrib/polyml-5.7.1-5/x86-darwin" > ML_SYSTEM="polyml-5.7.1" > ML_OPTIONS="-H 1000" Lets try with ML_OPTIONS="--minheap 1500" (in $ISABELLE_HOME_USER/etc/settings) and with threads=4 (in the Isabelle/jEdit / Plugins / Plugin Options / Isabelle / General -- near the bottom). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL build process hangs
Larry > On 3 May 2018, at 13:48, Makarius wrote: > > On 03/05/18 14:04, Lawrence Paulson wrote: >>> >>> What is your changeset id? >> >> ~/isabelle/Repos/src/HOL: hg id >> 8dc792d440b9+ tip > > That is after my change 0acf3206a723. Did you see the problem in > 36209dfb981e, too? I have no idea how I could answer this question, as these change numbers appear to be absolutely random. I have recently been pulling changes every morning and I saw similar symptoms yesterday. > What are the build options, e.g. the bottom of the output of "isabelle >>> build -?” ? > > The "isabelle build" tool with argument "-?" emits various settings for > convenience. ISABELLE_BUILD_OPTIONS="" ML_PLATFORM="x86-darwin" ML_HOME="/Users/lp15/.isabelle/contrib/polyml-5.7.1-5/x86-darwin" ML_SYSTEM="polyml-5.7.1" ML_OPTIONS="-H 1000" Larry___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL build process hangs
On 03/05/18 14:04, Lawrence Paulson wrote: >> >> What is your changeset id? > > ~/isabelle/Repos/src/HOL: hg id > 8dc792d440b9+ tip That is after my change 0acf3206a723. Did you see the problem in 36209dfb981e, too? >> What are the build options, e.g. the bottom of the output of "isabelle >> build -?” ? The "isabelle build" tool with argument "-?" emits various settings for convenience. E.g. ISABELLE_BUILD_OPTIONS="threads=6" ML_PLATFORM="x86-linux" ML_HOME="/home/makarius/.isabelle/contrib/polyml-5.7.1-5/x86-linux" ML_SYSTEM="polyml-5.7.1" ML_OPTIONS="-H 1500" Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL build process hangs
> On 3 May 2018, at 12:56, Makarius wrote: > > On 03/05/18 13:18, Lawrence Paulson wrote: >> I'm encountering a strange phenomenon: the HOL build process runs for just >> over two minutes (which is not long enough to complete) and then seems to >> stop running, using 0.1% of the processor. I can repeat it and the same >> thing happens again. Today I was lucky on the third attempt. What could >> cause the build to hang and do nothing? > > What is your changeset id? ~/isabelle/Repos/src/HOL: hg id 8dc792d440b9+ tip > What is the underlying hardware? Mac Pro (2013), 3.5GHz 6-Core Xeon E5 with 16GB > What are the build options, e.g. the bottom of the output of "isabelle > build -?” ? One was “isabelle jedit ” and the other was this: ~/isabelle/Repos/src/HOL: isabelle build -b HOL Building HOL ... ^C^C^C*** Interrupt HOL FAILED Unfinished session(s): HOL 0:08:42 elapsed time, 0:02:13 cpu time, factor 0.25 ^C^C ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL build process hangs
On 03/05/18 13:18, Lawrence Paulson wrote: > I'm encountering a strange phenomenon: the HOL build process runs for just > over two minutes (which is not long enough to complete) and then seems to > stop running, using 0.1% of the processor. I can repeat it and the same thing > happens again. Today I was lucky on the third attempt. What could cause the > build to hang and do nothing? What is your changeset id? What is the underlying hardware? What are the build options, e.g. the bottom of the output of "isabelle build -?" ? Is that really just the HOL image, or HOL-Proofs? For week I have trie to evade a resource problem with HOL-Proofs and threads=2. The latest attempt is 0acf3206a723, but it should not affect the HOL image. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] HOL build process hangs
I'm encountering a strange phenomenon: the HOL build process runs for just over two minutes (which is not long enough to complete) and then seems to stop running, using 0.1% of the processor. I can repeat it and the same thing happens again. Today I was lucky on the third attempt. What could cause the build to hang and do nothing? Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
