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

[Makarius]

On 28/06/18 16:07, Lawrence Paulson wrote:
> 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  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 guess that it is related to the HOL-Proofs multithreading problems,
we've seen in the past few months (especially on threads=2).

I will try to take a deeper look at it again, in the coming weeks before
the Isabelle2018 release.

At the bottom of it, there might be some delicate point in Poly/ML, but
it could be also just in the Isabelle/ML Concurrent modules.


Makarius

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

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

[Makarius]

On 02/07/18 15:20, Max W. Haslbeck wrote:
> Another option would be to set the HGPLAIN environment variable.
> 
> 
>> Am 02.07.2018 um 15:12 schrieb Max W. Haslbeck > >:
>>
>> I found the culprit.
>>
>> In my ~/.hgrc I activated the option:
>> [ui]
>> ...
>> tweakdefaults = True 

I did not know of HGPLAIN yet, and have added it here:

changeset:   68566:38c8b44b40b9
user:wenzelm
date:Mon Jul 02 16:26:58 2018 +0200
files:   src/Pure/General/mercurial.scala
description:
more robust: avoid dire effect of ui.tweakoptions on hg.known_files;

(I now see that I've got the log message slightly wrong.)


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

Re: [isabelle-dev] Isabelle build timing on high-end hardware

[Makarius]

On 02/07/18 15:53, Lawrence Paulson wrote:
> These speedups are certainly very impressive! I have wondered what sort of 
> factor could be achieved with enough cores, but was never persistent enough 
> in trying to borrow hardware from people who had it.

I was myself wondering about more cores: this is the best I have
recently seen, but cores alone don't crunch it.

Performance is ultimately a combination of many things: many cores, few
NUMA nodes, fast SSD, fast memory. (That hardware has 4x 16 2Rx8
PC4-2666V RAM.)


It also needs better scheduling on the Isabelle side: for this it always
helps if people buy test hardware and grant access to me :-)


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

Re: [isabelle-dev] Isabelle build timing on high-end hardware

[Lawrence Paulson]

These speedups are certainly very impressive! I have wondered what sort of 
factor could be achieved with enough cores, but was never persistent enough in 
trying to borrow hardware from people who had it.

Larry

> On 2 Jul 2018, at 14:21, Makarius  wrote:
> 
> Just for the fun of it, here are some timings on truly high-end
> hardware: some colleagues have upgraded recently and granted me access
> to make some tests.
> 
> The results may help others in their hardware decisions.
> 
> Here is an Executive Summary:
> 
>  * Intel Xeon performs better than AMD
>  * fewer NUMA nodes are better
>  * SSD file-systems help to save and load heap images fast
> 
> 
> Here are some details:
> 
> 2 * Intel(R) Xeon(R) Gold 6148 CPU @ 2.40GHz;
> 2 NUMA nodes: distance factor 2.1 for memory access;
> each CPU with 20 cores and hyper-threading: total of 80 hardware threads
> 
> 256 GB SSD
> 
> Ubuntu Linux 16.04
> 
> 
> Isabelle/eb53f944c8cd + AFP/f7e9efc65d82
> ISABELLE_BUILD_OPTIONS="threads=6"
> 
> 
> * 64bit: ML_OPTIONS="--minheap 3g --maxheap 30g"
> 
> Finished HOL (0:02:21 elapsed time, 0:07:13 cpu time, factor 3.07)
> 
> isabelle build -j10 -a -N -f
> 0:13:37 elapsed time, 5:12:16 cpu time, factor 22.91
> 0:18:02 elapsed time, 5:57:58 cpu time, factor 19.85
> 
> isabelle build -j10 -a -N -f -x HOL-Proofs
> 0:15:24 elapsed time, 5:11:24 cpu time, factor 20.20
> 0:14:12 elapsed time, 4:45:27 cpu time, factor 20.10
> 
> isabelle build -j10 -g main -N -f
> 0:07:56 elapsed time, 0:43:58 cpu time, factor 5.53
> 0:08:07 elapsed time, 0:44:33 cpu time, factor 5.48
> 
> 
> * 32bit: ML_OPTIONS="--minheap 1500"
> 
> Finished HOL (0:02:10 elapsed time, 0:06:42 cpu time, factor 3.10)
> 
> isabelle build -j10 -a -N -f
> 0:11:13 elapsed time, 3:24:13 cpu time, factor 18.20
> 0:12:05 elapsed time, 4:07:12 cpu time, factor 20.45
> 
> isabelle build -j10 -a -N -f -x HOL-Proofs
> 0:09:13 elapsed time, 3:37:16 cpu time, factor 23.55
> 0:09:02 elapsed time, 3:27:56 cpu time, factor 22.99
> 
> isabelle build -j10 -g main -N -f
> 0:07:02 elapsed time, 0:39:45 cpu time, factor 5.64
> 0:07:02 elapsed time, 0:39:28 cpu time, factor 5.61
> 
> 
> isabelle build -j4 -o threads=10 -g main -N -f
> 0:06:17 elapsed time, 0:46:10 cpu time, factor 7.34
> 0:05:58 elapsed time, 0:45:26 cpu time, factor 7.60
> 
> isabelle build -j6 -o threads=8 -g main -N -f
> 0:06:40 elapsed time, 0:43:18 cpu time, factor 6.49
> 
> 
> When trying out changes of Pure or HOL, I usually test "-g main" first:
> it consists of HOL, HOL-Algebra, HOL-Analysis,
> HOL-Computational_Algebra, HOL-Library, HOL-Number_Theory,
> HOL-Probability, HOL-SPARK, HOL-Word, HOLCF. Afterwards there is a high
> chance that all of Isabelle works.
> 
> The numbers above are really good for that: 6min and 12min respectively.
> These are "quasi-interactive" builds as they should be today.
> 
> 
>   Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[isabelle-dev] Isabelle build timing on high-end hardware

[Makarius]

Just for the fun of it, here are some timings on truly high-end
hardware: some colleagues have upgraded recently and granted me access
to make some tests.

The results may help others in their hardware decisions.

Here is an Executive Summary:

  * Intel Xeon performs better than AMD
  * fewer NUMA nodes are better
  * SSD file-systems help to save and load heap images fast


Here are some details:

2 * Intel(R) Xeon(R) Gold 6148 CPU @ 2.40GHz;
2 NUMA nodes: distance factor 2.1 for memory access;
each CPU with 20 cores and hyper-threading: total of 80 hardware threads

256 GB SSD

Ubuntu Linux 16.04


Isabelle/eb53f944c8cd + AFP/f7e9efc65d82
ISABELLE_BUILD_OPTIONS="threads=6"


* 64bit: ML_OPTIONS="--minheap 3g --maxheap 30g"

Finished HOL (0:02:21 elapsed time, 0:07:13 cpu time, factor 3.07)

isabelle build -j10 -a -N -f
0:13:37 elapsed time, 5:12:16 cpu time, factor 22.91
0:18:02 elapsed time, 5:57:58 cpu time, factor 19.85

isabelle build -j10 -a -N -f -x HOL-Proofs
0:15:24 elapsed time, 5:11:24 cpu time, factor 20.20
0:14:12 elapsed time, 4:45:27 cpu time, factor 20.10

isabelle build -j10 -g main -N -f
0:07:56 elapsed time, 0:43:58 cpu time, factor 5.53
0:08:07 elapsed time, 0:44:33 cpu time, factor 5.48


* 32bit: ML_OPTIONS="--minheap 1500"

Finished HOL (0:02:10 elapsed time, 0:06:42 cpu time, factor 3.10)

isabelle build -j10 -a -N -f
0:11:13 elapsed time, 3:24:13 cpu time, factor 18.20
0:12:05 elapsed time, 4:07:12 cpu time, factor 20.45

isabelle build -j10 -a -N -f -x HOL-Proofs
0:09:13 elapsed time, 3:37:16 cpu time, factor 23.55
0:09:02 elapsed time, 3:27:56 cpu time, factor 22.99

isabelle build -j10 -g main -N -f
0:07:02 elapsed time, 0:39:45 cpu time, factor 5.64
0:07:02 elapsed time, 0:39:28 cpu time, factor 5.61


isabelle build -j4 -o threads=10 -g main -N -f
0:06:17 elapsed time, 0:46:10 cpu time, factor 7.34
0:05:58 elapsed time, 0:45:26 cpu time, factor 7.60

isabelle build -j6 -o threads=8 -g main -N -f
0:06:40 elapsed time, 0:43:18 cpu time, factor 6.49


When trying out changes of Pure or HOL, I usually test "-g main" first:
it consists of HOL, HOL-Algebra, HOL-Analysis,
HOL-Computational_Algebra, HOL-Library, HOL-Number_Theory,
HOL-Probability, HOL-SPARK, HOL-Word, HOLCF. Afterwards there is a high
chance that all of Isabelle works.

The numbers above are really good for that: 6min and 12min respectively.
These are "quasi-interactive" builds as they should be today.


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

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

[Max W. Haslbeck]

Another option would be to set the HGPLAIN environment variable.
>

> Am 02.07.2018 um 15:12 schrieb Max W. Haslbeck :
> 
> I found the culprit.
> 
> In my ~/.hgrc I activated the option:
> [ui]
> ...
> tweakdefaults = True 
> 
> "tweakdefaults" changes the behaviour of mercurial to output paths relative 
> to the current working directory instead of printing paths relative to the 
> repository root [1].
> 
> I can get the same behaviour in both cases if I pass the --cwd option to 
> mercurial.
> <"${HG:-hg}" --config defaults.status\= --repository 
> /Users/mhaslbeck/Projects/isabelle --cwd /Users/mhaslbeck/Projects/isabelle 
> --noninteractive status --modified --added --clean --no-status>
> 
> [1]  > (at the end of the answer)
> 
> 
>> Am 02.07.2018 um 14:50 schrieb Makarius > >:
>> 
>> On 02/07/18 12:59, Max Haslbeck wrote:
>>> 
>>> 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]
>>> >>  
>>> >
>> 
>> Thanks for going to the bottom of it. Mercurial.known_files is merely a
>> command-line invocation as follows:
>> 
>> "${HG:-hg}" --config defaults.status\= --repository
>> /home/makarius/isabelle/repos --noninteractive status --modified --added
>> --clean --no-status
>> 
>> 
>> I did not see the reported problem: the file names are always relative
>> to the repository root, independently of the current working directory.
>> I have tried it Mercurial 4.6.1 on macOS 10.13.5, and Mercurial 3.7.3 on
>> Ubuntu 16.04.
>> 
>> So there must be something else in your setup. If we can figure this out
>> within the coming days or weeks, I can still do something about it for
>> the Isabelle2018 release.
>> 
>> 
>>  Makarius
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

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

[Max W. Haslbeck]

I found the culprit.

In my ~/.hgrc I activated the option:
[ui]
...
tweakdefaults = True 

"tweakdefaults" changes the behaviour of mercurial to output paths relative to 
the current working directory instead of printing paths relative to the 
repository root [1].

I can get the same behaviour in both cases if I pass the --cwd option to 
mercurial.
<"${HG:-hg}" --config defaults.status\= --repository 
/Users/mhaslbeck/Projects/isabelle --cwd /Users/mhaslbeck/Projects/isabelle 
--noninteractive status --modified --added --clean --no-status>

[1] > (at the end of the answer)


> Am 02.07.2018 um 14:50 schrieb Makarius :
> 
> On 02/07/18 12:59, Max Haslbeck wrote:
>> 
>> 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]
>> 
> 
> Thanks for going to the bottom of it. Mercurial.known_files is merely a
> command-line invocation as follows:
> 
> "${HG:-hg}" --config defaults.status\= --repository
> /home/makarius/isabelle/repos --noninteractive status --modified --added
> --clean --no-status
> 
> 
> I did not see the reported problem: the file names are always relative
> to the repository root, independently of the current working directory.
> I have tried it Mercurial 4.6.1 on macOS 10.13.5, and Mercurial 3.7.3 on
> Ubuntu 16.04.
> 
> So there must be something else in your setup. If we can figure this out
> within the coming days or weeks, I can still do something about it for
> the Isabelle2018 release.
> 
> 
>   Makarius

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

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

[Makarius]

On 02/07/18 14:50, Makarius wrote:
> 
> So there must be something else in your setup.

Do you maybe have a non-standard Python installation on macOS?


Makarius

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

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

[Makarius]

On 02/07/18 12:59, Max Haslbeck wrote:
> 
> 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]
> 

Thanks for going to the bottom of it. Mercurial.known_files is merely a
command-line invocation as follows:

"${HG:-hg}" --config defaults.status\= --repository
/home/makarius/isabelle/repos --noninteractive status --modified --added
--clean --no-status


I did not see the reported problem: the file names are always relative
to the repository root, independently of the current working directory.
I have tried it Mercurial 4.6.1 on macOS 10.13.5, and Mercurial 3.7.3 on
Ubuntu 16.04.

So there must be something else in your setup. If we can figure this out
within the coming days or weeks, I can still do something about it for
the Isabelle2018 release.


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

Re: [isabelle-dev] Towards Isabelle2018-RC1

[Makarius]

On 02/07/18 14:35, Lars Hupel wrote:
>> I will produce Isabelle2018-RC1 later today, maybe in approx. 3h.
>>
>> For that I also need a version of AFP that works.
> 
> According to , the latest
> known-good version (except for the "slow" sessions) is

The above hint was mainly for people pushing things in the last moment,
lets say within the next 2h.

When doing a release candidate, it often requires some final polishing
and consequently a full test afterwards. I am merely hoping that this
test will work, and I don't have to respin.


Again note that Isabelle2018-RC1 will be still on the main isabelle-dev
repository -- there will be no repository fork yet.


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

Re: [isabelle-dev] Towards Isabelle2018-RC1

[Lars Hupel]

> I will produce Isabelle2018-RC1 later today, maybe in approx. 3h.
> 
> For that I also need a version of AFP that works.

According to , the latest
known-good version (except for the "slow" sessions) is

Isabelle/1b9462304e1d
AFP/2af750da996c
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards Isabelle2018-RC1

[Makarius]

On 26/06/18 20:05, Makarius wrote:
> This is a reminder that the official Isabelle2018-RC1 snapshot is about
> to emerge within a few days (around 01-Jul-2018). The isabelle-dev
> repository fork will *not* happen yet: everyone is called to consolidate
> before and after the Isabelle2018-RC1 checkpoint with robustness and
> stability in mind.

I will produce Isabelle2018-RC1 later today, maybe in approx. 3h.

For that I also need a version of AFP that works.


Makarius

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

Re: [isabelle-dev] Jenkins reconfiguration

[Makarius]

On 29/06/18 19:31, Lars Hupel wrote:
>> Does it mean that the great new hardware is now locked up and
>> exclusively available for Jenkins?
> 
> That assessment is accurate.

That is bad.

It means that the development process will continue to decline, as we
have seen in the past few years -- it can be indirectly see by the
decreasing number of changes, substantial reforms etc. that were pushed
through.


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

Re: [isabelle-dev] Is hgbroy down?

[Lars Hupel]

> Apparently so. I'll let our administrators know.

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

Re: [isabelle-dev] Is hgbroy down?

[Lars Hupel]

> ~/isabelle/Repos/src/HOL: hg fetch
> remote: ssh: connect to host hgbroy.informatik.tu-muenchen.de port 22: 
> Operation timed out
> abort: no suitable response from remote hg!

Apparently so. I'll let our administrators know.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[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] 
>

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] Is hgbroy down?

[Lawrence Paulson]

~/isabelle/Repos/src/HOL: hg fetch
remote: ssh: connect to host hgbroy.informatik.tu-muenchen.de port 22: 
Operation timed out
abort: no suitable response from remote hg!

Larry

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