Re: [Ur] EUnurlify in code to be compiled to JavaScript[2]?

2017-05-01 Thread Adam Chlipala 

On 05/01/2017 09:42 AM, Benjamin Barenblat wrote:

On Sun, Apr 30, 2017 at 1:19 PM, Adam Chlipala  wrote:

Ur/Web doesn't support any interaction with cookies in client-side
code.

Is this because Ur/Web signs all its cookies and doing the signing and
verification on the client side is a security problem?


No, it's because said feature didn't seem necessary to implement so far 
(you can always hoist the cookie reads into the server-side code, 
referring to their variables in client code), /and/ the implementation 
strategy for deserializing cookie values so far happens to use 
server-side-specific code (direct generation of rather imperative C in 
the Ur/Web compiler), so it's not a quick job to extend to client code.
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] EUnurlify in code to be compiled to JavaScript[2]?

2017-05-01 Thread Benjamin Barenblat 
On Sun, Apr 30, 2017 at 1:19 PM, Adam Chlipala  wrote:
> Ur/Web doesn't support any interaction with cookies in client-side
> code.

Is this because Ur/Web signs all its cookies and doing the signing and
verification on the client side is a security problem?

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

Re: [Ur] EUnurlify in code to be compiled to JavaScript[2]?

2017-04-30 Thread Adam Chlipala 
Ah, that one's easy for me to spot.  Ur/Web doesn't support any 
interaction with cookies in client-side code.


On 04/21/2017 07:38 PM, Marko Schütz Schmuck wrote:


cookie auth : string
fun startSession (email : string) : transaction unit
   = setCookie auth {Value = email,
 Expires = None,
 Secure = False}

fun main () : transaction page
   = loggedIn <- source (None : option string);
 scUser <- source "";
 return 
   
   
 vu <- get scUser;
 rpc (startSession vu);
 c <- getCookie auth;
 case c of
 None => set loggedIn None
   | Some _ => set loggedIn (Some vu)}/>
   



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

Re: [Ur] EUnurlify in code to be compiled to JavaScript[2]?

2017-04-21 Thread Marko Schütz Schmuck 
On Fri, 21 Apr 2017 10:51:34 -0400,
Benjamin Barenblat wrote:
> 
> On Wed, Apr 19, 2017 at 3:58 PM, Marko Schütz Schmuck
>  wrote:
> > I'm getting this error. I don't see why this happens.
> 
> Might you be able to produce a smaller, standalone example? I’ve never
> seen that particular error message before, and I can’t reproduce it
> with the attachment you’ve sent, because I don’t have the `Ui`,
> `Default`, or `Password` modules.

Attached is a reduces example. The .urp consists only of a single line
EUnurlify.

Thanks and best regards,

Marko
P.S. Sorry for not paring it down to start with.

cookie auth : string

fun startSession (email : string) : transaction unit
  = setCookie auth {Value = email,
Expires = None,
Secure = False}

fun main () : transaction page
  = loggedIn <- source (None : option string);
scUser <- source "";
return 
  
  
vu <- get scUser;
rpc (startSession vu);
c <- getCookie auth;
case c of
None => set loggedIn None
  | Some _ => set loggedIn (Some vu)}/>
  



pgpjgyNHWkb2A.pgp
Description: OpenPGP Digital Signature
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] EUnurlify in code to be compiled to JavaScript[2]?

2017-04-21 Thread Benjamin Barenblat 
On Wed, Apr 19, 2017 at 3:58 PM, Marko Schütz Schmuck
 wrote:
> I'm getting this error. I don't see why this happens.

Might you be able to produce a smaller, standalone example? I’ve never
seen that particular error message before, and I can’t reproduce it
with the attachment you’ve sent, because I don’t have the `Ui`,
`Default`, or `Password` modules.

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

[Ur] EUnurlify in code to be compiled to JavaScript[2]?

2017-04-19 Thread Marko Schütz Schmuck 
Dear All,

I'm getting this error. I don't see why this happens. Please enlighten
me.

Thanks and best regards,

Marko
structure Theme = Ui.Make(Default)

type user = string

val expireSeconds = 3600 * 4

sequence sessionIds

table session : {Id : int, Key : int, Identifier : string, Expires : time}
  PRIMARY KEY Id

task periodic 60 = fn () => dml (DELETE FROM session
 WHERE Expires < CURRENT_TIMESTAMP)

type authMode
  = {User : user, Session : int, Key : int}

cookie auth : authMode

fun newSession email =
  ses <- nextval sessionIds;
  now <- now;
  key <- rand;
  dml (INSERT INTO session (Id, Key, Identifier, Expires)
 VALUES ({[ses]}, {[key]}, {[email]}, {[addSeconds now 
expireSeconds]}));
  return {Session = ses, Key = key}

fun startSession (email : string) : transaction unit
  = ses <- newSession email;
setCookie auth {Value = ({User = email} ++ ses),
Expires = None,
Secure = False}

fun serverLogin (r : {User : string, Pass : string}) : transaction unit
  = u <- Password.authenticate r;
case u of
None => return ()
  | Some user => startSession user

con toBool = fn (t :: Type) => bool
fun toBool_option [t ::: Type] (a : option t) : toBool (option t)
  = case a of
None => False
  | Some _ => True

fun some [t ::: Type] (op : option t) : t
  = case op of
None => error Cannot get data from option None.
  | Some d => d

fun main () : transaction page
  = loggedIn <- source (None : option string);
scUser <- source "";
scPass <- source "";
c <- getCookie auth;
Theme.simple
"Main"
(Ui.moded (toBool_option c)
 (Ui.const 

   
 vu <- get scUser;
 vp <- get scPass;
 rpc (serverLogin {User = vu, 
Pass = vp});
 c <- getCookie auth;
 case c of
   None => set loggedIn None
 | Some _ => set loggedIn (Some 
vu)}/>
   )
 (Ui.const Logged in as
   {[some 
s]}}/>
   
)
)



pgpOSLAse5k4C.pgp
Description: OpenPGP Digital Signature
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur