[Reproducible-builds] Bug#813820: ssreflect: FTBFS: Error: Unbound type constructor glob_constr_and_expr

[Chris Lamb]

Source: ssreflect
Version: 1.5-3
Severity: serious
Justification: fails to build from source
User: reproducible-builds at lists.alioth.debian.org
Usertags: ftbfs
X-Debbugs-Cc: reproducible-builds at 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
     `. `'`      lamby at debian.org / chris-lamb.co.uk
       `-
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ssreflect.1.5-3.unstable.amd64.log.txt.gz
Type: application/octet-stream
Size: 1381 bytes
Desc: not available
URL: <http://lists.alioth.debian.org/pipermail/reproducible-builds/attachments/20160205/c348097e/attachment.obj>