Source: ssreflect Version: 1.5-3 Severity: serious Justification: fails to build from source User: [email protected] Usertags: ftbfs X-Debbugs-Cc: [email protected]
Dear Maintainer,
ssreflect fails to build from source in unstable/amd64:
[..]
/usr/bin/ocamldep.opt -slash -I "src" -pp '/usr/bin/camlp5o -I
/usr/lib/ocaml/ -I /usr/lib/ocaml/threads/ -I "/usr/lib/coq/kernel" -I
"/usr/lib/coq/lib" -I "/usr/lib/coq/library" -I "/usr/lib/coq/parsing" -I
"/usr/lib/coq/pretyping" -I "/usr/lib/coq/interp" -I "/usr/lib/coq/printing" -I
"/usr/lib/coq/intf" -I "/usr/lib/coq/proofs" -I "/usr/lib/coq/tactics" -I
"/usr/lib/coq/tools" -I "/usr/lib/coq/toplevel" -I "/usr/lib/coq/stm" -I
"/usr/lib/coq/grammar" -I "/usr/lib/coq/config" -I
"/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I
"/usr/lib/coq//plugins/decl_mode" -I "/usr/lib/coq//plugins/derive" -I
"/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I
"/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I
"/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I
"/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/quote" -I
"/usr/lib/coq//plugins/romega" -I "/usr/lib/coq//plugins/rtauto" -I
"/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/syntax" -I
"/usr/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo
unix.cma threads.cma grammar.cma -loc loc -impl' -impl "src/ssrmatching.ml4" >
"src/ssrmatching.ml4.d" || ( RV=$?; rm -f "src/ssrmatching.ml4.d"; exit ${RV} )
"/usr/bin//coqdep" -c -R "theories" Ssreflect -I "src" "theories/fintype.v" >
"theories/fintype.v.d" || ( RV=$?; rm -f "theories/fintype.v.d"; exit ${RV} )
"/usr/bin//coqdep" -c -R "theories" Ssreflect -I "src" "theories/choice.v" >
"theories/choice.v.d" || ( RV=$?; rm -f "theories/choice.v.d"; exit ${RV} )
"/usr/bin//coqdep" -c -R "theories" Ssreflect -I "src" "theories/seq.v" >
"theories/seq.v.d" || ( RV=$?; rm -f "theories/seq.v.d"; exit ${RV} )
"/usr/bin//coqdep" -c -R "theories" Ssreflect -I "src" "theories/ssrnat.v" >
"theories/ssrnat.v.d" || ( RV=$?; rm -f "theories/ssrnat.v.d"; exit ${RV} )
"/usr/bin//coqdep" -c -R "theories" Ssreflect -I "src" "theories/eqtype.v" >
"theories/eqtype.v.d" || ( RV=$?; rm -f "theories/eqtype.v.d"; exit ${RV} )
"/usr/bin//coqdep" -c -R "theories" Ssreflect -I "src" "theories/ssrbool.v" >
"theories/ssrbool.v.d" || ( RV=$?; rm -f "theories/ssrbool.v.d"; exit ${RV} )
"/usr/bin//coqdep" -c -R "theories" Ssreflect -I "src" "theories/ssrfun.v" >
"theories/ssrfun.v.d" || ( RV=$?; rm -f "theories/ssrfun.v.d"; exit ${RV} )
"/usr/bin//coqdep" -c -R "theories" Ssreflect -I "src" "theories/ssreflect.v"
> "theories/ssreflect.v.d" || ( RV=$?; rm -f "theories/ssreflect.v.d"; exit
${RV} )
"/usr/bin//coqdep" -c -R "theories" Ssreflect -I "src"
"theories/ssrmatching.v" > "theories/ssrmatching.v.d" || ( RV=$?; rm -f
"theories/ssrmatching.v.d"; exit ${RV} )
/usr/bin/ocamlc.opt -c -rectypes -thread -I "src" -I "/usr/lib/coq/kernel"
-I "/usr/lib/coq/lib" -I "/usr/lib/coq/library" -I "/usr/lib/coq/parsing" -I
"/usr/lib/coq/pretyping" -I "/usr/lib/coq/interp" -I "/usr/lib/coq/printing" -I
"/usr/lib/coq/intf" -I "/usr/lib/coq/proofs" -I "/usr/lib/coq/tactics" -I
"/usr/lib/coq/tools" -I "/usr/lib/coq/toplevel" -I "/usr/lib/coq/stm" -I
"/usr/lib/coq/grammar" -I "/usr/lib/coq/config" -I
"/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I
"/usr/lib/coq//plugins/decl_mode" -I "/usr/lib/coq//plugins/derive" -I
"/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I
"/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I
"/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I
"/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/quote" -I
"/usr/lib/coq//plugins/romega" -I "/usr/lib/coq//plugins/rtauto" -I
"/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/syntax" -I
"/usr/lib/coq//plugins/xml" -I /usr/lib/ocaml/camlp5 src/ssrmatching.mli
File "src/ssrmatching.mli", line 76, characters 14-34:
Error: Unbound type constructor glob_constr_and_expr
Makefile.coq:377: recipe for target 'src/ssrmatching.cmi' failed
make[3]: *** [src/ssrmatching.cmi] Error 2
make[3]: Leaving directory
'/home/lamby/temp/cdt.20160205163034.f1vmaezmGz/ssreflect-1.5'
Makefile:8: recipe for target 'all' failed
make[2]: *** [all] Error 2
make[2]: Leaving directory
'/home/lamby/temp/cdt.20160205163034.f1vmaezmGz/ssreflect-1.5'
debian/rules:40: recipe for target 'override_dh_auto_install' failed
make[1]: *** [override_dh_auto_install] Error 2
make[1]: Leaving directory
'/home/lamby/temp/cdt.20160205163034.f1vmaezmGz/ssreflect-1.5'
debian/rules:22: recipe for target 'binary' failed
make: *** [binary] Error 2
[..]
The full build log is attached.
Regards,
--
,''`.
: :' : Chris Lamb
`. `'` [email protected] / chris-lamb.co.uk
`-
ssreflect.1.5-3.unstable.amd64.log.txt.gz
Description: Binary data
