Re: [isabelle] Failing afp-2015 build

On 7 Dec 2015, at 22:19, Makarius <makarius at> wrote:
> That is almost 3 weeks old, and nothing has happened yet.  I am routinely on afp-devel, but not the official release branches. Ultimately, it is the job of the AFP authors to maintain their material.

Makarius, I am on holidays presently and will not get to this until February 2016 or later.

You have previously pushed substantial changes to ConcurrentGC without discussing them with me at all, and I donât see why this should be any different. If it is important to you, go ahead and commit it. It should be clear that I simply want those tactics to work - I have no deep insight into the Isabelle tactic API, for otherwise I would have got it right before now. If it were my project, I would take this as an opportunity to make the Isabelle tactic API more robust, so people like me donât cause maintenance headaches for people like you.

As for runtimes: Florianâs email on isabelle-dev 2015-11-26 (why is this thread Iâm responding to on isabelle-users? Arenât we talking about the development version of the AFP for the upcoming Isabelle2016 release? *brain explodes*):

> For the record:
>> Running on host lxbroy10
>> isabelle: fc53fbf9fe01 tip
>> afp: 835c7e115feb tip
>> Running ConcurrentGC ...
>> Finished ConcurrentGC (1:08:48 elapsed time, 5:15:14 cpu time, factor 4.58)
>> 1:21:59 elapsed time, 5:53:13 cpu time, factor 4.30

Five hours of CPU seems excessive. Is this machine ancient? I donât remember it being this bad when I submitted it to the AFP.

> Just from the English, what does âPerhaps itâs a wash at this stage." meand?

As for English idioms, I would start by asking Google; it seems the phrase âitâs a washâ has a few interpretations. I humbly suggest you avoid using the passive voice as it tends to come across as aggressive. In many cases it distracts me and other subscribers from the often valid points you are making.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.