[Agda] Re: panic error message on Windows

[Andrea Vezzosi]

Agda uses getTemporaryDirectory[1] to find the temp dir, which looks into
environment variables, so you could have some form of wrapper which sets
the variable to somewhere else just for the agda process.

I don't know enough about windows to know what the best way would be, a
.bat should work though.

[1]
http://www.haskell.org/ghc/docs/latest/html/libraries/directory-1.2.0.1/System-Directory.html#v:getTemporaryDirectory

Cheers,
Andrea


On Thu, Feb 20, 2014 at 5:55 PM, Aaron Stump <aaron-stump at uiowa.edu> wrote:

>  Hi, Andrea.
>
>
> On 02/20/2014 10:12 AM, Andrea Vezzosi wrote:
>
> Hi,
>
>  That's quite unfortunate, do you still need a workaround?
>
>
> Thanks for asking!  I am telling people not to use Adobe products while
> running Agda on Windows 8.  Bad news for Adobe, right?  :-)
>
>
>
>  I guess one option would be to use a directory next to the file agda is
> working on, rather than the temp directory.
>
>
> Yes, if Agda had a command-line flag to set the temporary directory, or
> something like this, that would help with this problem.  But Agda is just
> calling a Haskell library function for opening the temp file, I think, so
> that would require a little more of a change to the Agda code, to set the
> temporary directory.  I would imagine it should not be hard, though.
>
> Aaron
>
>
>
>
>  Best,
> Andrea
>
>
> On Thu, Feb 20, 2014 at 4:59 PM, Aaron Stump <aaron-stump at uiowa.edu>wrote:
>
>> Hi, Agda community.
>>
>> Just a follow-up on my email of a couple weeks back, about a mysterious
>> "Panic" error message from Agda (see below).
>>
>> It seems that on Windows 8, some other programs, like apparently Adobe
>> Acrobat, have a bad habit of changing the permissions of the Windows temp
>> directory to be read-only.  See this forum discussion, for example:
>>
>>
>> http://www.eightforums.com/user-accounts-family-safety/27720-set-permissions-user-appdata-local-temp-folder.html
>>
>> Agda does not like this, of course, since it needs to write to the temp
>> directory.
>>
>> This is not a bug in Agda, but rather bad behavior from other programs in
>> the Windows 8 ecosystem.  Just for others who may run into this.
>>
>> Best wishes,
>> Aaron
>>
>>
>> On 02/07/2014 03:14 PM, Aaron Stump wrote:
>>
>>> Hi, Agda community.
>>>
>>> For my big (> 90 students) undergrad this semester which is using Agda
>>> 2.3.2, we are occasionally getting disturbing reports from Windows users of
>>> receiving the following error message from Agda under emacs:
>>>
>>> Panic: invalid range when printing error:
>>> C:\Users\TheStudent\AppData\Local\Temp\: openTempFile: permission denied
>>> (Permission denied)
>>>
>>> This is a nasty one, as we don't know even a workaround.  I do find some
>>> discussion on ghc list archives about openTempFile having a problem if the
>>> file is actually a directory, or something like this -- but the issue was
>>> supposedly fixed long ago in ghc.
>>>
>>> Any ideas how to work around this problem?
>>>
>>> Thanks,
>>> Aaron
>>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140220/2a477dcc/attachment-0001.html