[Ur] redirect breaks channels

[Adam Chlipala]

On 12/24/2013 07:24 PM, Sergey Mironov wrote:
> OK, I've looked under the hood and now I see that my application is
> invalid because we can't call recv() on channels obtained from
> anywhere but the channel call.

Right.  Channels are page-view-specific, even though the type system 
isn't enforcing such use statically.

I'm of two minds about your suggestion to introduce separate abstract 
types for writable and readable channels, where only the former is 
allowed in the database.  There's the clear "pro" of ruling out confused 
uses of channels, but there's the "con" of not allowing a pattern that's 
already used in one of the demos: what if we want to promote modularity 
by allowing code that checks if a channel has already been created for 
the current client?  If so, we can just return it out of the database, 
but such a handle becomes unreadable, with your typing change.

For now, I've just added another sentence to the manual, which should 
hopefully help guide new users sooner to the understanding that you have 
now.  We could still discuss potential code changes further.

> Unfortunately, rewriting my program didn't help me to deal with errors
> [1] . I see them in correctly written programs as well. Is it the
> concurrency problem you mentioned in the manual? Could you please
> explain in a bit more details why do we need to start a transaction
> within a transaction here?
>
> [1] Begin error: cannot start a transaction within a
> transaction<br/>Expunge blocked by error: Error running SQL BEGIN
>    

Higher-order bits: I think this indicates an Ur/Web bug; it should not 
be possible to write Ur/Web code that does anything explicit with 
transactions.  It's possible that something about the non-atomic 
transactions of SQLite (which I warn about in the manual) is responsible 
somehow, but it doesn't seem likely to me.

I haven't been able to reproduce this issue.  Everything seems to work 
fine with your code with both SQLite and Postgres, after I change the 
redirect to return the proper page content inline instead.  Could you 
explain what changes you've made to the code you sent before and how you 
reproduce the error?

I think I spotted some points in the Ur/Web implementation that could 
lead to behavior like this under some circumstances, and I've pushed a 
changeset to adjust them.

P.S.: In general, your life using Ur/Web will be easiest if you stick to 
Postgres as the database.  The Ur/Web manual should contain literally a 
complete description of everything you need to know to set up Ur/Web and 
Postgres together, even if you have no prior knowledge of Postgres.