Re: [isabelle] Failing afp-2015 build
On Tue, 8 Dec 2015, Peter Gammie wrote:
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.
I have no problems to push that on afp-devel, but thus it won't be on
afp-2015. The start of the thread (and its subject line) is about
afp-2015: Lars Hupel reported problems that are relevant for that release
branch, for continuous testing in sequential mode.
Isabelle and AFP are not just a sink for material. It is continuously
crunched and continuosly improved, especially for performance and
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.
The tactic API is from 1989 and cannot be changed without changing almost
everything of the Paulson goal state representation (which was a big asset
in its time, and still has many benefits that other ITP systems lack).
The "implementation" manual is quite explicit about what the ML type
tactic (and Proof.method) mean semantically. It is OK to ignore manuals
in the first round. It is not OK to complain about the existence of
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.
The machine is ancient, but ConcurrentGC has always been that slow.
Before I made some changes with 'subgoal' it was even slower -- approx. by
a factor 1.5.
Just from the English, what does âPerhaps itâs a wash at this stage."
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.
Sorry, I don't know English slang, only international scientific pidgin.
So far the agressions has been mostly on the side of the massive
ConcurrentGC session, which has sucked up quite a lot of resources of
everybody involved in ongoing Isabelle + AFP maintenance.
It is still unclear to me, why these proofs are so slow. You as the
author should know.
This archive was generated by a fusion of
Pipermail (Mailman edition) and