<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!&nbsp; I am telling people not to use Adobe products
    while running Agda on Windows 8.&nbsp; Bad news for Adobe, right?&nbsp; :-)<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.&nbsp; 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.&nbsp; 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">&lt;<a moz-do-not-send="true"
              href="mailto:aaron-stump@uiowa.edu" target="_blank">aaron-stump@uiowa.edu</a>&gt;</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.
            &nbsp;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. &nbsp;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 (&gt; 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. &nbsp;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>