Bug#498713: No why-related *.vo files in coq/user-contrib
Package: why
Version: 2.15-1.1
Severity: important
Hi,
compiling why 2.15 with the debian/ from pkg-ocaml-maint in svn.debian.org
prevents *.vo files from being put in /usr/lib/coq/user-contrib.
This is because (see install-coq-v8 in Makefile.in) the makefile tests for
the existence and writeability of COQDIR, which at package compilation is
debian/why/usr/lib/coq but actually does not exists. Hence the *.vo are put
in $(LIBDIR)/why/coq (with a warning message).
I think this makes using why "out-of-the-box" difficult with Coq.
I tried for my own version of the package (hence the "Version" above) by
adding the following line in debian/rules (with some context):
##########################
dh_installdirs
+ mkdir -p $(CURDIR)/debian/why/usr/lib/coq
$(MAKE) prefix=$(CURDIR)/debian/why/usr install COQLIB=$(CURDIR)/debian/why/usr/lib/coq
mkdir -p $(CURDIR)/debian/why/usr/lib/coq
##########################
I suspect adding usr/lib/coq to a debian/dirs file would also do the trick,
but I did not test this solution.
Regards,
Samuel Colin
-- System Information:
Debian Release: lenny/sid
APT prefers testing
APT policy: (500, 'testing')
Architecture: i386 (i686)
Kernel: Linux 2.6.25 (PREEMPT)
Locale: LANG=C, LC_CTYPE=fr_FR.UTF8 (charmap=UTF-8)
Shell: /bin/sh linked to /bin/bash
Versions of packages why depends on:
ii libatk1.0-0 1.22.0-1 The ATK accessibility toolkit
ii libc6 2.7-13 GNU C Library: Shared libraries
ii libcairo2 1.6.4-6 The Cairo 2D vector graphics libra
ii libglib2.0-0 2.16.5-1 The GLib library of C routines
ii libgtk2.0-0 2.12.11-3 The GTK+ graphical user interface
ii libpango1.0-0 1.20.5-2 Layout and rendering of internatio
why recommends no packages.
Versions of packages why suggests:
ii coq 8.1.pl3+dfsg-1+b2 proof assistant for higher-order l
-- no debconf information
Reply to: