[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