Package: why
Version: 2.03.dfsg-1
Severity: wishlist
Hello,
I tried to check some simple program usign floats and discovered it
was impossible with why. The reason is that the file WhyFloats.v is
missing, which is caused by the float library missing during the
build. I think it should be possible to check programs with floats,
which could be accomplished by three ways:
Take the float library from http://coq.inria.fr/contribs/Float.tar.gz
and either
- add it to the coq-libs package, and make why build-dep on coq-libs
- make an extra package coq-lib-float, and -"-
- add this library to the why package itself
What do you think?
Regards
Jiri Palecek
-- System Information:
Debian Release: lenny/sid
APT prefers testing
APT policy: (990, 'testing'), (500, 'unstable'), (1, 'experimental')
Architecture: i386 (i686)
Kernel: Linux 2.6.20.3-rt8 (PREEMPT)
Locale: LANG=cs_CZ, LC_CTYPE=cs_CZ (charmap=ISO-8859-2) (ignored: LC_ALL
set to cs_CZ)
Shell: /bin/sh linked to /bin/dash
Versions of packages why depends on:
ii libatk1.0-0 1.18.0-2 The ATK accessibility toolkit
ii libc6 2.5-11 GNU C Library: Shared
libraries
ii libcairo2 1.4.6-1.1 The Cairo 2D vector graphics
libra
ii libfontconfig1 2.4.2-1.2 generic font configuration
library
ii libglib2.0-0 2.12.12-1 The GLib library of C routines
ii libgtk2.0-0 2.10.13-1 The GTK+ graphical user
interface
ii libpango1.0-0 1.16.4-1 Layout and rendering of
internatio
ii libx11-6 2:1.0.3-7 X11 client-side library
ii libxcursor1 1:1.1.8-2 X cursor management library
ii libxext6 1:1.0.3-2 X11 miscellaneous extension
librar
ii libxfixes3 1:4.0.3-2 X11 miscellaneous 'fixes'
extensio
ii libxi6 1:1.0.1-4 X11 Input extension library
ii libxinerama1 1:1.0.2-1 X11 Xinerama extension library
ii libxrandr2 2:1.2.1-1 X11 RandR extension library
ii libxrender1 1:0.9.2-1 X Rendering Extension client
libra
why recommends no packages.
-- no debconf information
