Add update_database for OCaml 5, fix a bug in search, add make switch-5 #115
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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.
|
Thank you, this now makes everything work in OCaml 5! I've tested it on OCaml 5.1.0 under Mac OS. |
|
I think we can use OPAM's compatible version management in the future. :) It will conceptually have a matrix of usable OCaml & camlp5 versions. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This patch
After this patch, I think HOL Light is ready to support OCaml 5, resolving github issue #95 and partially resolving #101. I tested holtest and s2n-bignum arm proofs 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.