Opened 15 years ago
Closed 9 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 15 years ago by mf2k (Frank Schima)
Owner: | changed from macports-tickets@… to reilles@… |
---|
comment:2 Changed 10 years ago by jmroot (Joshua Root)
Owner: | changed from reilles@… to perry@… |
---|
comment:3 Changed 9 years ago by pmetzger (Perry E. Metzger)
comment:4 Changed 9 years ago by Ionic (Mihai Moldovan)
Cc: | ionic@… added |
---|---|
Resolution: | → fixed |
Status: | new → closed |
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.
So far as I can tell, port install coq +doc works fine now. I would like to close this.