I forgot one thing: In modern Linux systems, to support installing 32-bit and 64-bit runtimes together, many package’s library files have been moved from “/usr/lib” to “/usr/lib/x86_64-linux-gnu”. But HOL’s building scripts do not recognize “/usr/lib/x86_64-linux-gnu” when searching for “libpolymain.a”.
To correctly use system “polyml” for building HOL4, a symbolic link from “/usr/lib/x86_64-linux-gnu/libpolymain.a” to “/usr/lib/libpolymain.a” must be made manually. One way is to stand in “/usr/lib” with root access, and execute the following command: ln -s x86_64-linux-gnu/libpolymain.a . Regards, Chun > Il giorno 01 mag 2017, alle ore 15:15, Chun Tian (binghe) > <[email protected]> ha scritto: > > Hi Liu, > > I hope my experiences could help a little: > > 1. In Ubuntu 16.04, there’s no need to build PolyML from source, you can use > one of the following commands to install system package “polyml” (currently > the version if 5.6, enough to build HOL): > > $ sudo apt-get install polyml > $ sudo aptitude install polyml > > 1a. You should also install OCaml (Ubuntu package name: “ocaml”), because the > building of “holyhammer” component needs it. > > 2. The “dot” command is provided by system package “graphviz”, you can > install it easily by “apt-get” or “aptitude” commands too. It’s not > necessary, but the Theory graph generated by dot is very useful for > references. > 3. Once you have a freshly checked out HOL from Git master [1], and suppose > you’re in the HOL root directory, then the following commands will finish the > builds in about 10 minutes: > >> poly < tools/smart-configure.sml >> bin/build -j 4 —stdknl > > (there’s really no surprise that above commands fail, unless you have > uninstalled GCC or some other > > 4. To access HOL4 easier, you can either put "/home/liu/hol/bin” into PATH > environment variable, or make symbolic links of "/home/liu/hol/bin/hol” and > "/home/liu/hol/bin/Holmake” into somewhere already part of PATH (e.g. > "/home/liu/bin”) > > 5. To use HOL4 for theory creations. I suggest the toolchain of Emacs + > sml-mode.el . For details, see "an 8-page guide to HOL interaction and basic > proof using Emacs” [2] > > Regards, > > Chun Tian > > [1] git clone https://github.com/HOL-Theorem-Prover/HOL.git > [2] https://hol-theorem-prover.org/HOL-interaction.pdf > >> Il giorno 01 mag 2017, alle ore 10:42, Liu Gengyang >> <[email protected]> ha scritto: >> >> Hi, >> >> I am installing the latest HOL 4 in ubuntu 16.04. I have followed the steps >> given in the tutorial to complete the installation. When I input bin/hol for >> entering the HOL system, I failed, and the system prompted: >> >> Error trying to use the file:'/home/liu/hol/bin/hol.ML' >> >> if I input:/home/liu/hol/bin/hol.ML, the system prompted no such file or >> dir. However, I have this file and dir. >> >> I have installed poly/ml-5.6 successfully, I can enter it. Now I don't know >> how to enter HOL. Could you help me? >> >> In addition, After the step of bin/build, the system prompted: >> >> Writing HOLPage >> >> *** Can't see dot executable at /usr/bin/dot; not generating theory-graph >> *** You can try reconfiguring and providing an explicit path >> *** (val DOT_PATH = "....") in >> *** tools-poly/poly-includes.ML (Poly/ML) >> *** or >> *** config-override (Moscow ML) >> *** >> *** (Under Poly/ML you will have to delete bin/hol.state0 as well) >> *** >> *** (Or: build with -nograph to stop this message from appearing again) >> >> I do not know whether this is the reason for. >> >> Thanks, >> >> Liu >> >> ------------------------------------------------------------------------------ >> Check out the vibrant tech community on one of the world's most >> engaging tech sites, Slashdot.org! >> http://sdm.link/slashdot_______________________________________________ >> hol-info mailing list >> [email protected] >> https://lists.sourceforge.net/lists/listinfo/hol-info >
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
