Skip to Content.
Sympa Menu

k-user - Re: [K-user] K Time

k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [K-user] K Time


Chronological Thread 
  • From: Omar Duhaiby <3omarz AT gmail.com>
  • To: Dwight Guth <dwight.guth AT runtimeverification.com>
  • Cc: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>, "Musab A. AlTurki" <musab AT kfupm.edu.sa>, "yilong.li AT runtimeverification.com" <yilong.li AT runtimeverification.com>, "traian.serbanuta AT gmail.com" <traian.serbanuta AT gmail.com>
  • Subject: Re: [K-user] K Time
  • Date: Wed, 15 Oct 2014 23:44:57 +0300
  • List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
  • List-id: <k-user.cs.uiuc.edu>

OK. I looked into the pull request of #external IO operator, but it got me more confused! I think my function is easier to implement. I still don't know where to start!

On Fri, Oct 10, 2014 at 2:04 PM, Omar Duhaiby <3omarz AT gmail.com> wrote:
OK. I opened an issue here and I'm looking into the pull request to get an idea how and where to start.

On Thu, Oct 9, 2014 at 5:20 PM, Dwight Guth <dwight.guth AT runtimeverification.com> wrote:
The way I would recommend doing this would be to add a new builtin function, say, #time(), which rewrites to the current number of milliseconds since the epoch. It wouldn't be the most reliable, since you can't completely control when a builtin function decides to evaluate, but it should be basically workable. I suggest you take a look at the following pull request, which does something very similar, and use it as a starting point for your own efforts to implement this functionality.

https://github.com/kframework/k/pull/967

On Thu, Oct 9, 2014 at 8:15 AM, Rosu, Grigore <grosu AT illinois.edu> wrote:
Hi Omar,

This would be great!  Like Traian suggested, why don't you open an issue on github and then try to do it yourself.  Feel free to ask Traian, Dwight, Yilong (all CCed) and myself questions if you have any (but let us now use the k-user list to continue the discussion on this topic).

Thank you,
Grigore
 
 

From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of Omar Duhaiby [3omarz AT gmail.com]
Sent: Thursday, October 09, 2014 6:41 AM
To: traian.serbanuta AT gmail.com
Cc: k-user AT cs.uiuc.edu; Musab A. AlTurki
Subject: Re: [K-user] K Time

I would love to implement it but I don't even know where to start.

How about waiting? Can execution wait or sleep for a certain time?

On Oct 9, 2014 1:13 PM, "Traian Florin Şerbănuţă" <traian.serbanuta AT fmi.unibuc.ro> wrote:
I don't think it has;  but it should be fairly easy to add something like that.

one way to do it would be to have a special stream, similar to input and output which whenever something is requested from it would return the current time.

You can either open an issue for that on the github page (and if enough people care about it it might become a priority to the dev. team), or if you want it bad and quick, you can try implementing it yourself and submitting a pull request.

best wishes,
Traian


2014-10-09 8:49 GMT+03:00 Omar Duhaiby <3omarz AT gmail.com>:
Hello,

Does K have a built-in function that returns the current time?

Thank you
Omar Alzuhaibi

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user








Archive powered by MHonArc 2.6.16.

Top of Page