[Agda] Re: panic error message on Windows

[Aaron Stump]

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 
> <mailto: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 <mailto: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/4dd4812b/attachment.html