[Ur] redirect breaks channels

[Adam Chlipala]

On 12/28/2013 01:38 PM, Sergey Mironov wrote:
>> Executive summary: any properly typed function exported from a program's
>> main module is treated as accessible via GET requests.  However, RFCs say
>> that GET requests shouldn't cause side effects.  One fix is to add a .urs
>> file that only exposes the entry points you really intended.  (As a bonus,
>> this should also enable you to remove [: transaction page] annotations in
>> the .ur file!)
>>      
> Yes, the problem can be solved by adding channel2.urs containing
> 'main' signature only.

I think the error reporting was overeager in that case; I've pushed a 
changeset quieting it down.  Your original program compiles for me now.

However, you should be aware that this wasn't just a case of 
overconservative program analysis by Ur/Web.  Your program really does 
violate HTTP standards.  Redirects and links make GET requests, and GET 
requests aren't supposed to have side effects, whereas the functions you 
got complaints about do cause persistent side effects.  I only intended 
for 'safeGet' to be used in cases where there are especially compelling 
reasons to "break the rules"!

In your case, for instance, it would be easy to call [put] via a form or 
RPC, which use POST requests and so are allowed to cause persistent side 
effects.

> Unfortunately, I have at least one more test
> which I can't compile anymore because of similar errors. This
> application is rather complex so I don't plan to post it here, but it
> contains a single 'main' function without forms and redirects, only
> with  back-links to itself (via<a link={main {}}>back</a>).   That is
> why I think that urweb become too suspicious.

Let me know if my change doesn't fix that problem.  I'm not sure why any 
prior, recent Ur/Web changes would affect such things, though.

> In the end, it is strange to see
> error messages mentioning forms because channel2.ur contains no forms!
>    

Despite the fact that it wasn't actually called for in your code, that 
error message happened to be missing a third case, RPC handlers.  I 
added that possibility to the text, which should be helpful to further 
confuse people who come upon the message in the future. ;)  (Actually, 
when it only fires in appropriate cases, I hope it will always be clear 
what the problem is.)