Stream: Coq devs & plugin devs

Topic: latex1 test from test-suite fails

Pierre-Marie Pédrot (Aug 23 2022 at 20:42):

Hi all, I've recently updated my texlive package on Debian unstable (to version 2022.20220722-1) and now I'm getting weird errors from test-suite/coq-makefile/latex1.v.

Pierre-Marie Pédrot (Aug 23 2022 at 20:43):

I get a bunch of

! Argument of <C2> has an extra }.
<inserted text>
                \par
l.24 ...t.sub.testsub}{Library }{test.sub.testsub}

Runaway argument?

Pierre-Marie Pédrot (Aug 23 2022 at 20:44):

Did I break something in my installation, or is the Coq tex wrapper incompatible with the latest TexLive release?

Julien Puydt (Aug 24 2022 at 06:58):

I'll see if coq-doc compiles with a recent unstable -- I didn't check that when I did my Coq 8.16 work

Julien Puydt (Aug 24 2022 at 07:17):

The compilation of coq-doc 8.15.2 just went through. [Reminder: coq-doc is the non-free package building the Coq documentation in Debian]

Last updated: May 28 2023 at 16:30 UTC