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

2018-07-02 Thread Max Haslbeck
So I did some further digging with good ol println in Scala :)

When I’m in one of the "wrong" directories the build process spend most of its 
time in the function Mercurial.check_files [1]. The problem seems to be that 
the paths in hg.known_files() are relative to the current working directory. So 
"hg.root + Path.explode(name)" returns an incorrect path. The filtering of 
files in the next lines then doesn’t work and it reruns check() for every file.

The build process works in the directory "~/tmp/tmp" because the paths in 
hg.known_files() start with "../../" and by luck "hg.root + Path.explode(name)" 
returns a correct path.

The version of my mercurial installation is 4.6.1.

[1] 
<https://isabelle.in.tum.de/repos/isabelle/file/1b9462304e1d/src/Pure/General/mercurial.scala#l156
 
<https://isabelle.in.tum.de/repos/isabelle/file/1b9462304e1d/src/Pure/General/mercurial.scala#l156>>

Gruß
Max 



> Am 28.06.2018 um 15:53 schrieb Makarius :
> 
> 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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


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

2018-06-28 Thread Max Haslbeck
Hi,

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.
9. run 'mkdir ~/tmp/tmp; cd ~/tmp/tmp'
10. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle build -v Pure'
  build process finishes successfully

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

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

Gruß
Max
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev