Can you reliably reproduce the bug? (Your message says it happens occasionally, so I’m not optimistic.)
Michael > On 8 May 2015, at 17:25, Narges Khakpour <[email protected]> wrote: > > I am the only user and the owner of HOL installation. I also have read/write > access to the theory files. Initially I thought maybe I do not have the right > access to the directory and reinstalled it in another drive, but it did not > work. None of the installations is in the home directory (I’m a Mac user). > > Thanks, > Narges > >> On May 8, 2015, at 8:51 AM, Michael Norrish <[email protected]> >> wrote: >> >> 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
