Opened 14 years ago

Closed 8 years ago

#22726 closed defect (fixed)

Cannot compile LaTeX doc for Coq

Reported by: hippallium-macports@… Owned by: pmetzger (Perry E. Metzger)
Priority: Normal Milestone:
Component: ports Version: 1.8.1
Keywords: LaTeX Cc: Ionic (Mihai Moldovan)
Port: coq

Description

$ sudo port install coq +coqide +doc

--->  Fetching coq
--->  Attempting to fetch coq-8.2pl1.tar.gz from http://distfiles.macports.org/coq
--->  Verifying checksum(s) for coq
--->  Extracting coq
--->  Applying patches to coq
--->  Configuring coq
--->  Building coq
Error: Target org.macports.build returned: shell command " cd "/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_ports_lang_coq/work/coq-8.2pl1" && /usr/bin/make -j2 world " returned error 2
Command output: 
! Extra }, or forgotten dgroup. (file Reference-Manual.tex)
l.188 }

I've deleted a group-closing symbol because it seems to be
spurious, as in `$x}$'. But perhaps the } is legitimate and
you forgot something else, as in `\hbox{$x}'. In such cases
the way to recover is to insert both the forgotten and the
deleted material, e.g., by typing `I$}'.

) (./RefMan-modr.aux) (./RefMan-oth.v.aux) (./RefMan-pro.aux) (./RefMan-tac.v.a
ux) (./RefMan-ltac.v.aux) (./RefMan-tacex.v.aux) (./RefMan-decl.v.aux) (./RefMa
n-syn.v.aux) (./RefMan-com.aux) (./RefMan-uti.aux) (./RefMan-ide.aux) (./AddRef
Man-pre.aux) (./Cases.v.aux) (./Coercion.v.aux) (./Classes.v.aux) (./Omega.v.au
x) (./Micromega.v.aux) (./Extraction.v.aux) (./Program.v.aux) (./Polynom.v.aux)
Runaway argument?
{! File ended while scanning use of \@writefile. (file Reference-Manual.tex)
<inserted text>
\par
l.46 \@input{Polynom.v.aux}

I suspect you have forgotten a `}', causing me
to read past where you wanted me to stop.
I'll try to recover; but if the error is serious,
you'd better type `E' or `X' now and fix your file.

make[1]: *** [doc/refman/Reference-Manual.pdf] Error 1
make[1]: *** Waiting for unfinished jobs....
LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.
make: *** [world] Error 2

Error: Status 1 encountered during processing.

$ sudo port install coq +coqide +doc

--->  Computing dependencies for coq
--->  Building coq
--->  Staging coq into destroot
--->  Installing coq @8.2pl1_1+coqide+doc
--->  Activating coq @8.2pl1_1+coqide+doc
The style file for LaTeX documentation,
coqdoc.sty, is in /opt/local/share/coq/latex.
Add this to your TEXINPUTS if you wish to
use it.
--->  Cleaning coq

$ 

Change History (4)

comment:1 Changed 14 years ago by mf2k (Frank Schima)

Owner: changed from macports-tickets@… to reilles@…

comment:2 Changed 9 years ago by jmroot (Joshua Root)

Owner: changed from reilles@… to perry@…

comment:3 Changed 8 years ago by pmetzger (Perry E. Metzger)

So far as I can tell, port install coq +doc works fine now. I would like to close this.

comment:4 Changed 8 years ago by Ionic (Mihai Moldovan)

Cc: ionic@… added
Resolution: fixed
Status: newclosed

Closing on maintainer's request.

If the problem still persists, please comment here and the ticket will be reopened.

Note: See TracTickets for help on using tickets.