Yes, I recently “always" receive this message. I copied and Holmade "n-bit” folder in another path which I have full access to, but it did not help.
Thanks, Narges > On 13 May 2015, at 07:40, Michael Norrish <[email protected]> > wrote: > > 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
