Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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.

Top of Page