coq 8.4pl1 doesn't install

[xavierleroy]

On Ubuntu 12.04 LTS:

==== ERROR [while installing coq.8.4pl1] ====
# opam-version    0.9.3 (0.9.3-2-g2a64f59)
# os              linux
# command         make world
# path            /home/xleroy/.opam/4.00.1/build/coq.8.4pl1
# exit-code       2
# env-file        /home/xleroy/.opam/4.00.1/build/coq.8.4pl1/coq-60459a.env
# stdout-file     /home/xleroy/.opam/4.00.1/build/coq.8.4pl1/coq-60459a.out
# stderr-file     /home/xleroy/.opam/4.00.1/build/coq.8.4pl1/coq-60459a.err
### stdout ###
...[truncated]
1460 strings out of 495062
15866 string characters out of 1182644
61348 words of memory out of 3000000
4677 multiletter control sequences out of 15000+50000
4709 words of font info for 16 fonts, out of 3000000 for 9000
28 hyphenation exceptions out of 8191
27i,0n,24p,228b,37s stack positions out of 5000i,500n,10000p,200000b,50000s
No pages of output.

make[1]: Leaving directory `/home/xleroy/.opam/4.00.1/build/coq.8.4pl1'
### stderr ###
...[truncated]
Usage: makeindex [-ilqrcgLT] [-s sty] [-o ind] [-t log] [-p num] [idx0 idx1 ...]
egrep: Reference-Manual.ilg: No such file or directory
Input index file Reference-Manual.comidx not found.
Usage: makeindex [-ilqrcgLT] [-s sty] [-o ind] [-t log] [-p num] [idx0 idx1 ...]
egrep: Reference-Manual.ilg: No such file or directory
Input index file Reference-Manual.erridx not found.
Usage: makeindex [-ilqrcgLT] [-s sty] [-o ind] [-t log] [-p num] [idx0 idx1 ...]
egrep: Reference-Manual.ilg: No such file or directory
make[1]: *** [doc/refman/Reference-Manual.dvi] Error 1
make: *** [world] Error 2

I am also suspicious that lablgtk2 wasn't compiled as a dependency. Does this package provide coqide? This is an essential part of Coq.

[avsm]

I don't see this on Ubuntu Raring x86_64 and OPAM-0.9.{5/6}; I suspect you're missing some system library/tool for compiling the documentation, but can't be sure from the truncated output. If you update your OPAM to the latest 0.9.6, and try opam install lablgtk coq --verbose, that will show you the full build output, and give you coqide too.

Lablgtk is an optional dependency in the package. If lablgtk is installed (either at the same time as Coq, or subsequently), then Coq will be recompiled to include coqide. Lablgtk is a bit painful to install on MacOS X due to a broken pkg-config (#112), and so GTK isn't a hard dependency as the command line bits do compile independently.

[avsm]

Confirmed that coqide compiled on Raring too, when lablgtk was installed:

install -d "/home/avsm/.opam/system/share/coq"
install -m 644  ide/coq.png "/home/avsm/.opam/system/share/coq"
install -d "/home/avsm/.opam/system/lib/coq/config"
install -m 644  ide/coqide-gtk2rc "/home/avsm/.opam/system/lib/coq/config"
if [ X11 = QUARTZ ] ; then install -m 644  ide/mac_default_accel_map "/home/avsm/.opam/system/lib/coq/config"/coqide.keys ; fi
install -d "/home/avsm/.opam/system/doc"
install -m 644  ide/FAQ "/home/avsm/.opam/system/doc"/FAQ-CoqIde
make[1]: Leaving directory `/home/avsm/.opam/system/build/coq.8.4pl1'
Installing coq.8.4pl1.
$  coqide
coqide      coqide.opt  

[xavierleroy]

Thanks for the quick feedback. I confirm the problem was due to missing TeX packages. For the record, I had to install no less than 4 packages:
texlive-fonts-recommended
texlive-fonts-extra
texlive-latex-extra
texlive-math-extra
to get Coq's documentation to compile.

[avsm]

Thanks; OPAM 1.0 has support for a depexts field where OS-specific dependencies can be recorded. This will let OS-specific scripts be invoked before the source packages are built. We're still writing those external scripts though...

[samoht]

Closing the issue as it works when the right external dependencies are installed (and the general issue of correctly tracking external dependencies is OCamlPro/opam#399)