Source: ssreflect
Version: 1.5-3
Severity: serious
Justification: fails to build from source
User: reproducible-bui...@lists.alioth.debian.org
Usertags: ftbfs
X-Debbugs-Cc: reproducible-bui...@lists.alioth.debian.org

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
     `. `'`      la...@debian.org / chris-lamb.co.uk
       `-

Attachment: ssreflect.1.5-3.unstable.amd64.log.txt.gz
Description: Binary data

Reply via email to