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

Lawrence Paulson lp15 at cam.ac.uk
Thu Jun 28 15:58:12 CEST 2018


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)
> ISABELLE_BUILD_OPTIONS=""
> 
> 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