Hi Adnan, | I am having a weird message persistently while loading the multivariate | realanalysis theory in HOL-Light. | | *Segmentation fault (core dumped)* | This message appear after loading some of the theorems. I guess that this | error may be due to my recent update of HOL-Light sources from the github | repositories. Is there any way around?
This sounds like the sort of error that "shouldn't happen" in normal OCaml code like HOL Light. Loading all the Multivariate theories, the image gets pretty big, and so conceivably on a machine without much memory you could hit this because OCaml runs out of resources. However, the image size is nothing out of the ordinary compared with everyday applications like Web browsers, and anyway I normally see a cleaner "out of memory" type message in such a context. The only place where HOL Light does any hacky system-level stuff is in the maintainence of the theorem database. I would recommend using the toplevel "update_database.ml" file rather than the one in "Examples/update_database.ml" (in fact I should probably just remove the latter as it is now obselete). | I have another query. Can anybody know the way to reduce the loading time | of HOL-Light theories? If you are using some version of Linux there are checkpointing options, as explained in the README file. Personally I tend to just have a few HOL Light sessions open. I agree this is somewhat inconvenient though. John. ------------------------------------------------------------------------------ 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
