[isabelle-dev] Isabelle build only works in certain directories

Lawrence Paulson lp15 at cam.ac.uk
Thu Jun 28 16:07:08 CEST 2018

My last email was premature, because the exact same thing happened again: it hung at 2:15 minutes of CPU time. Fortunately I was able to kill it and retry, and thanks to multithreading, you don't have to wait anything like two minutes before reaching the two minute mark.


> On 28 Jun 2018, at 14:58, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> I wonder whether this relates to the problem I have seen from time to time, where the build process "goes to sleep" around two minutes into building HOL. It's reproducible enough that I can feel confident that HOL will build only when the activity monitor shows that the process has consumed at least three minutes of CPU time. But I haven't seen it for a couple of weeks. 
> I am (currently) running macOS High Sierra 10.13.5 but there may have been an OS update during that time. It may be worth updating your system and trying again.
> Larry
>> On 28 Jun 2018, at 12:25, Max Haslbeck <max.haslbeck at gmx.de> wrote:
>> I have the following curious problem: isabelle build only seems to work when I’m in certain directories.
>> Steps to reproduce:
>> 1. Start out with clean mercurial repository of isabelle in '/Users/mhaslbeck/Projects/isabelle'
>> 2. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle components -I'
>> 3. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle components -a'
>> 4. run 'cd /'
>> 5. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle build -v Pure'
>> Output:
>> ```
>> ### Building Isabelle/Scala ...
>> Started at Thu Jun 28 13:03:18 GMT+2 2018 (polyml-5.7.1_x86-darwin on lap44-cl-c703)
>> ML_PLATFORM="x86-darwin"
>> ML_HOME="/Users/mhaslbeck/.isabelle/contrib/polyml-5.7.1-6/x86-darwin"
>> ML_SYSTEM="polyml-5.7.1"
>> ML_OPTIONS="--minheap 500"
>> Session Pure/Pure
>> ```
>> 6. The build process now freezes and doesn’t react to keyboard input, can be killed by 'pkill java'
>> 7. run 'mkdir ~/tmp; cd ~/tmp'
>> 8. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle build -v Pure'
>> freezes with same output as in 5.

More information about the isabelle-dev mailing list