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

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.


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

Reply via email to