Your message dated Sun, 11 Feb 2007 18:32:04 +0000
with message-id <[EMAIL PROTECTED]>
and subject line Bug#400535: fixed in coq 8.1~gamma-4
has caused the attached Bug report 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 I am
talking about this indicates a serious mail system misconfiguration
somewhere. Please contact me immediately.)
Debian bug tracking system administrator
(administrator, Debian Bugs database)
--- Begin Message ---
Package: coq
Version: 8.1~gamma-2
Severity: serious
Hi,
your package failed to build from source because it couldn't
find the ocamlopt command. I'm honestly not sure whether this
is a bug in your build-depends or in ocaml-nox, which seems to
have provided this command in the past, but doesn't do so anymore.
| Automatic build of coq_8.1~gamma-2 on meitner by sbuild/hppa 79
| Build started at 20061126-1620
| ******************************************************************************
| coq_8.1~gamma-2.dsc exists in cwd
| ** Using build dependencies supplied by package:
| Build-Depends: debhelper (>= 4.0.0), dpkg-dev (>= 1.13.19), dpatch, ocaml-nox
(>= 3.09.0), ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0),
tetex-extra, hevea
| ** Filtered missing central deps that are dependencies of or provide
build-deps:
| libncurses5-dev (>= 5.3.20030510-1)
[...]
| make[1]: Leaving directory `/build/buildd/coq-8.1~gamma'
| NATIVE CODE COMPILATION FAILED
| Coq was built in bytecode instead
| /usr/bin/make glob.dump
| make[1]: Entering directory `/build/buildd/coq-8.1~gamma'
| rm -f glob.dump
| rm -f theories/*/*.vo
| /usr/bin/make GLOB="-dump-glob glob.dump" world
| make[2]: Entering directory `/build/buildd/coq-8.1~gamma'
| OCAMLOPT config/coq_config.ml
| /bin/sh: ocamlopt: command not found
| make[2]: *** [config/coq_config.cmx] Error 127
| make[2]: Leaving directory `/build/buildd/coq-8.1~gamma'
| make[1]: *** [glob.dump] Error 2
| make[1]: Leaving directory `/build/buildd/coq-8.1~gamma'
| make: *** [build-stamp] Error 2
| ******************************************************************************
| Build finished at 20061126-1809
| FAILED [dpkg-buildpackage died]
Full build log(s):
http://experimental.ftbfs.de/build.php?&ver=8.1~gamma-2&pkg=coq&arch=hppa
Gruesse,
--
Frank Lichtenheld <[EMAIL PROTECTED]>
www: http://www.djpig.de/
--- End Message ---
--- Begin Message ---
Source: coq
Source-Version: 8.1~gamma-4
We believe that the bug you reported is fixed in the latest version of
coq, which is due to be installed in the Debian FTP archive:
coq-libs_8.1~gamma-4_all.deb
to pool/main/c/coq/coq-libs_8.1~gamma-4_all.deb
coq_8.1~gamma-4.diff.gz
to pool/main/c/coq/coq_8.1~gamma-4.diff.gz
coq_8.1~gamma-4.dsc
to pool/main/c/coq/coq_8.1~gamma-4.dsc
coq_8.1~gamma-4_i386.deb
to pool/main/c/coq/coq_8.1~gamma-4_i386.deb
coqide_8.1~gamma-4_i386.deb
to pool/main/c/coq/coqide_8.1~gamma-4_i386.deb
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 [EMAIL PROTECTED],
and the maintainer will reopen the bug report if appropriate.
Debian distribution maintenance software
pp.
Samuel Mimram <[EMAIL PROTECTED]> (supplier of updated coq 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 [EMAIL PROTECTED])
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Format: 1.7
Date: Sun, 11 Feb 2007 18:02:49 +0100
Source: coq
Binary: coqide coq-libs coq
Architecture: source i386 all
Version: 8.1~gamma-4
Distribution: experimental
Urgency: low
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Samuel Mimram <[EMAIL PROTECTED]>
Description:
coq - proof assistant for higher-order logic (toplevel and compiler)
coq-libs - proof assistant for higher-order logic (theories)
coqide - proof assistant for higher-order logic (gtk interface)
Closes: 400535
Changes:
coq (8.1~gamma-4) experimental; urgency=low
.
* Correctly build glob.dump on non-native archs, closes: #400535.
Files:
764fd9afaa2805b30dc28fa8cd99e3dc 945 math optional coq_8.1~gamma-4.dsc
5f7094afff6a0b0ef0586784694bdb90 14185 math optional coq_8.1~gamma-4.diff.gz
cc7c480ef2568e7ec6138f0b5e54552e 14581038 math optional
coq-libs_8.1~gamma-4_all.deb
64216e305953a33b4e99092a56d90a39 6307048 math optional coq_8.1~gamma-4_i386.deb
7394d1e7a8538d75a508ce5dee553961 4587346 math optional
coqide_8.1~gamma-4_i386.deb
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
iD8DBQFFz176Iae1O4AJae8RAig5AJwPcGDhdWe0E2Fa7yaxiFxs1nFh/ACeOQj5
zjmz3ij+6/FHCUhiAI99Mqs=
=dD9B
-----END PGP SIGNATURE-----
--- End Message ---
