No release - and none with OCaml 5 support

[SnarkBoojum]

If this is your official repository, you should tag the releases here so the tarballs are generated automatically and the distributions (I'm from Debian) detect them and package them.

We (Debian) are moving to OCaml 5, so it would be good if a compatible version were available.

Thanks!

[yuzibo]

Is there any update about this? An RC bug has been reported there

[aqjune]

Hi, I could not open the log whose link appeared at the Debian Bug report. Is this link accessible to you? http://ocaml.debian.net/transitions/ocaml-5.2.0/pool/hol-light.log

[yuzibo]

Hi, I could not open the log whose link appeared at the Debian Bug report. Is this link accessible to you?

yeah, it is the same the link is not available for me also. But I just rebuild it on my local build, it was the same result with this log.

[aqjune]

The failure is addressed in the latest version of HOL Light (head commit of this repo). Is it possible to update it to use the latest commit?

[yuzibo]

sorry for late reply.

It seems the build is okay with the latest commit but now I have to need to fix the test failed from my side. Thanks.

[aqjune]

Hi! OCaml 5 seems to be supported now. Do you want to check?

[yuzibo]

hi, thanks for working on this.

hmm, but I tried this with the latest commits on Debian sid, still get:

Effective set of compiler predicates: pkg_compiler-libs,pkg_camlp-streams,autolink,byte,create_toploop
+ ocamlmktop -verbose -o ocaml -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/compiler-libs -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/camlp-streams /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/camlp-streams/camlp_streams.cma
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 "/<<PKGBUILDDIR>>/hol_lib.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?
Error in included file /<<PKGBUILDDIR>>/hol_lib.ml
Unbound value pp_print_num.
Unbound value pp_print_fpf.
Unbound value pp_print_qtype.
Unbound value pp_print_qterm.
Unbound value pp_print_thm.
Unbound value pp_print_goal.
Unbound value pp_print_goalstack.

File "/<<PKGBUILDDIR>>/help.ml", line 43, characters 18-21:
43 |   let true_path = map hol_expand_directory (!help_path) in
                       ^^^
Error: Unbound value "map"
Hint: Did you mean "max"?
Error in included file /<<PKGBUILDDIR>>/help.ml
File "help.ml" already loaded
...

Am I missing something there?

[aqjune]

It seems the Debian package is using a separate (probably old) build command. The latest version should use make to build it. Where can I find its build command?

[yuzibo]

It seems the Debian package is using a separate (probably old) build command. The latest version should use make to build it. Where can I find its build command?

Thanks, it works.

But there are two issues others for me are unclear, need to wait other maintainer's review.

Thanks.

[aqjune]

FWIW, there is a new official release now: https://github.com/jrh13/hol-light/releases/tag/Release-3.0.0 Would using this be helpful in resolving this problem?

[mpu]

Thanks a lot @aqjune for all the work you put into democratizing this lovely proof system.

[aqjune]

Hi @SnarkBoojum @yuzibo , has this issue been resolved?

[yuzibo]

Hi @aqjune Thanks for your effort, it worked on Debian, so the issue was addressed from my side, thanks again.

[jrh13]

Thank you all, I'll now consider this one closed.