Re: [Ur] Mandatory nginx conf: merge_slashes off

2019-04-15 Thread Adam Chlipala
Done 
 
now!  Thanks for the suggestion.


On 1/26/19 2:00 PM, Simon Van Casteren wrote:
If it's not much work, I'd say yes. What I mentioned won't happen 
often, but it was an extremely annoying thing to track down.


Simon

Op za 26 jan. 2019 om 19:33 schreef Adam Chlipala >:


Reviewing a PR just now, I'm reminded that the logic I
half-recalled to avoid empty serializations is only for strings. 
Would it be worth changing [unit] serialization to avoid empty
serializations there, too?

On 1/25/19 8:21 AM, Simon Van Casteren wrote:

It doesn't happen often of course, since you rarely use unit in a
page or RPC function. How I ran into it was actually via the now
fixed bug
https://github.com/urweb/urweb/issues/117, I made some ADT's that
got around that bug by declaring all constructors to have at
least one parameter, unit if nothing else. That came back to bite
me now...

A page with this signature:

val page: unit -> string -> transaction page

Would be affected by the issue I described. This obviously won't
happen much outside of you making a mistake (for example because
first the function took just a unit, then you added the string
parameter), but because it doesn't happen often and it's actually
nginx making the "mistake", I still thought it could help someone
out in the future!

Simon

On Fri, 25 Jan 2019 at 13:57, Adam Chlipala mailto:ad...@csail.mit.edu>> wrote:

Thanks for sharing that wisdom!  Somehow I remember making a
special effort to encode empty strings with underscores,
precisely to avoid this problem (though it was appearing in
Apache, if I recall correctly).  Can you point us to an
example where it arises, in a URL that an Ur/Web app
generates itself?

On 1/25/19 5:13 AM, Simon Van Casteren wrote:

Hi,

I just ran into an awful problem combining urweb with nginx.
By default, nginx by default merges double slashes in urls,
eg: http://www.bla.com//users becomes
http//www.bla.com/users . This can
be a problem for UrWeb applications since a double slash is
actually how urweb encodes the unit or () value.

The solution is to use the option: "merge_slashes off".

It's not a bug in either application so I didnt want me make
an issue for it, but this could be useful info for other
people running Ur/Web programs behind nginx...

Simon



___
Ur mailing list
Ur@impredicative.com 
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur


Re: [Ur] Mandatory nginx conf: merge_slashes off

2019-01-26 Thread Simon Van Casteren
If it's not much work, I'd say yes. What I mentioned won't happen often,
but it was an extremely annoying thing to track down.

Simon

Op za 26 jan. 2019 om 19:33 schreef Adam Chlipala :

> Reviewing a PR just now, I'm reminded that the logic I half-recalled to
> avoid empty serializations is only for strings.  Would it be worth changing
> [unit] serialization to avoid empty serializations there, too?
>
> On 1/25/19 8:21 AM, Simon Van Casteren wrote:
>
> It doesn't happen often of course, since you rarely use unit in a page or
> RPC function. How I ran into it was actually via the now fixed bug
> https://github.com/urweb/urweb/issues/117, I made some ADT's that got
> around that bug by declaring all constructors to have at least one
> parameter, unit if nothing else. That came back to bite me now...
>
> A page with this signature:
>
> val page: unit -> string -> transaction page
>
> Would be affected by the issue I described. This obviously won't happen
> much outside of you making a mistake (for example because first the
> function took just a unit, then you added the string parameter), but
> because it doesn't happen often and it's actually nginx making the
> "mistake", I still thought it could help someone out in the future!
>
> Simon
>
> On Fri, 25 Jan 2019 at 13:57, Adam Chlipala  wrote:
>
>> Thanks for sharing that wisdom!  Somehow I remember making a special
>> effort to encode empty strings with underscores, precisely to avoid this
>> problem (though it was appearing in Apache, if I recall correctly).  Can
>> you point us to an example where it arises, in a URL that an Ur/Web app
>> generates itself?
>>
>> On 1/25/19 5:13 AM, Simon Van Casteren wrote:
>>
>> Hi,
>>
>> I just ran into an awful problem combining urweb with nginx. By default,
>> nginx by default merges double slashes in urls, eg:
>> http://www.bla.com//users becomes http//www.bla.com/users. This can be a
>> problem for UrWeb applications since a double slash is actually how urweb
>> encodes the unit or () value.
>>
>> The solution is to use the option: "merge_slashes off".
>>
>> It's not a bug in either application so I didnt want me make an issue for
>> it, but this could be useful info for other people running Ur/Web programs
>> behind nginx...
>>
>> Simon
>>
>> ___
> Ur mailing list
> Ur@impredicative.com
> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
>
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur


Re: [Ur] Mandatory nginx conf: merge_slashes off

2019-01-26 Thread Adam Chlipala
Reviewing a PR just now, I'm reminded that the logic I half-recalled to 
avoid empty serializations is only for strings.  Would it be worth 
changing [unit] serialization to avoid empty serializations there, too?


On 1/25/19 8:21 AM, Simon Van Casteren wrote:
It doesn't happen often of course, since you rarely use unit in a page 
or RPC function. How I ran into it was actually via the now fixed bug
https://github.com/urweb/urweb/issues/117, I made some ADT's that got 
around that bug by declaring all constructors to have at least one 
parameter, unit if nothing else. That came back to bite me now...


A page with this signature:

val page: unit -> string -> transaction page

Would be affected by the issue I described. This obviously won't 
happen much outside of you making a mistake (for example because first 
the function took just a unit, then you added the string parameter), 
but because it doesn't happen often and it's actually nginx making the 
"mistake", I still thought it could help someone out in the future!


Simon

On Fri, 25 Jan 2019 at 13:57, Adam Chlipala > wrote:


Thanks for sharing that wisdom!  Somehow I remember making a
special effort to encode empty strings with underscores, precisely
to avoid this problem (though it was appearing in Apache, if I
recall correctly).  Can you point us to an example where it
arises, in a URL that an Ur/Web app generates itself?

On 1/25/19 5:13 AM, Simon Van Casteren wrote:

Hi,

I just ran into an awful problem combining urweb with nginx. By
default, nginx by default merges double slashes in urls, eg:
http://www.bla.com//users becomes http//www.bla.com/users
. This can be a problem for UrWeb
applications since a double slash is actually how urweb encodes
the unit or () value.

The solution is to use the option: "merge_slashes off".

It's not a bug in either application so I didnt want me make an
issue for it, but this could be useful info for other people
running Ur/Web programs behind nginx...

Simon


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur


Re: [Ur] Mandatory nginx conf: merge_slashes off

2019-01-25 Thread Simon Van Casteren
It doesn't happen often of course, since you rarely use unit in a page or
RPC function. How I ran into it was actually via the now fixed bug
https://github.com/urweb/urweb/issues/117, I made some ADT's that got
around that bug by declaring all constructors to have at least one
parameter, unit if nothing else. That came back to bite me now...

A page with this signature:

val page: unit -> string -> transaction page

Would be affected by the issue I described. This obviously won't happen
much outside of you making a mistake (for example because first the
function took just a unit, then you added the string parameter), but
because it doesn't happen often and it's actually nginx making the
"mistake", I still thought it could help someone out in the future!

Simon

On Fri, 25 Jan 2019 at 13:57, Adam Chlipala  wrote:

> Thanks for sharing that wisdom!  Somehow I remember making a special
> effort to encode empty strings with underscores, precisely to avoid this
> problem (though it was appearing in Apache, if I recall correctly).  Can
> you point us to an example where it arises, in a URL that an Ur/Web app
> generates itself?
>
> On 1/25/19 5:13 AM, Simon Van Casteren wrote:
>
> Hi,
>
> I just ran into an awful problem combining urweb with nginx. By default,
> nginx by default merges double slashes in urls, eg:
> http://www.bla.com//users becomes http//www.bla.com/users. This can be a
> problem for UrWeb applications since a double slash is actually how urweb
> encodes the unit or () value.
>
> The solution is to use the option: "merge_slashes off".
>
> It's not a bug in either application so I didnt want me make an issue for
> it, but this could be useful info for other people running Ur/Web programs
> behind nginx...
>
> Simon
>
> ___
> Ur mailing list
> Ur@impredicative.com
> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
>
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur


Re: [Ur] Mandatory nginx conf: merge_slashes off

2019-01-25 Thread Adam Chlipala
Thanks for sharing that wisdom! Somehow I remember making a special 
effort to encode empty strings with underscores, precisely to avoid this 
problem (though it was appearing in Apache, if I recall correctly).  Can 
you point us to an example where it arises, in a URL that an Ur/Web app 
generates itself?


On 1/25/19 5:13 AM, Simon Van Casteren wrote:

Hi,

I just ran into an awful problem combining urweb with nginx. By 
default, nginx by default merges double slashes in urls, eg: 
http://www.bla.com//users becomes http//www.bla.com/users 
. This can be a problem for UrWeb 
applications since a double slash is actually how urweb encodes the 
unit or () value.


The solution is to use the option: "merge_slashes off".

It's not a bug in either application so I didnt want me make an issue 
for it, but this could be useful info for other people running Ur/Web 
programs behind nginx...


Simon
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur


[Ur] Mandatory nginx conf: merge_slashes off

2019-01-25 Thread Simon Van Casteren
Hi,

I just ran into an awful problem combining urweb with nginx. By default,
nginx by default merges double slashes in urls, eg:
http://www.bla.com//users becomes http//www.bla.com/users. This can be a
problem for UrWeb applications since a double slash is actually how urweb
encodes the unit or () value.

The solution is to use the option: "merge_slashes off".

It's not a bug in either application so I didnt want me make an issue for
it, but this could be useful info for other people running Ur/Web programs
behind nginx...

Simon
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur