[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

help to fix test failed on hol-light (#1073882 also)



Hi,

I am looking at how to fix #1073882, now the build it okay with
upstream's the latest commit from my side[0] but the test is failed.
But I have no idea how to fix it after serval hours debug.

Could anyone help to look at this in your free time?

```
make[1]: Leaving directory '/<<PKGBUILDDIR>>'
   debian/rules override_dh_auto_test
make[1]: Entering directory '/<<PKGBUILDDIR>>'
debian/test-hol-light
######################## HOL Light test Library/agm.ml ###################
OCaml version 5.2.0
Enter #help;; for help.

Findlib has been successfully loaded. Additional directives:
  #require "package";;      to load a package
  #list;;                   to list the available packages
  #camlp4o;;                to load camlp4 (standard syntax)
  #camlp4r;;                to load camlp4 (revised syntax)
  #predicates "p,q,...";;   to set these predicates
  Topfind.reset();;         to force that packages will be reloaded
  #thread;;                 to enable threads

/usr/lib/x86_64-linux-gnu/ocaml/5.2.0/compiler-libs: added to search path
/usr/lib/x86_64-linux-gnu/ocaml/5.2.0/camlp-streams: added to search path
/usr/lib/x86_64-linux-gnu/ocaml/5.2.0/camlp-streams/camlp_streams.cma: loaded
/usr/lib/x86_64-linux-gnu/ocaml/5.2.0/camlp5: added to search path
/usr/lib/x86_64-linux-gnu/ocaml/5.2.0/camlp5/odyl.cma: loaded
/usr/lib/x86_64-linux-gnu/ocaml/5.2.0/camlp5/camlp5.cma: loaded
File "hol.ml", line 1:
Error: Reference to undefined compilation unit "`Bignum'"
Hint: This means that the interface of a module is loaded, but its
implementation is not.
      Found "bignum.cmo" in the load paths. Did you mean to load it using
      "#load "bignum.cmo"" or by passing it as an argument to the toplevel?
    * HOL-Light syntax in effect *

        Camlp5 parsing version (HOL-Light) 8.03.00

# File "/<<PKGBUILDDIR>>/Library/products.ml", line 5, characters 0-14:
5 | prioritize_num();;
    ^^^^^^^^^^^^^^
Error: Unbound value "prioritize_num"
Error in included file /<<PKGBUILDDIR>>/Library/products.ml

- : unit = ()

File "/<<PKGBUILDDIR>>/Library/agm.ml", line 7, characters 0-15:
7 | prioritize_real();;
    ^^^^^^^^^^^^^^^
Error: Unbound value "prioritize_real"
Error in included file /<<PKGBUILDDIR>>/Library/agm.ml

val it : unit = ()
#
Error: Reference to undefined compilation unit "`Bignum'"
Error: Unbound value "prioritize_num"
Error in included file /<<PKGBUILDDIR>>/Library/products.ml
Error: Unbound value "prioritize_real"
Error in included file /<<PKGBUILDDIR>>/Library/agm.ml

Error in Library/agm.ml, test failed
make[1]: *** [debian/rules:50: override_dh_auto_test] Error 1
make[1]: Leaving directory '/<<PKGBUILDDIR>>'
make: *** [debian/rules:22: binary] Error 2
dpkg-buildpackage: error: debian/rules binary subprocess returned exit status 2

```

BR,
Bo

[0]: https://salsa.debian.org/vimerbf-guest/hol-light


Reply to: