Comments (6)
maggesi
commented on September 7, 2024
Hi, I have some instructions for running HOL Light in a Docker container:
https://github.com/maggesi/hol-light-docker
You may want to start with the usage guide:
https://github.com/maggesi/hol-light-docker/blob/master/USAGE.md
Actually, I now use a slightly different method that accommodates for working on a HOL repository on the host system (instead of using a cloned repository on the container). I will eventually update these script before long.
Do not hesitate to give feedback if you try to use it.
from hol-light.
binghe
commented on September 7, 2024
Some possible steps: (confirmed on Mac OS X 10.11)
- Install Macports from https://www.macports.org
- Install OCaml and related packages:
sudo port install ocaml ocaml-num camlp5 - Clone HOL-Light Git into your local directory.
- Go to HOL-Light directory and execute
make - Start OCaml by
ocaml(orocaml -safe-string) - Load HOL-Light by
#use "hol.ml";;(#is part of the command) - Load a theory, e.g.
needs "Multivariate/transcendentals.ml";;(it takes a long time)
from hol-light.
brando90
commented on September 7, 2024
@binghe hmmm seems I get an error:
(base) brandomiranda~ $ cd hol-light/
(base) brandomiranda~/hol-light $ make
cp update_database_`ocamlc -version | cut -c1`.ml update_database.ml
\
if test `ocamlc -version | cut -c1-3` = "3.0" ; \
then cp pa_j_`ocamlc -version | cut -c1-4`.ml pa_j.ml ; \
else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -c1` = "7" ; \
then if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "7.01" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "7.02" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "7.03" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "7.04" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "7.05" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "7.06" ; \
then cp pa_j_4.xx_7.06.ml pa_j.ml; \
else cp pa_j_4.xx_7.xx.ml pa_j.ml; \
fi \
else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.02.1" ; \
then cp pa_j_3.1x_6.02.1.ml pa_j.ml; \
else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.02.2" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.02.3" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.03" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.04" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.05" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.06" ; \
then cp pa_j_3.1x_6.02.2.ml pa_j.ml; \
else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.06" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.07" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.08" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.09" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.10" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.11" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.12" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.13" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.14" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.15" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.16" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` = "6.17" ; \
then cp pa_j_3.1x_6.11.ml pa_j.ml; \
else cp pa_j_3.1x_`camlp5 -v 2>&1 | cut -f3 -d' ' | cut -c1`.xx.ml pa_j.ml; \
fi \
fi \
fi \
fi \
fi
if test `ocamlc -version | cut -c1-3` = "3.0" ; \
then ocamlc -c -pp "camlp4r pa_extend.cmo q_MLast.cmo" -I `camlp4 -where` pa_j.ml ; \
else if test `ocamlc -version | cut -c1-3` = "3.1" -o `ocamlc -version | cut -c1-4` = "4.00" -o `ocamlc -version | cut -c1-4` = "4.01" -o `ocamlc -version | cut -c1-4` = "4.02" -o `ocamlc -version | cut -c1-4` = "4.03" -o `ocamlc -version | cut -c1-4` = "4.04" -o `ocamlc -version | cut -c1-4` = "4.05" ; \
then ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I `camlp5 -where` pa_j.ml ; \
else ocamlc -safe-string -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I `camlp5 -where` pa_j.ml ; \
fi \
fi
File "pa_j.ml", line 806, characters 23-39:
Warning 3: deprecated: String.uppercase
Use String.uppercase_ascii instead.
File "pa_j.ml", line 807, characters 28-44:
Warning 3: deprecated: String.lowercase
Use String.lowercase_ascii instead.
(base) brandomiranda~/hol-light $ ocaml
(base) brandomiranda~/hol-light $ ocaml
OCaml version 4.06.0
# use "hol.ml";;
Error: Unbound value use
from hol-light.
binghe
commented on September 7, 2024
Noticed that # is part of the command. Thus you should see the following text on your screen:
# #use "hol.ml";;
Don't ask why, I also hate OCaml. (I'm Standard ML and HOL4 user.)
from hol-light.
brando90
commented on September 7, 2024
Hmmm i did put that at some point...will paste that attempt later.
Im stuck with ocaml
…Sent from my iPhone
On Aug 28, 2019, at 7:04 PM, Chun Tian ***@***.***> wrote:
Noticed that # is part of the command. Thus you should see the following in your screen:
# #use "hol.ml";;
Don't ask why, I also hate OCaml. (I'm Standard ML and HOL4 user.)
—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub, or mute the thread.
from hol-light.
aqjune-aws
commented on September 7, 2024
HOL Light now has make switch which will create a local OPAM switch and install dependency packages in there, as well as hol.sh which encapsulates all details about how to run:
make switch
eval $(opam env)
make
./hol.sh
from hol-light.
Related Issues (20)
- how to get start after these commands are done HOT 6
- No release - and none with OCaml 5 support HOT 5
- Compatibility with camlp5-7.07? HOT 1
- Forum for HOL Light questions, collaborations etc HOT 5
- Failure with camlp5 7.11 (+ Debian patch) HOT 2
- "Comms::Receive failed" when inference the whole val dataset to generate proof_log
- Illegal begin of top_parse HOT 1
- unable to install hol-light on mac or centos 7.4
- unnecessary hyp in TAN_ADD HOT 1
- make error HOT 5
- [INFO] HOL Light Native HOT 1
- HOL light installation problem on macos HOT 6
- opam installation HOT 2
- `instantiate` can produce terms that are not parsable HOT 1
- HOL Terminal Basic Issues, Syntax and Related Commands HOT 4
- HOL-Light with recent versions of ocaml & camlp5 ? HOT 5
- How to use Map.Make after "hol.ml"? HOT 2
- Logic/canon.ml fails HOT 1
- Updating update_database.ml for OCaml 5 HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from hol-light.