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

Makarius makarius at sketis.net
Thu Jun 28 15:53:05 CEST 2018


On 28/06/18 13:25, Max Haslbeck wrote:
> 
> I have the following curious problem: isabelle build only seems to work when I’m in certain directories.
> 4. run 'cd /'
> 5. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle build -v Pure'
>   Output:
> 6. The build process now freezes and doesn’t react to keyboard input, can be killed by 'pkill java'

> OS: macOS High Sierra 10.13.4
> Isabelle rev: f5ca4c2157a5

I have made some experiments with this Isabelle version and macOS
10.13.5, but did not see any such problems.

Maybe there is something odd with the local file-system setup
(encryption, "protections" by Apple etc.). It could be again some fight
of Oracle (Java) vs. Apple.


> Is there any way to get more verbose output from the building process?

Pure is the initial bootstrap: you may get more information if you build
it from a different directory first, and then repeat the experiment with
"isabelle build -b FOL".

An alternative experiment: use "isabelle scala" to build from the
running Isabelle/Scala process:

  import isabelle._

  val options = Options.init()

  Build.build(options, new Console_Progress, sessions = List("Pure"),
verbose = true)



Can you try if some older Isabelle version still works?

You can use "hg up -r Isabelle2017" (or other tags or revs) and then
repeat "isabelle components -a && isabelle jedit -bf" + build invocations.

If you have found a good situation, you can also use hg bisect to narrow
it down:

  hg bisect --reset  #once
  hg up -r f5ca4c2157a5 ; hg bisect --bad

Then "hg bisect --bad" or "hg bisect --good" to record the changing
state of that point in history.


You can also check the particular versions where the underlying JDK
changes: hg grep --all jdk Admin/components/main


	Makarius



More information about the isabelle-dev mailing list