Bug#459050: marked as done (coq: FTBFS with dash: Error while loading "parsing/q_constr.cmo": file not found in path.)
Your message dated Sat, 05 Jan 2008 09:32:04 +0000
with message-id <E1JB5Ns-0006ua-AN@ries.debian.org>
and subject line Bug#459050: fixed in coq 8.1.pl3+dfsg-1
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.pl2+dfsg-3
User: debian-qa@lists.debian.org
Usertags: qa-ftbfs-dash-20080103 qa-ftbfs-dash
Hi,
During a rebuild of all packages in sid using /bin/dash as /bin/sh, your package failed to build.
Relevant part:
> OCAMLC pretyping/pretyping.mli
> OCAMLC pretyping/pretyping.ml
> OCAMLC pretyping/matching.mli
> OCAMLC pretyping/matching.ml
> OCAMLC -a -o pretyping/pretyping.cma
> OCAMLC parsing/lexer.mli
> OCAMLC4 parsing/lexer.ml4
> OCAMLC interp/topconstr.ml
> OCAMLC interp/ppextend.mli
> OCAMLC interp/ppextend.ml
> OCAMLC interp/notation.mli
> OCAMLC interp/notation.ml
> OCAMLC interp/genarg.ml
> OCAMLC interp/syntax_def.mli
> OCAMLC interp/syntax_def.ml
> OCAMLC interp/reserve.mli
> OCAMLC interp/reserve.ml
> OCAMLC library/impargs.mli
> OCAMLC library/impargs.ml
> OCAMLC interp/constrintern.mli
> OCAMLC interp/constrintern.ml
> OCAMLC interp/modintern.mli
> OCAMLC interp/modintern.ml
> OCAMLC interp/constrextern.mli
> OCAMLC interp/constrextern.ml
> OCAMLC interp/coqlib.mli
> OCAMLC interp/coqlib.ml
> OCAMLC toplevel/discharge.mli
> OCAMLC toplevel/discharge.ml
> OCAMLC library/declare.mli
> OCAMLC library/declare.ml
> OCAMLC -a -o interp/interp.cma
> OCAMLC proofs/decl_expr.mli
> OCAMLC proofs/proof_type.mli
> OCAMLC proofs/proof_type.ml
> OCAMLC proofs/redexpr.mli
> OCAMLC proofs/redexpr.ml
> OCAMLC proofs/proof_trees.mli
> OCAMLC proofs/proof_trees.ml
> OCAMLC proofs/logic.mli
> OCAMLC proofs/logic.ml
> OCAMLC proofs/refiner.mli
> OCAMLC proofs/refiner.ml
> OCAMLC proofs/evar_refiner.mli
> OCAMLC proofs/evar_refiner.ml
> OCAMLC proofs/tacmach.mli
> OCAMLC proofs/tacmach.ml
> OCAMLC proofs/pfedit.mli
> OCAMLC proofs/pfedit.ml
> OCAMLC proofs/tactic_debug.mli
> OCAMLC proofs/tactic_debug.ml
> OCAMLC proofs/clenvtac.mli
> OCAMLC proofs/clenvtac.ml
> OCAMLC proofs/decl_mode.mli
> OCAMLC proofs/decl_mode.ml
> OCAMLC -a -o proofs/proofs.cma
> OCAMLC parsing/extend.mli
> OCAMLC parsing/extend.ml
> OCAMLC toplevel/vernacexpr.ml
> OCAMLC parsing/pcoq.mli
> OCAMLC4 parsing/pcoq.ml4
> OCAMLC parsing/egrammar.mli
> OCAMLC parsing/egrammar.ml
> OCAMLC4 parsing/g_xml.ml4
> OCAMLC parsing/ppconstr.mli
> OCAMLC parsing/ppconstr.ml
> OCAMLC parsing/printer.mli
> OCAMLC parsing/printer.ml
> OCAMLC parsing/pptactic.mli
> OCAMLC -rectypes parsing/pptactic.ml
> OCAMLC parsing/ppdecl_proof.mli
> OCAMLC parsing/ppdecl_proof.ml
> OCAMLC parsing/tactic_printer.mli
> OCAMLC parsing/tactic_printer.ml
> OCAMLC parsing/printmod.mli
> OCAMLC parsing/printmod.ml
> OCAMLC parsing/prettyp.mli
> OCAMLC parsing/prettyp.ml
> OCAMLC parsing/search.mli
> OCAMLC parsing/search.ml
> OCAMLC -a -o parsing/parsing.cma
> OCAMLC tactics/dn.mli
> OCAMLC tactics/dn.ml
> OCAMLC tactics/termdn.mli
> OCAMLC tactics/termdn.ml
> OCAMLC tactics/btermdn.mli
> OCAMLC tactics/btermdn.ml
> OCAMLC tactics/nbtermdn.mli
> OCAMLC tactics/nbtermdn.ml
> OCAMLC tactics/tacticals.mli
> OCAMLC tactics/tacticals.ml
> OCAMLC tactics/hipattern.mli
> OCAMLC4 tactics/hipattern.ml4
> Error while loading "parsing/q_constr.cmo": file not found in path.
> Preprocessor error
> make[2]: *** [tactics/hipattern.cmo] Error 2
> make[2]: Leaving directory `/build/user/coq-8.1.pl2+dfsg'
> make[1]: *** [world] Error 2
> make[1]: Leaving directory `/build/user/coq-8.1.pl2+dfsg'
> make: *** [build-stamp] Error 2
> dpkg-buildpackage: failure: debian/rules build gave error exit status 2
The full build log is available from:
http://people.debian.org/~lucas/logs/2008/01/03.dash/
Rumors say that Ubuntu is using dash as /bin/sh on their buildds, so a patch
might be available. Check <http://packages.qa.debian.org/coq>, or
directly on launchpad: <https://launchpad.net/ubuntu/+source/coq>.
A list of current common problems and possible solutions is available at
http://wiki.debian.org/qa.debian.org/FTBFS . You're welcome to contribute!
--
| Lucas Nussbaum
| lucas@lucas-nussbaum.net http://www.lucas-nussbaum.net/ |
| jabber: lucas@nussbaum.fr GPG: 1024D/023B3F4F |
--- End Message ---
--- Begin Message ---
Source: coq
Source-Version: 8.1.pl3+dfsg-1
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.pl3+dfsg-1_all.deb
to pool/main/c/coq/coq-libs_8.1.pl3+dfsg-1_all.deb
coq_8.1.pl3+dfsg-1.diff.gz
to pool/main/c/coq/coq_8.1.pl3+dfsg-1.diff.gz
coq_8.1.pl3+dfsg-1.dsc
to pool/main/c/coq/coq_8.1.pl3+dfsg-1.dsc
coq_8.1.pl3+dfsg-1_i386.deb
to pool/main/c/coq/coq_8.1.pl3+dfsg-1_i386.deb
coq_8.1.pl3+dfsg.orig.tar.gz
to pool/main/c/coq/coq_8.1.pl3+dfsg.orig.tar.gz
coqide_8.1.pl3+dfsg-1_i386.deb
to pool/main/c/coq/coqide_8.1.pl3+dfsg-1_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 459050@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.
Debian distribution maintenance software
pp.
Samuel Mimram <smimram@debian.org> (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 ftpmaster@debian.org)
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Format: 1.7
Date: Fri, 04 Jan 2008 13:21:43 +0000
Source: coq
Binary: coqide coq-libs coq
Architecture: source all i386
Version: 8.1.pl3+dfsg-1
Distribution: unstable
Urgency: low
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Samuel Mimram <smimram@debian.org>
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: 459050
Changes:
coq (8.1.pl3+dfsg-1) unstable; urgency=low
.
[ Stefano Zacchiroli ]
* fix vcs-svn field to point just above the debian/ dir
.
[ Samuel Mimram ]
* New upstream release.
* Makefile should now be compatible with dash, closes: #459050.
* Updated watch file.
Files:
ad66f75e3da720e59c388d7296a7fb2d 1070 math optional coq_8.1.pl3+dfsg-1.dsc
35571b435de17bc560f018be53585822 2534628 math optional coq_8.1.pl3+dfsg.orig.tar.gz
f56b319a4f74365422613f6614524961 15578 math optional coq_8.1.pl3+dfsg-1.diff.gz
ccfc98f81a253b6570486a1b7ecbc348 12591954 math optional coq-libs_8.1.pl3+dfsg-1_all.deb
74a6b5ab00d801b8973aac89013e4442 8445120 math optional coq_8.1.pl3+dfsg-1_i386.deb
059c52306e39c094c164d3b08b289aa8 4919202 math optional coqide_8.1.pl3+dfsg-1_i386.deb
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
iD8DBQFHf0ujIae1O4AJae8RAtRMAJ9a/NqbOUPzJHstMf8MzN6uuEn9xgCfXoLf
bjOFStz+SMgWtiEMZIB0nUM=
=d8kG
-----END PGP SIGNATURE-----
--- End Message ---
Reply to: