Add make switch fore easy installation of dependencies
#98
Conversation
| thanks to Hendrik Tews, so installation of HOL Light and all its | ||
| prerequisites is as simple as | ||
|
|
||
| sudo apt-get install hol-light |
There was a problem hiding this comment.
I found that the apt package of hol-light is not working anymore; should we remove this (as edited in this patch)?
There was a problem hiding this comment.
Yes, I agree that we should probably delete this, unless someone volunteers to take over maintenance of the apt package. Direct HOL Light installation (thanks to this patch, among others) is now so much easier anyway.
|
I have tried this out on several machines and it mostly worked perfectly, thanks! One small suggestion: I still had trouble on an ARM-based Mac OS, apparently around the use of |
|
OK, I figured out the m4 problem, which was just the fact that the homebrew version of m4 wasn't in my PATH. So it all worked fine on the ARM-based machine too. So the only suggestion would be the "ocaml-base-compiler" change if you agree. |
This patch adds `make switch` that - Creates a local OPAM switch under the current hol-light directory - Chooses the latest OCaml version (4.14 for now; would be great if it is 5.0 in the future!) - And installs dependencies that are needed by HOL Light. This is to help beginners set the environment for HOL Light. I also updated README to explain(recommend) this option. A separate 'DEPENDENCIES' chapter is added to explain the original, detailed steps.
The two seemed identical to me because |
|
Great, thank you I've already found it useful on an old machine where my system OCaml was in a weird state. I'll merge this in now. |
| switch:; \ | ||
| opam switch create . ocaml-base-compiler.4.14.0 ; \ | ||
| eval $(opam env) ; \ | ||
| opam install -y zarith camlp5 ledit |
There was a problem hiding this comment.
The camlp5 version should be explicitly given: camlp5.8.02.01. The current version of camlp5 (8.03) is not compatible with pa_j_4.xx_8.02.ml.
|
A problem is that in some machine 8.02 is not available. Does pinning it to
8.00.(some minor version) work?
…On Sat, May 25, 2024 at 9:04 PM Alexey Solovyev ***@***.***> wrote:
***@***.**** commented on this pull request.
------------------------------
In Makefile
<#98 (comment)>:
> @@ -37,6 +37,15 @@ CAMLP5_VERSION=`camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-'
default: update_database.ml pa_j.cmo hol.sh;
+# Create a local OPAM switch and install dependencies on it.
+# This will use the latest OCaml version that fully supports features of
+# HOL Light.
+# ledit is installed for line editing of OCaml REPL
+switch:; \
+ opam switch create . ocaml-base-compiler.4.14.0 ; \
+ eval $(opam env) ; \
+ opam install -y zarith camlp5 ledit
The camlp5 version should be explicitly given: camlp5.8.02.01. The
current version of camlp5 (8.03) is not compatible with pa_j_4.xx_8.02.ml.
—
Reply to this email directly, view it on GitHub
<#98 (review)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ABRPHGKHMTU2RSHRG7CCF6TZEE7JZAVCNFSM6AAAAABGRBKTAGVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZDANZZGMZTKOBQGQ>
.
You are receiving this because you authored the thread.Message ID:
***@***.***>
|
|
I tested Camlp5 8.00.03 and it works with OCaml 4.14. |
…SUMS_TAC` help To fix the failure mentioned in jrh13#98 , This updates `make switch` to pin the camlp5 version to 8.02.01. I previously mentioned that this version was not available on some machine in the thread, but it seems it was available unless the opam version itself was problematic. Furthermore, to check that `make switch` is working okay, the CI check of HOL Light is updated to use `make switch` to set up the environment. Another small orthogonal update is fixing typos in the help doc of `NAME_ASSUMS_TAC`.
…SUMS_TAC` help To fix the failure mentioned in jrh13#98 , This updates `make switch` to pin the camlp5 version to 8.02.01. I previously mentioned that this version was not available on some machine in the thread, but it seems it was available unless the opam version itself was problematic. Furthermore, to check that `make switch` is working okay, the CI check of HOL Light is updated to use `make switch` to set up the environment. Another small orthogonal update is fixing typos in the help doc of `NAME_ASSUMS_TAC`.
…SUMS_TAC` help To fix the failure mentioned in jrh13#98 , This updates `make switch` to pin the camlp5 version to 8.02.01. I previously mentioned that this version was not available on some machine in the thread, but it seems it was available unless the opam version itself was problematic. Furthermore, to check that `make switch` is working okay, the CI check of HOL Light is updated to use `make switch` to set up the environment. Another small orthogonal update is fixing typos in the help doc of `NAME_ASSUMS_TAC`.
This patch adds
make switchthatThis is to help beginners set the environment for HOL Light.
I also updated README to explain(recommend) this option. A separate 'DEPENDENCIES' chapter is added to explain the original, detailed steps.