Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

No release - and none with OCaml 5 support #101

Open
SnarkBoojum opened this issue Jun 20, 2024 · 11 comments
Open

No release - and none with OCaml 5 support #101

SnarkBoojum opened this issue Jun 20, 2024 · 11 comments

Comments

@SnarkBoojum
Copy link

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
Copy link

yuzibo commented Aug 9, 2024

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

@aqjune
Copy link
Contributor

aqjune commented Aug 9, 2024

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
Copy link

yuzibo commented Aug 10, 2024

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
Copy link
Contributor

aqjune commented Aug 10, 2024

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
Copy link

yuzibo commented Aug 14, 2024

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 added a commit to aqjune-aws/hol-light that referenced this issue Oct 11, 2024
@aqjune
Add update_database for OCaml 5, fix a bug in search, add make switch-5
590b570 
This patch
- Adds update_database for OCaml5, which is almost a copy of the file for OCaml 4.14
- Fixes a failure when there are theorems inside a module (OCaml 4.14). My test code:
```
loads "update_database.ml";;
unset_jrh_lexer;;
module A_SIMPLE_MODULE = struct let mythm = new_axiom `1 + 1 = 2` end;;
set_jrh_lexer;;
search [name "A_SIMPLE_MODULE"];;
search [name "ADD_SUB"];;
```
- Moves update_database_*.ml files into a separate directory
- Fixes usage of a deprecated function in Mizarlight.
- Add switch-5 which is a command for setting OPAM switch with OCaml 5.2 (the latest version).

After this patch, I think HOL Light is ready to support OCaml 5, resolving github issue jrh13#95 and partially resolving jrh13#101.
I tested holtest on OCaml 5.2 and it worked fine.
About the new command 'switch-5': I would like to suggest having switch-X for each major version X.
aqjune pushed a commit to aqjune-aws/hol-light that referenced this issue Oct 11, 2024
@aqjune-aws
Add update_database for OCaml 5, fix a bug in search, add make switch-5
cb1bd18 
This patch
- Adds update_database for OCaml5, which is almost a copy of the file for OCaml 4.14
- Fixes a failure when there are theorems inside a module (OCaml 4.14). My test code:
```
loads "update_database.ml";;
unset_jrh_lexer;;
module A_SIMPLE_MODULE = struct let mythm = new_axiom `1 + 1 = 2` end;;
set_jrh_lexer;;
search [name "A_SIMPLE_MODULE"];;
search [name "ADD_SUB"];;
```
- Moves update_database_*.ml files into a separate directory
- Fixes usage of a deprecated function in Mizarlight.
- Add switch-5 which is a command for setting OPAM switch with OCaml 5.2 (the latest version).

After this patch, I think HOL Light is ready to support OCaml 5, resolving github issue jrh13#95 and partially resolving jrh13#101.
I tested holtest on OCaml 5.2 and it worked fine.
About the new command 'switch-5': I would like to suggest having switch-X for each major version X.
@aqjune-aws aqjune-aws mentioned this issue Oct 11, 2024
Merged
@aqjune
Copy link
Contributor

aqjune commented Oct 12, 2024

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

@yuzibo
Copy link

yuzibo commented Oct 14, 2024

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
Copy link
Contributor

aqjune commented Oct 14, 2024

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
Copy link

yuzibo commented Oct 15, 2024

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
Copy link
Contributor

aqjune commented Oct 15, 2024

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
Copy link
Contributor

mpu commented Oct 15, 2024

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@mpu @SnarkBoojum @aqjune @yuzibo