building pdf fails because of comments
igloo at earth.li
Wed Dec 8 12:42:17 EST 2010
On Wed, Dec 08, 2010 at 03:47:39PM +0100, Andrzej Giniewicz wrote:
> I was following the project for quite a while, you are doing quite
> impressive work here!
> When I noticed, that camp switched to coq 8.3
> (which comes with my distro) I decided to give it a try. The build
> "make coq" goes fine (after update to latest 8.3 from svn, though as I
> started already I did that too),
Right, I ran into a couple of show-stopper coq bugs in the last few
days, so you really do need the latest patches from the branch.
Incidentally, what I'm currently working on is a proof that catches
satisfy the patchlike axioms.
> but building pdf fails
Sorry about that; I've been focussing on the proof lately, so not
building the PDF.
(and as a result, the PDF is probably a bit out of sync with the proofs.
And generally lacking in text for that matter).
> but I didn't found a way to output % into .tex file.
The trick is to give up, and use # instead :-)
% We can't use % as a comment character in files that go through coqdoc,
% as it uses that as the latex escape character. Sigh. So we use #
I've pushed a patch to fix this up, and also correct a few include
More information about the Camp