<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
Hi, Andrea.<br>
<br>
<div class="moz-cite-prefix">On 02/20/2014 10:12 AM, Andrea Vezzosi
wrote:<br>
</div>
<blockquote
cite="mid:CAOSJkmwHX=Ua-5AzpjfzdZDoe5PBq_8oMZRA3nHuavwC5MdFaQ@mail.gmail.com"
type="cite">
<div dir="ltr">Hi,
<div><br>
</div>
<div>That's quite unfortunate, do you still need a workaround?</div>
</div>
</blockquote>
<br>
Thanks for asking! I am telling people not to use Adobe products
while running Agda on Windows 8. Bad news for Adobe, right? :-)<br>
<br>
<blockquote
cite="mid:CAOSJkmwHX=Ua-5AzpjfzdZDoe5PBq_8oMZRA3nHuavwC5MdFaQ@mail.gmail.com"
type="cite">
<div dir="ltr">
<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>
</blockquote>
<br>
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.<br>
<br>
Aaron<br>
<br>
<blockquote
cite="mid:CAOSJkmwHX=Ua-5AzpjfzdZDoe5PBq_8oMZRA3nHuavwC5MdFaQ@mail.gmail.com"
type="cite">
<div dir="ltr">
<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 moz-do-not-send="true"
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 moz-do-not-send="true"
href="http://www.eightforums.com/user-accounts-family-safety/27720-set-permissions-user-appdata-local-temp-folder.html"
target="_blank">http://www.eightforums.com/user-accounts-family-safety/27720-set-permissions-user-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\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>
_______________________________________________<br>
Agda mailing list<br>
<a moz-do-not-send="true"
href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a moz-do-not-send="true"
href="https://lists.chalmers.se/mailman/listinfo/agda"
target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div>
</div>
</blockquote>
</div>
<br>
</div>
</blockquote>
<br>
</body>
</html>