<div dir="ltr">Hi,<div><br></div><div>That's quite unfortunate, do you still need a workaround?</div><div><br></div><div>I guess one option would be to use a directory next to the file agda is working on, rather than the temp directory.</div>
<div><br></div><div><br></div><div>Best,</div><div>Andrea</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Feb 20, 2014 at 4:59 PM, Aaron Stump <span dir="ltr"><<a href="mailto:aaron-stump@uiowa.edu" target="_blank">aaron-stump@uiowa.edu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi, Agda community.<br>
<br>
Just a follow-up on my email of a couple weeks back, about a mysterious "Panic" error message from Agda (see below).<br>
<br>
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:<br>
<br>
<a href="http://www.eightforums.com/user-accounts-family-safety/27720-set-permissions-user-appdata-local-temp-folder.html" target="_blank">http://www.eightforums.com/<u></u>user-accounts-family-safety/<u></u>27720-set-permissions-user-<u></u>appdata-local-temp-folder.html</a><br>
<br>
Agda does not like this, of course, since it needs to write to the temp directory.<br>
<br>
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.<br>
<br>
Best wishes,<br>
Aaron<div class="HOEnZb"><div class="h5"><br>
<br>
On 02/07/2014 03:14 PM, Aaron Stump wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi, Agda community.<br>
<br>
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:<br>
<br>
Panic: invalid range when printing error:<br>
C:\Users\TheStudent\AppData\<u></u>Local\Temp\: openTempFile: permission denied<br>
(Permission denied)<br>
<br>
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.<br>
<br>
Any ideas how to work around this problem?<br>
<br>
Thanks,<br>
Aaron<br>
</blockquote>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>