Bug#498713: marked as done (No why-related *.vo files in coq/user-contrib)
Your message dated Sun, 22 Mar 2009 16:49:11 +0000
with message-id <E1LlQrH-0001Em-CR@ries.debian.org>
and subject line Bug#498713: fixed in why 2.18.dfsg-1
has caused the Debian Bug report #498713,
regarding No why-related *.vo files in coq/user-contrib
to be marked as done.
This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.
(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact owner@bugs.debian.org
immediately.)
--
498713: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=498713
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message ---
- To: Debian Bug Tracking System <submit@bugs.debian.org>
- Subject: No why-related *.vo files in coq/user-contrib
- From: Samuel Colin <samuel.colin@loria.fr>
- Date: Fri, 12 Sep 2008 16:22:18 +0200
- Message-id: <20080912142218.30023.34185.reportbug@tyneth.hivernal.org>
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
--- End Message ---
--- Begin Message ---
Source: why
Source-Version: 2.18.dfsg-1
We believe that the bug you reported is fixed in the latest version of
why, which is due to be installed in the Debian FTP archive:
libjessie-ocaml-dev_2.18.dfsg-1_i386.deb
to pool/main/w/why/libjessie-ocaml-dev_2.18.dfsg-1_i386.deb
libwhy-coq_2.18.dfsg-1_all.deb
to pool/main/w/why/libwhy-coq_2.18.dfsg-1_all.deb
why-examples_2.18.dfsg-1_all.deb
to pool/main/w/why/why-examples_2.18.dfsg-1_all.deb
why_2.18.dfsg-1.diff.gz
to pool/main/w/why/why_2.18.dfsg-1.diff.gz
why_2.18.dfsg-1.dsc
to pool/main/w/why/why_2.18.dfsg-1.dsc
why_2.18.dfsg-1_i386.deb
to pool/main/w/why/why_2.18.dfsg-1_i386.deb
why_2.18.dfsg.orig.tar.gz
to pool/main/w/why/why_2.18.dfsg.orig.tar.gz
A summary of the changes between this version and the previous one is
attached.
Thank you for reporting the bug, which will now be closed. If you
have further comments please address them to 498713@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.
Debian distribution maintenance software
pp.
Mehdi Dogguy <dogguy@pps.jussieu.fr> (supplier of updated why package)
(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmaster@debian.org)
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Format: 1.8
Date: Fri, 27 Feb 2009 14:09:32 +0100
Source: why
Binary: why why-examples libjessie-ocaml-dev libwhy-coq
Architecture: source i386 all
Version: 2.18.dfsg-1
Distribution: unstable
Urgency: low
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Mehdi Dogguy <dogguy@pps.jussieu.fr>
Description:
libjessie-ocaml-dev - Jessie library for code analysis
libwhy-coq - Why library for Coq
why - A software verification tool
why-examples - Examples of programs certified with Why
Closes: 498713
Changes:
why (2.18.dfsg-1) unstable; urgency=low
.
[ Mehdi Dogguy ]
* New upstream release.
* New binary packages:
+ libjessie-ocaml-dev:
- Build and install jc.{cma,cmxa,a} using jessie_lib.dpatch
- Install jc.cmi
- Add a META file for Jessie library
+ why-examples:
- why-examples recommends why
+ libwhy-coq:
- Install .vo files in /usr/lib/coq/user-contrib, closes: #498713.
* debian/rules:
+ do not compress .v,.sx,.why files
+ Use debhelper 7
+ Move logo in /usr/share/why (using logopath.dpatch)
+ Setting up manpages for krakatoa, gwhy-bin, tool-stat and why-config
* debian/control:
+ Bump standards version to 3.8.0, no changes needed.
+ Why recommends alt-ergo and suggest libwhy-coq.
+ Add missing runtime dependency for why (on non-native-architecures).
+ Change vcs-* fields to point to Git repository
+ Depend on coq-${F:CoqABI} instead of Coq
+ Add DMUA flag with Sam's blessing
+ Remove not needed build dependency: ocamlweb
* Add patch descriptions to configure.dpatch and logopath.dpatch
.
[ Samuel Mimram ]
* Use predefined variables from ocamlvars.mk and coqvars.mk.
Checksums-Sha1:
7e03d5fa05acb73354ee975521c425e1661c6122 1452 why_2.18.dfsg-1.dsc
8ca25b8294f801d6955bc5d8556a334290cfb6ce 2409443 why_2.18.dfsg.orig.tar.gz
7b6c87b4ae32dbe85a852ee4e167bc90c3c3d426 7299 why_2.18.dfsg-1.diff.gz
3ed712caa99ad2bf413bea566c67ec612a909b1d 4494240 why_2.18.dfsg-1_i386.deb
696a64904a2b769a67a6f8c9e3ea3dfeba9c9a49 295502 why-examples_2.18.dfsg-1_all.deb
cda4264d6b45f4ecc7a4eb5e886a678f0b344f73 670286 libjessie-ocaml-dev_2.18.dfsg-1_i386.deb
35cc5ee153885b0bfeacfbe51652bd66b9c82c10 370230 libwhy-coq_2.18.dfsg-1_all.deb
Checksums-Sha256:
55cd0d0a9ae51078593d31e733a3537d3abaf3cf5d70e09ae1814365f36285e9 1452 why_2.18.dfsg-1.dsc
ec0aea397806b49096cbbabf271632331d6018e481c7b728b7c7e0b49c9829e1 2409443 why_2.18.dfsg.orig.tar.gz
e32e22cce30c7220e96453fe13d902ef3477319147cc2cfb60e38f260e8e3fb6 7299 why_2.18.dfsg-1.diff.gz
35db88c70b5e90c694d80dc6badbd82c54de15c21e22feab66961d5c01654be5 4494240 why_2.18.dfsg-1_i386.deb
cecd341805120b65a83a3255878e58cbd27e98224fb4abeec3b7c944db459e87 295502 why-examples_2.18.dfsg-1_all.deb
36be24bdfa59d7685159eeac2409e88946b9c2bf248506c65cddb0d8bbc4f09a 670286 libjessie-ocaml-dev_2.18.dfsg-1_i386.deb
9abb89fea1ecbcf99d5e46026f30d1d8c133cd9c65a36df150f3f8b9caf10ce2 370230 libwhy-coq_2.18.dfsg-1_all.deb
Files:
e63dd9f7ea61b34531330538eade9afc 1452 math optional why_2.18.dfsg-1.dsc
d2afe1587e1d09640ee7126ea9e12adc 2409443 math optional why_2.18.dfsg.orig.tar.gz
fa3c4aaaee597e660bd9ab461020eb48 7299 math optional why_2.18.dfsg-1.diff.gz
45f607afa38c0149613aabf8bfd8d874 4494240 math optional why_2.18.dfsg-1_i386.deb
5a9271f9daa32921f7b7367fbe3b66a3 295502 doc optional why-examples_2.18.dfsg-1_all.deb
f8dc15d48cff45a62727cd20c9b33079 670286 libdevel optional libjessie-ocaml-dev_2.18.dfsg-1_i386.deb
0d1a9073b7bb355ce6c080528c949cea 370230 libdevel optional libwhy-coq_2.18.dfsg-1_all.deb
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.9 (GNU/Linux)
iEYEARECAAYFAknGU6wACgkQIae1O4AJae+HEQCcDx2x3dib3jJWUyXzZTUkptUh
xwAAn1Zho0huVNdJof6Dzl++7927th9f
=IsNv
-----END PGP SIGNATURE-----
--- End Message ---
Reply to: