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

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

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

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

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

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:

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

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

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

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

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

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

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

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

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

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

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

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 +

Re: [isabelle-dev] Towards Isabelle2018-RC1

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

Re: [isabelle-dev] Towards Isabelle2018-RC1

> 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

Re: [isabelle-dev] Towards Isabelle2018-RC1

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

Re: [isabelle-dev] Jenkins reconfiguration

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

Re: [isabelle-dev] Is hgbroy down?

> 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?

> ~/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

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

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.

[isabelle-dev] Is hgbroy down?

~/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