Where is your HOL installation installed? Is it owned by a different (Unix) user?
Is it possible that when you run HOL, the system is trying to write to a directory that is not owned by you? I can imagine this being a bug, though I will have to look into how it is that loading a theory should cause a .HOLMK directory to be needed. Michael > On 8 May 2015, at 16:31, Narges Khakpour <[email protected]> wrote: > > I am using Poly/ML. This error is raised when I load some specific theories > like wordsTheory. > > Narges > >> On May 8, 2015, at 1:58 AM, Michael Norrish <[email protected]> >> wrote: >> >> Are you using Poly/ML or Moscow ML? >> >> Michael >> >>> On 7 May 2015, at 20:17, Narges kh <[email protected]> wrote: >>> >>> Hello, >>> >>> When I load a theory in HOL4, I *occasionally* receive the following error >>> message: >>> >>> "Loading wordsTheory >>> Couldn't make .HOLMK directory: Permission denied >>> Exception- Fail "Couldn't make .HOLMK directory: Permission denied” raised“ >>> >>> Does anybody has an idea why this error is raised? and how should I fix it? >>> >>> Thanks, >>> Narges >>> >>> >>> ------------------------------------------------------------------------------ >>> One dashboard for servers and applications across Physical-Virtual-Cloud >>> Widest out-of-the-box monitoring support with 50+ applications >>> Performance metrics, stats and reports that give you Actionable Insights >>> Deep dive visibility with transaction tracing using APM Insight. >>> http://ad.doubleclick.net/ddm/clk/290420510;117567292;y >>> _______________________________________________ >>> hol-info mailing list >>> [email protected] >>> https://lists.sourceforge.net/lists/listinfo/hol-info >> >> >> ________________________________ >> >> The information in this e-mail may be confidential and subject to legal >> professional privilege and/or copyright. National ICT Australia Limited >> accepts no liability for any damage caused by this email or its attachments. > ------------------------------------------------------------------------------ One dashboard for servers and applications across Physical-Virtual-Cloud Widest out-of-the-box monitoring support with 50+ applications Performance metrics, stats and reports that give you Actionable Insights Deep dive visibility with transaction tracing using APM Insight. http://ad.doubleclick.net/ddm/clk/290420510;117567292;y _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
