coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
Archive powered by MHonArc 2.6.18.