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 > <2015200...@mail.buct.edu.cn> 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 > hol-info@lists.sourceforge.net > 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
