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 robustness.

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 manuals.

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." 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.

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 MHonArc.