<div dir="ltr">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.<div>
<br></div><div>I don't know enough about windows to know what the best way would be, a .bat should work though.</div><div><br></div><div>[1]<a href="http://www.haskell.org/ghc/docs/latest/html/libraries/directory-1.2.0.1/System-Directory.html#v:getTemporaryDirectory">http://www.haskell.org/ghc/docs/latest/html/libraries/directory-1.2.0.1/System-Directory.html#v:getTemporaryDirectory</a></div>
<div><br></div><div>Cheers,</div><div>Andrea</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Feb 20, 2014 at 5:55 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">
<div bgcolor="#FFFFFF" text="#000000">
Hi, Andrea.<div class=""><br>
<br>
<div>On 02/20/2014 10:12 AM, Andrea Vezzosi
wrote:<br>
</div>
<blockquote type="cite">
<div dir="ltr">Hi,
<div><br>
</div>
<div>That's quite unfortunate, do you still need a workaround?</div>
</div>
</blockquote>
<br></div>
Thanks for asking! I am telling people not to use Adobe products
while running Agda on Windows 8. Bad news for Adobe, right? :-)<div class=""><br>
<br>
<blockquote 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></div>
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.<span class="HOEnZb"><font color="#888888"><br>
<br>
Aaron</font></span><div><div class="h5"><br>
<br>
<blockquote 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 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/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>
<div><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 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/mailman/listinfo/agda</a><br>
</div>
</div>
</blockquote>
</div>
<br>
</div>
</blockquote>
<br>
</div></div></div>
</blockquote></div><br></div>