Viewing error messages as they are printed by Coq
The CtCoq interface processes the error messages from Coq before printing
them in its message window. Unfortunately, there has been so far no
arrangement with the Coq group to provide a regular form of error messages.
For this reason, it may happen that some of the information in the
error message is lost before printing by CtCoq. To have a view where
you see the exact error message, you can open a new xterm window
and run the command coqserver-spy in this window. This command
will print all the answers from Coq to requests from the CtCoq user-interface.
In particular, you will see the error messages the way they are really produced
by CtCoq. Beware though, that this may make the interaction slower.
Adapting CtCoq to the actual setting of your X server
It may happen that the character fonts available on your X server are not the
same as the ones with which we have designed the interface. When this is
the case, you can adapt your setting using the tool we called caff
(the acronym for Check All the F**ing Fonts). This tool checks that
the fonts requested in the resources are available on you X server and
gives indications to solve the problem when this is not the case.
Yves Bertot
Last modified: Tue Sep 24 10:43:52 MET DST