coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Debug output in PG / XML, now disabled by default

From: "Paul A. Steckler" <steck AT stecksoft.com>
To: Coqdev <coqdev AT inria.fr>, coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Debug output in PG / XML, now disabled by default
Date: Fri, 16 Sep 2016 12:18:25 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=stecksoft AT gmail.com; spf=Pass smtp.mailfrom=stecksoft AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f54.google.com
Ironport-phdr: 9a23:IaryVR25yuusGd3VsmDT+DRfVm0co7zxezQtwd8ZsegXKfad9pjvdHbS+e9qxAeQG96KsrQb1KGH6OigATVGusnR9ihaMdRlbFwst4Y/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbre9JomHpMOu2+2ss8nYZBxEiSSVYLVoLRzwox+H8oEdhpInIaIswFOdqXxRPu9S2GlAJFSJnh+66N3mr7B59CEF8coo6soIeOOyRLg1Rr9cAS5sezQu+MDgtjHYUQaE5WAbXHlQmR1NVVuWpCrmV4v853Op/tF23zOXaJX7

A couple of people mentioned to me that the debug output in the Proof
General fork that uses XML was slow, due to debugging output.

I've pushed code that disables the debugging output by default. Also,
the HOWTO-USE file explains how to disable the traffic logging, if
things are still too slow.

My last message has gotten a few more people to clone the repo. Thanks
to all who are trying out the code.

-- Paul

[Coq-Club] Debug output in PG / XML, now disabled by default, Paul A. Steckler, 09/16/2016