[racket-users] format-id and blue arrows

[Tim Brown]

Folks,

The following program behaves as I would expect:

;; --
#lang racket
(require (for-syntax racket/syntax))

(define-syntax (def-a/boxed-a stx)
  (syntax-case stx ()
[(_ base-name base-val)
 (with-syntax
 ([box-name (format-id #'base-name #:source #'base-name
"~a-boxed" (syntax-e #'base-name))])
   #'(begin
   (define base-name base-val)
   (define box-name (box base-val]))


(def-a/boxed-a tim #;[1] "42")

tim #;[2]

tim-boxed #;[3]
;; --

Prints:
"22"
'#&"22"

So the variables are defined (maybe that’s a bit of a naïve description
of what’s happened).

But... in DrRacket, I get a blue binding line from the tim at [2] to
the tim at [1]; however, I don’t get a line from tim-boxed at [3] to
the tim at [2].

Am I missing something?
I thought I had annotated the format-id with the necessary.

How does Racket know that tim is defined at [1], but not know that
tim-boxed is also defined (for my purposes) at [1]?

And, strictly, what do the blue lines indicate?


Some context:
I am actually using `prepare` to prepare some database queries. So I
have macros to define: find-a-thing-sql and find-a-thing-sql/prepared
For the most part I use find-a-thing-sql/prepared in my queries; so
*that* is what I want to jump back to the definition of using
"Jump to Binding Occurrence".

Thanks in advance,

Tim

-- 
Tim Brown CEng MBCS 

City Computing Limited · www.cityc.co.uk
  City House · Sutton Park Rd · Sutton · Surrey · SM1 2AE · GB
T:+44 20 8770 2110 · F:+44 20 8770 2130

City Computing Limited registered in London No:1767817.
Registered Office: City House, Sutton Park Road, Sutton, Surrey, SM1 2AE
VAT No: GB 918 4680 96

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Redex Engine Internals

[Anton Podkopaev]

Thank you for your answer, Robby.

Actually at the beginning I planned to implement another version of the
semantics
in Coq and prove something useful about it. But before spending (a lot of)
time with
Coq version, it's better to be sure that the semantics is something I want,
as you
mentioned. And for this purpose I need to be able to run tests, which are
little bit
bigger than ones I can run in a reasonable time now. So I still wonder if
there are
some guidelines, which can help me with my current Redex version.

My supervisor suggested to implement the semantics in Racket, w/o using
Redex
reduction engine, but reusing some Redex functionality (e.g. `traces` and
`stepper`
functions, which are extremely useful). Is it a good idea?

BR,
Anton Podkopaev

2015-12-03 19:44 GMT+03:00 Robby Findler :

> Redex isn't really designed with performance in mind. Some future
> version of Redex will probably improve on this, but perhaps not enough
> for the use case you have in mind.
>
> My best advice (which is kind of depressing that this is the best I
> can do) is to experiment with the Redex version until you're pretty
> sure that you have something you like and then to implement another
> version of the language in some inherently more efficient way. Then
> you can use the Redex version to experiment with variations and to
> provide a test oracle for the more efficient implementation.
>
> hth,
> Robby
>
>
> On Thu, Dec 3, 2015 at 10:14 AM, Anton Podkopaev 
> wrote:
> > Hello, dear colleagues!
> > Could you, please, answer some of my questions?
> >
> > 1) Is there any paper about how the Racket engine works?
> > 2) Is there any guide or a paper about effective (in terms of semantics
> execution) Redex usage?
> >
> > I want to know it because I'm interested in optimizing my semantics in
> Redex.
> >
> > What I want to find in aforementioned papers:
> > - Are environments and holes effective, or I should use them rarely?
> > - Is there any factorization of states during the reduction process?
> > - ...
> >
> > Background story:
> > I'm working on highly non-deterministic semantics for a concurrent
> language using PLT/Redex. Unfortunately, I faced a performance problem ---
> an execution of some tests, which aren't so big, takes too much time (> 40
> minutes). Originally, I though that the problem was in my heap
> representation and I should have factorized it. But an execution of a
> smaller test w/ only 280 states according to `traces` and w/o any
> heap-related problems takes 30 seconds, which is still too much in my
> opinion.
> >
> > ---
> > Best regards,
> > Anton Podkopaev, PhD student, SPbSU
> >
> > --
> > You received this message because you are subscribed to the Google
> Groups "Racket Users" group.
> > To unsubscribe from this group and stop receiving emails from it, send
> an email to racket-users+unsubscr...@googlegroups.com.
> > For more options, visit https://groups.google.com/d/optout.
>

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Re: reducing pauses with incremental GC

[JCG]

> 
> It was definitely less jerky from a user standpoint.

Interestingly, I tried this yesterday on a Debian desktop running on 2008 
2-core  iMac.  It was definitely feeling better with the PLT_INCREMENTAL_GC.  
Running the same image on the same machine underneath VMWare Fusion, the 
PLT_INCREMENTAL_GC was much less fluid than without the setting.  In other 
words, mileage appears to vary.  

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Redex Engine Internals

[Anton Podkopaev]

> One thing to check for is ambiguous patterns. Those can cause
> exponential blowup internally in Redex.

Yes, there are a lot of ambiguous patterns, but it's made intentionally.
Most of the rules have such structure:
(--> ((in-hole E   operation) globalState)
 ((in-hole E (ret value)) globalState'))
where
[E hole
   (E >>= K)
   (par E Expr)
   (par Expr E)]
and the `par` constructor is used to represent different threads.

The performance problem is actual for terms with four threads of such
structure, even if `expr`* are small ones:
(par (par expr0
  expr1)
 (par expr2
  expr3))

> But just to double check: when you run one of the examples that takes
> a long time, how many different terms are you getting? Millions or
> dozens? If dozens, then we may have a hope of fixing something.

I think there are thousands of terms. As I mentioned before I'm not
completely satisfied with performance even for cases with 270 terms.
BTW, is there a better way to get a number of terms than to execute
`traces` and see a number it shows?

> As for implementing it in Racket, if you write the one-step function
> of a reduction semantics as a Racket function, then you can certainly
> use traces to visualize it. One trick is to write:

Thank you, it's realy nice trick.

> If you have a concrete example that you think is mysteriously slow,
> then perhaps you could send me a complete program (that runs that
> example)? I would be happy to take a look.

Yes, I have some examples, but they are too complex to be shown,
and it'll take too much time to extract them from the project
, but they are here

:
- `term_Big` is a term, a reduction of which leads to 270 terms according
   to `traces`, and `test-->>` run takes 30 seconds. I think it should be
much faster.
- The `test-->>` run for `term_WW_WRMW_W_RRR` takes dozens of minutes.
Appropriate `test-->>` calls are commented out.

The project: https://github.com/anlun/OperationalSemanticsC11
The file with terms:
https://github.com/anlun/OperationalSemanticsC11/blob/master/test%2FrelAcqNaRlxPost_t1.rkt


BR,
Anton Podkopaev

2015-12-04 15:52 GMT+03:00 Robby Findler :

> Well, maybe there is a bug somewhere; if you're trying to run
> paper-sized examples you should be able to get them to complete
> reasonably quickly.
>
> One thing to check for is ambiguous patterns. Those can cause
> exponential blowup internally in Redex.
>
> But just to double check: when you run one of the examples that takes
> a long time, how many different terms are you getting? Millions or
> dozens? If dozens, then we may have a hope of fixing something.
>
> As for implementing it in Racket, if you write the one-step function
> of a reduction semantics as a Racket function, then you can certainly
> use traces to visualize it. One trick is to write:
>
>  (define-language empty)
>  (reduction-relation empty (--> any ,(call-my-racket-implementation
> (term any
>
> I would say that if you do do that and the time to reduce goes from 40
> minutes to milliseconds, then there is either a performance bug in
> Redex or an ambiguity that's tripping Redex up in the patterns in your
> language (or they are not the same language, I suppose).
>
> If you have a concrete example that you think is mysteriously slow,
> then perhaps you could send me a complete program (that runs that
> example)? I would be happy to take a look.
>
> Robby
>
>
> On Fri, Dec 4, 2015 at 5:14 AM, Anton Podkopaev 
> wrote:
> > Thank you for your answer, Robby.
> >
> > Actually at the beginning I planned to implement another version of the
> > semantics
> > in Coq and prove something useful about it. But before spending (a lot
> of)
> > time with
> > Coq version, it's better to be sure that the semantics is something I
> want,
> > as you
> > mentioned. And for this purpose I need to be able to run tests, which are
> > little bit
> > bigger than ones I can run in a reasonable time now. So I still wonder if
> > there are
> > some guidelines, which can help me with my current Redex version.
> >
> > My supervisor suggested to implement the semantics in Racket, w/o using
> > Redex
> > reduction engine, but reusing some Redex functionality (e.g. `traces` and
> > `stepper`
> > functions, which are extremely useful). Is it a good idea?
> >
> > BR,
> > Anton Podkopaev
> >
> > 2015-12-03 19:44 GMT+03:00 Robby Findler :
> >>
> >> Redex isn't really designed with performance in mind. Some future
> >> version of Redex will probably improve on this, but perhaps not enough
> >> for the use case you have in mind.
> >>
> >> My best advice (which is kind of depressing that this is the best I
> >> can do) is to experiment with the Redex version until you're pretty
> >> sure that you have something you like and then to 

[racket-users] Syntax checker suggestion

[brendan]

I was messing around in DrRacket and started writing a macro. When I finished 
the first draft it gave me an error message saying that I can't use the _ 
wildcard in an expression context. I figured I had misremembered the format so 
I went to the syntax-parse docs... well, to shorten the story I had actually 
forgotten that syntax/parse has to be required for-syntax. Similar things have 
happened to me a few times. A more experienced user would have identified the 
problem immediately, of course, however it might be helpful for novices like me 
if the checker looked for unbound identifiers at lower levels of nesting before 
reporting errors at higher levels... if that wouldn't take a major rewrite.

...Y'know, let me concentrated my obvious noobness in one post :) and ask a 
silly question: why is "free-identifier=?" so named? It compares identifier 
bindings, which obviously implies that the identifiers are not "free" at all. I 
only got the hang of that one when I started mentally renaming it to 
"identifier-binding-site=?".

Thanks for your help.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] format-id and blue arrows

[Robby Findler]

On Fri, Dec 4, 2015 at 8:45 AM, Tim Brown  wrote:
> These examples seem to work fine without syntax-local-introduce on the 
> identifiers. What is s-l-i’s role in this code?

The syntax-local-introduce compensates for the extra
macro-introduction scope that the expander puts on the identifiers
(which it doesn't put onto properties in the result of the macro
transformer). It makes sure that the identifier compare as the same
identifier by the time check syntax gets its hands on them.  at
least I think that was the point of it.

I see the same thing you do, however, that removing it still works. I
suppose that's due to the new expander and I wonder if there might be
another way in which one could supply identifiers to this macro such
that the syntax-local-introduce version works but the other doesn't. I
woudl guess there is, but I'm really not sure of that at all.

Robby

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Redex Engine Internals

[Robby Findler]

Well, maybe there is a bug somewhere; if you're trying to run
paper-sized examples you should be able to get them to complete
reasonably quickly.

One thing to check for is ambiguous patterns. Those can cause
exponential blowup internally in Redex.

But just to double check: when you run one of the examples that takes
a long time, how many different terms are you getting? Millions or
dozens? If dozens, then we may have a hope of fixing something.

As for implementing it in Racket, if you write the one-step function
of a reduction semantics as a Racket function, then you can certainly
use traces to visualize it. One trick is to write:

 (define-language empty)
 (reduction-relation empty (--> any ,(call-my-racket-implementation
(term any

I would say that if you do do that and the time to reduce goes from 40
minutes to milliseconds, then there is either a performance bug in
Redex or an ambiguity that's tripping Redex up in the patterns in your
language (or they are not the same language, I suppose).

If you have a concrete example that you think is mysteriously slow,
then perhaps you could send me a complete program (that runs that
example)? I would be happy to take a look.

Robby


On Fri, Dec 4, 2015 at 5:14 AM, Anton Podkopaev  wrote:
> Thank you for your answer, Robby.
>
> Actually at the beginning I planned to implement another version of the
> semantics
> in Coq and prove something useful about it. But before spending (a lot of)
> time with
> Coq version, it's better to be sure that the semantics is something I want,
> as you
> mentioned. And for this purpose I need to be able to run tests, which are
> little bit
> bigger than ones I can run in a reasonable time now. So I still wonder if
> there are
> some guidelines, which can help me with my current Redex version.
>
> My supervisor suggested to implement the semantics in Racket, w/o using
> Redex
> reduction engine, but reusing some Redex functionality (e.g. `traces` and
> `stepper`
> functions, which are extremely useful). Is it a good idea?
>
> BR,
> Anton Podkopaev
>
> 2015-12-03 19:44 GMT+03:00 Robby Findler :
>>
>> Redex isn't really designed with performance in mind. Some future
>> version of Redex will probably improve on this, but perhaps not enough
>> for the use case you have in mind.
>>
>> My best advice (which is kind of depressing that this is the best I
>> can do) is to experiment with the Redex version until you're pretty
>> sure that you have something you like and then to implement another
>> version of the language in some inherently more efficient way. Then
>> you can use the Redex version to experiment with variations and to
>> provide a test oracle for the more efficient implementation.
>>
>> hth,
>> Robby
>>
>>
>> On Thu, Dec 3, 2015 at 10:14 AM, Anton Podkopaev 
>> wrote:
>> > Hello, dear colleagues!
>> > Could you, please, answer some of my questions?
>> >
>> > 1) Is there any paper about how the Racket engine works?
>> > 2) Is there any guide or a paper about effective (in terms of semantics
>> > execution) Redex usage?
>> >
>> > I want to know it because I'm interested in optimizing my semantics in
>> > Redex.
>> >
>> > What I want to find in aforementioned papers:
>> > - Are environments and holes effective, or I should use them rarely?
>> > - Is there any factorization of states during the reduction process?
>> > - ...
>> >
>> > Background story:
>> > I'm working on highly non-deterministic semantics for a concurrent
>> > language using PLT/Redex. Unfortunately, I faced a performance problem ---
>> > an execution of some tests, which aren't so big, takes too much time (> 40
>> > minutes). Originally, I though that the problem was in my heap
>> > representation and I should have factorized it. But an execution of a
>> > smaller test w/ only 280 states according to `traces` and w/o any
>> > heap-related problems takes 30 seconds, which is still too much in my
>> > opinion.
>> >
>> > ---
>> > Best regards,
>> > Anton Podkopaev, PhD student, SPbSU
>> >
>> > --
>> > You received this message because you are subscribed to the Google
>> > Groups "Racket Users" group.
>> > To unsubscribe from this group and stop receiving emails from it, send
>> > an email to racket-users+unsubscr...@googlegroups.com.
>> > For more options, visit https://groups.google.com/d/optout.
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] format-id and blue arrows

[Tim Brown]

Robby,

Thanks for that.

The following works splendidly for me (and is ripped pretty well
straight off from the Check_Syntax page you quoted below):
~
(define-syntax (def-a/boxed-a stx)
  (syntax-case stx ()
[(_ base-name base-val)
 (let ()
   (define boxed-name
 (format-id #'base-name #:source #'base-name "~a-boxed"
(syntax-e #'base-name)))
   (define base-len
 (string-length (symbol->string (syntax-e #'base-name
   #`(begin
   (define base-name base-val)
   #,(syntax-property
  #`(define #,boxed-name (box base-val))
  'sub-range-binders
  (list
   (vector (syntax-local-introduce boxed-name)
   0 base-len 0.5 0.5
   (syntax-local-introduce #'base-name)
   0 base-len 0.5 0.5)]))
~

I can use this, but I can’t add the syntax-property at a place that
would make it useful in format-id. If I understand correctly) the
syntax-property is being added to the whole binding of boxed-name to
(box base-val). If I try to add a property to boxed-name alone:
~
(define-syntax (def-a/boxed-a:2 stx)
  (syntax-case stx ()
[(_ base-name base-val)
 (let ()
   (define base-len (string-length (symbol->string (syntax-e
#'base-name
   (define boxed-name
 (format-id #'base-name #:source #'base-name "~a-boxed"
(syntax-e #'base-name)))

   #`(begin
   (define base-name base-val)
   (define #,(syntax-property
  boxed-name
  'sub-range-binders
  (list
   (vector (syntax-local-introduce boxed-name)
   0 base-len 0.5 0.5
   (syntax-local-introduce #'base-name)
   0 base-len 0.5 0.5)))
 (box base-val]))

(def-a/boxed-a:2 bar 22)
~

The sub-range-bindings on bar-boxed are not recognised (although
bar-boxed *is* bound to (box 22)).

If I can’t do what I’m trying in def-a/boxed-a:2; I cannot then move the
wrapping up around format-id to attempt to bake it into format id (by
mapping it over the ‘v’ arguments, for example).

Is it right to be moving this annotation up into format-id in the first
place? (I have no opinion now I have a pattern to follow, above).

Suggestions on next steps?


Tim

On 04/12/15 13:06, Robby Findler wrote:
> Looking at the implementation of format-id, I see that it doesn't do
> what would be needed to be done in order to make the arrows in
> DrRacket show up like they do for define-syntax. I think this would be
> a great addition, however! It basically needs to set up some
> properties on the identifier.
> 
> If you (or anyone) wants to look into fixing this, these are the relevant 
> docs:
> 
> http://docs.racket-lang.org/tools/Check_Syntax.html
> 
> Look for the description of "sub-range-binders".
> 
> Robby
> 
> 
> On Fri, Dec 4, 2015 at 4:27 AM, Tim Brown  wrote:
>> Folks,
>>
>> The following program behaves as I would expect:
>>
>> ;; --
>> #lang racket
>> (require (for-syntax racket/syntax))
>>
>> (define-syntax (def-a/boxed-a stx)
>>   (syntax-case stx ()
>> [(_ base-name base-val)
>>  (with-syntax
>>  ([box-name (format-id #'base-name #:source #'base-name
>> "~a-boxed" (syntax-e #'base-name))])
>>#'(begin
>>(define base-name base-val)
>>(define box-name (box base-val]))
>>
>>
>> (def-a/boxed-a tim #;[1] "42")
>>
>> tim #;[2]
>>
>> tim-boxed #;[3]
>> ;; --
>>
>> Prints:
>> "22"
>> '#&"22"
>>
>> So the variables are defined (maybe that’s a bit of a naïve description
>> of what’s happened).
>>
>> But... in DrRacket, I get a blue binding line from the tim at [2] to
>> the tim at [1]; however, I don’t get a line from tim-boxed at [3] to
>> the tim at [2].
>>
>> Am I missing something?
>> I thought I had annotated the format-id with the necessary.
>>
>> How does Racket know that tim is defined at [1], but not know that
>> tim-boxed is also defined (for my purposes) at [1]?
>>
>> And, strictly, what do the blue lines indicate?
>>
>>
>> Some context:
>> I am actually using `prepare` to prepare some database queries. So I
>> have macros to define: find-a-thing-sql and find-a-thing-sql/prepared
>> For the most part I use find-a-thing-sql/prepared in my queries; so
>> *that* is what I want to jump back to the definition of using
>> "Jump to Binding Occurrence".
>>
>> Thanks in advance,
>>
>> Tim
>>
>> --
>> Tim Brown CEng MBCS 

Re: [racket-users] format-id and blue arrows

[Robby Findler]

Looking at the implementation of format-id, I see that it doesn't do
what would be needed to be done in order to make the arrows in
DrRacket show up like they do for define-syntax. I think this would be
a great addition, however! It basically needs to set up some
properties on the identifier.

If you (or anyone) wants to look into fixing this, these are the relevant docs:

http://docs.racket-lang.org/tools/Check_Syntax.html

Look for the description of "sub-range-binders".

Robby


On Fri, Dec 4, 2015 at 4:27 AM, Tim Brown  wrote:
> Folks,
>
> The following program behaves as I would expect:
>
> ;; --
> #lang racket
> (require (for-syntax racket/syntax))
>
> (define-syntax (def-a/boxed-a stx)
>   (syntax-case stx ()
> [(_ base-name base-val)
>  (with-syntax
>  ([box-name (format-id #'base-name #:source #'base-name
> "~a-boxed" (syntax-e #'base-name))])
>#'(begin
>(define base-name base-val)
>(define box-name (box base-val]))
>
>
> (def-a/boxed-a tim #;[1] "42")
>
> tim #;[2]
>
> tim-boxed #;[3]
> ;; --
>
> Prints:
> "22"
> '#&"22"
>
> So the variables are defined (maybe that’s a bit of a naïve description
> of what’s happened).
>
> But... in DrRacket, I get a blue binding line from the tim at [2] to
> the tim at [1]; however, I don’t get a line from tim-boxed at [3] to
> the tim at [2].
>
> Am I missing something?
> I thought I had annotated the format-id with the necessary.
>
> How does Racket know that tim is defined at [1], but not know that
> tim-boxed is also defined (for my purposes) at [1]?
>
> And, strictly, what do the blue lines indicate?
>
>
> Some context:
> I am actually using `prepare` to prepare some database queries. So I
> have macros to define: find-a-thing-sql and find-a-thing-sql/prepared
> For the most part I use find-a-thing-sql/prepared in my queries; so
> *that* is what I want to jump back to the definition of using
> "Jump to Binding Occurrence".
>
> Thanks in advance,
>
> Tim
>
> --
> Tim Brown CEng MBCS 
> 
> City Computing Limited · www.cityc.co.uk
>   City House · Sutton Park Rd · Sutton · Surrey · SM1 2AE · GB
> T:+44 20 8770 2110 · F:+44 20 8770 2130
> 
> City Computing Limited registered in London No:1767817.
> Registered Office: City House, Sutton Park Road, Sutton, Surrey, SM1 2AE
> VAT No: GB 918 4680 96
>
> --
> You received this message because you are subscribed to the Google Groups 
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an 
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] format-id and blue arrows

[Tim Brown]

These examples seem to work fine without syntax-local-introduce on the 
identifiers. What is s-l-i’s role in this code?

Tim

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Redex Engine Internals

[Jay McCarthy]

Hi Anton,

It wasn't really designed for general use, but I had a similar problem
building a machine for evaluating Java. I made a revised version of Redex
(called "Fedex") that removed a lot of features we weren't using (most
importantly, evaluation contexts) and I got very good results. I found Fedex to
be thousands and thousands of times faster. The model of Java running
a Church-encoded
factorial takes days in Redex but seconds in Fedex. I experimented with
taking the techniques and applying to general Redex programs, but Redex
allows lots of bizarre things that were pretty hard to capture (in fact, it
was partly this conversation that led to the ASPLAS paper in 2011.)

Anyways, here's the model:

https://github.com/ericmercer/4M/blob/master/4M/super_model/super-model.rkt

And here's Fedex:

https://github.com/ericmercer/4M/blob/master/4M/super_model/fedex.rkt

Jay


On Fri, Dec 4, 2015 at 10:32 AM, Anton Podkopaev 
wrote:

> > One thing to check for is ambiguous patterns. Those can cause
> > exponential blowup internally in Redex.
>
> Yes, there are a lot of ambiguous patterns, but it's made intentionally.
> Most of the rules have such structure:
> (--> ((in-hole E   operation) globalState)
>  ((in-hole E (ret value)) globalState'))
> where
> [E hole
>(E >>= K)
>(par E Expr)
>(par Expr E)]
> and the `par` constructor is used to represent different threads.
>
> The performance problem is actual for terms with four threads of such
> structure, even if `expr`* are small ones:
> (par (par expr0
>   expr1)
>  (par expr2
>   expr3))
>
> > But just to double check: when you run one of the examples that takes
> > a long time, how many different terms are you getting? Millions or
> > dozens? If dozens, then we may have a hope of fixing something.
>
> I think there are thousands of terms. As I mentioned before I'm not
> completely satisfied with performance even for cases with 270 terms.
> BTW, is there a better way to get a number of terms than to execute
> `traces` and see a number it shows?
>
> > As for implementing it in Racket, if you write the one-step function
> > of a reduction semantics as a Racket function, then you can certainly
> > use traces to visualize it. One trick is to write:
>
> Thank you, it's realy nice trick.
>
> > If you have a concrete example that you think is mysteriously slow,
> > then perhaps you could send me a complete program (that runs that
> > example)? I would be happy to take a look.
>
> Yes, I have some examples, but they are too complex to be shown,
> and it'll take too much time to extract them from the project
> , but they are here
> 
> :
> - `term_Big` is a term, a reduction of which leads to 270 terms according
>to `traces`, and `test-->>` run takes 30 seconds. I think it should be
> much faster.
> - The `test-->>` run for `term_WW_WRMW_W_RRR` takes dozens of minutes.
> Appropriate `test-->>` calls are commented out.
>
> The project: https://github.com/anlun/OperationalSemanticsC11
> The file with terms:
> https://github.com/anlun/OperationalSemanticsC11/blob/master/test%2FrelAcqNaRlxPost_t1.rkt
>
>
> BR,
> Anton Podkopaev
>
> 2015-12-04 15:52 GMT+03:00 Robby Findler :
>
>> Well, maybe there is a bug somewhere; if you're trying to run
>> paper-sized examples you should be able to get them to complete
>> reasonably quickly.
>>
>> One thing to check for is ambiguous patterns. Those can cause
>> exponential blowup internally in Redex.
>>
>> But just to double check: when you run one of the examples that takes
>> a long time, how many different terms are you getting? Millions or
>> dozens? If dozens, then we may have a hope of fixing something.
>>
>> As for implementing it in Racket, if you write the one-step function
>> of a reduction semantics as a Racket function, then you can certainly
>> use traces to visualize it. One trick is to write:
>>
>>  (define-language empty)
>>  (reduction-relation empty (--> any ,(call-my-racket-implementation
>> (term any
>>
>> I would say that if you do do that and the time to reduce goes from 40
>> minutes to milliseconds, then there is either a performance bug in
>> Redex or an ambiguity that's tripping Redex up in the patterns in your
>> language (or they are not the same language, I suppose).
>>
>> If you have a concrete example that you think is mysteriously slow,
>> then perhaps you could send me a complete program (that runs that
>> example)? I would be happy to take a look.
>>
>> Robby
>>
>>
>> On Fri, Dec 4, 2015 at 5:14 AM, Anton Podkopaev 
>> wrote:
>> > Thank you for your answer, Robby.
>> >
>> > Actually at the beginning I planned to implement another version of the
>> > semantics
>> > in Coq and prove something useful about it. But before spending (a lot
>> of)
>> > time 

Re: [racket-users] Redex Engine Internals

[Robby Findler]

It looks like your semantics has a lot of different ways to reach the
same term (ie the reduction graph has a lot of sharing in it).

In it's default mode, test-->> (and apply-reduction-relation*) will
not notice this sharing and explore all of the different paths, which
can be very expensive.

I think you want to do this:

 (current-cache-all? #t)

That should speed up the test case for (term (,term_Big defaultState))
by about 50x and perhaps you will see similar speedups on other test
cases.

There is a little more discussion in the docs for apply-reduction-relation*.

Robby


On Fri, Dec 4, 2015 at 9:32 AM, Anton Podkopaev  wrote:
>> One thing to check for is ambiguous patterns. Those can cause
>> exponential blowup internally in Redex.
>
> Yes, there are a lot of ambiguous patterns, but it's made intentionally.
> Most of the rules have such structure:
> (--> ((in-hole E   operation) globalState)
>  ((in-hole E (ret value)) globalState'))
> where
> [E hole
>(E >>= K)
>(par E Expr)
>(par Expr E)]
> and the `par` constructor is used to represent different threads.
>
> The performance problem is actual for terms with four threads of such
> structure, even if `expr`* are small ones:
> (par (par expr0
>   expr1)
>  (par expr2
>   expr3))
>
>> But just to double check: when you run one of the examples that takes
>> a long time, how many different terms are you getting? Millions or
>> dozens? If dozens, then we may have a hope of fixing something.
>
> I think there are thousands of terms. As I mentioned before I'm not
> completely satisfied with performance even for cases with 270 terms.
> BTW, is there a better way to get a number of terms than to execute
> `traces` and see a number it shows?
>
>> As for implementing it in Racket, if you write the one-step function
>> of a reduction semantics as a Racket function, then you can certainly
>> use traces to visualize it. One trick is to write:
>
> Thank you, it's realy nice trick.
>
>> If you have a concrete example that you think is mysteriously slow,
>> then perhaps you could send me a complete program (that runs that
>> example)? I would be happy to take a look.
>
> Yes, I have some examples, but they are too complex to be shown,
> and it'll take too much time to extract them from the project, but they are
> here:
> - `term_Big` is a term, a reduction of which leads to 270 terms according
>to `traces`, and `test-->>` run takes 30 seconds. I think it should be
> much faster.
> - The `test-->>` run for `term_WW_WRMW_W_RRR` takes dozens of minutes.
> Appropriate `test-->>` calls are commented out.
>
> The project: https://github.com/anlun/OperationalSemanticsC11
> The file with terms:
> https://github.com/anlun/OperationalSemanticsC11/blob/master/test%2FrelAcqNaRlxPost_t1.rkt
>
>
> BR,
> Anton Podkopaev
>
> 2015-12-04 15:52 GMT+03:00 Robby Findler :
>>
>> Well, maybe there is a bug somewhere; if you're trying to run
>> paper-sized examples you should be able to get them to complete
>> reasonably quickly.
>>
>> One thing to check for is ambiguous patterns. Those can cause
>> exponential blowup internally in Redex.
>>
>> But just to double check: when you run one of the examples that takes
>> a long time, how many different terms are you getting? Millions or
>> dozens? If dozens, then we may have a hope of fixing something.
>>
>> As for implementing it in Racket, if you write the one-step function
>> of a reduction semantics as a Racket function, then you can certainly
>> use traces to visualize it. One trick is to write:
>>
>>  (define-language empty)
>>  (reduction-relation empty (--> any ,(call-my-racket-implementation
>> (term any
>>
>> I would say that if you do do that and the time to reduce goes from 40
>> minutes to milliseconds, then there is either a performance bug in
>> Redex or an ambiguity that's tripping Redex up in the patterns in your
>> language (or they are not the same language, I suppose).
>>
>> If you have a concrete example that you think is mysteriously slow,
>> then perhaps you could send me a complete program (that runs that
>> example)? I would be happy to take a look.
>>
>> Robby
>>
>>
>> On Fri, Dec 4, 2015 at 5:14 AM, Anton Podkopaev 
>> wrote:
>> > Thank you for your answer, Robby.
>> >
>> > Actually at the beginning I planned to implement another version of the
>> > semantics
>> > in Coq and prove something useful about it. But before spending (a lot
>> > of)
>> > time with
>> > Coq version, it's better to be sure that the semantics is something I
>> > want,
>> > as you
>> > mentioned. And for this purpose I need to be able to run tests, which
>> > are
>> > little bit
>> > bigger than ones I can run in a reasonable time now. So I still wonder
>> > if
>> > there are
>> > some guidelines, which can help me with my current Redex version.
>> >
>> > My supervisor suggested to implement the semantics in Racket, w/o using
>> 

Re: [racket-users] format-id and blue arrows

[Robby Findler]

On Fri, Dec 4, 2015 at 10:36 AM, Alex Knauth  wrote:
> I just happened to run into that exact problem yesterday, and my solution
> was to have an `id-append` function that returned two values:
> https://github.com/AlexKnauth/lens/blob/0b026923508eabdff241cad861c5e1c4008cfb19/unstable/lens/private/id-append.rkt
>
> The first for the identifier, and the second for the value of the syntax
> property, which the user of the function would have to get with
> define-values and attach it someplace other that the identifier itself.
>
> With your fix, (if I only cared about future versions of racket) would it be
> able to return the identifier with the syntax property on it instead of
> doing this two-value stuff?

Yes (assuming the one identifier survives to the result of the
expansion in a binding position).

Robby

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] format-id and blue arrows

[Robby Findler]

I've pushed a fix to DrRacket to look for the property on occurrences
of binding identifiers.

Thanks!

Robby

On Fri, Dec 4, 2015 at 7:45 AM, Tim Brown  wrote:
> Robby,
>
> Thanks for that.
>
> The following works splendidly for me (and is ripped pretty well
> straight off from the Check_Syntax page you quoted below):
> ~
> (define-syntax (def-a/boxed-a stx)
>   (syntax-case stx ()
> [(_ base-name base-val)
>  (let ()
>(define boxed-name
>  (format-id #'base-name #:source #'base-name "~a-boxed"
> (syntax-e #'base-name)))
>(define base-len
>  (string-length (symbol->string (syntax-e #'base-name
>#`(begin
>(define base-name base-val)
>#,(syntax-property
>   #`(define #,boxed-name (box base-val))
>   'sub-range-binders
>   (list
>(vector (syntax-local-introduce boxed-name)
>0 base-len 0.5 0.5
>(syntax-local-introduce #'base-name)
>0 base-len 0.5 0.5)]))
> ~
>
> I can use this, but I can’t add the syntax-property at a place that
> would make it useful in format-id. If I understand correctly) the
> syntax-property is being added to the whole binding of boxed-name to
> (box base-val). If I try to add a property to boxed-name alone:
> ~
> (define-syntax (def-a/boxed-a:2 stx)
>   (syntax-case stx ()
> [(_ base-name base-val)
>  (let ()
>(define base-len (string-length (symbol->string (syntax-e
> #'base-name
>(define boxed-name
>  (format-id #'base-name #:source #'base-name "~a-boxed"
> (syntax-e #'base-name)))
>
>#`(begin
>(define base-name base-val)
>(define #,(syntax-property
>   boxed-name
>   'sub-range-binders
>   (list
>(vector (syntax-local-introduce boxed-name)
>0 base-len 0.5 0.5
>(syntax-local-introduce #'base-name)
>0 base-len 0.5 0.5)))
>  (box base-val]))
>
> (def-a/boxed-a:2 bar 22)
> ~
>
> The sub-range-bindings on bar-boxed are not recognised (although
> bar-boxed *is* bound to (box 22)).
>
> If I can’t do what I’m trying in def-a/boxed-a:2; I cannot then move the
> wrapping up around format-id to attempt to bake it into format id (by
> mapping it over the ‘v’ arguments, for example).
>
> Is it right to be moving this annotation up into format-id in the first
> place? (I have no opinion now I have a pattern to follow, above).
>
> Suggestions on next steps?
>
>
> Tim
>
> On 04/12/15 13:06, Robby Findler wrote:
>> Looking at the implementation of format-id, I see that it doesn't do
>> what would be needed to be done in order to make the arrows in
>> DrRacket show up like they do for define-syntax. I think this would be
>> a great addition, however! It basically needs to set up some
>> properties on the identifier.
>>
>> If you (or anyone) wants to look into fixing this, these are the relevant 
>> docs:
>>
>> http://docs.racket-lang.org/tools/Check_Syntax.html
>>
>> Look for the description of "sub-range-binders".
>>
>> Robby
>>
>>
>> On Fri, Dec 4, 2015 at 4:27 AM, Tim Brown  wrote:
>>> Folks,
>>>
>>> The following program behaves as I would expect:
>>>
>>> ;; --
>>> #lang racket
>>> (require (for-syntax racket/syntax))
>>>
>>> (define-syntax (def-a/boxed-a stx)
>>>   (syntax-case stx ()
>>> [(_ base-name base-val)
>>>  (with-syntax
>>>  ([box-name (format-id #'base-name #:source #'base-name
>>> "~a-boxed" (syntax-e #'base-name))])
>>>#'(begin
>>>(define base-name base-val)
>>>(define box-name (box base-val]))
>>>
>>>
>>> (def-a/boxed-a tim #;[1] "42")
>>>
>>> tim #;[2]
>>>
>>> tim-boxed #;[3]
>>> ;; --
>>>
>>> Prints:
>>> "22"
>>> '#&"22"
>>>
>>> So the variables are defined (maybe that’s a bit of a naïve description
>>> of what’s happened).
>>>
>>> But... in DrRacket, I get a blue binding line from the tim at [2] to
>>> the tim at [1]; however, I don’t get a line from tim-boxed at [3] to
>>> the tim at [2].
>>>
>>> Am I missing something?
>>> I thought I had annotated the format-id with the necessary.
>>>
>>> How does Racket know that tim is defined at [1], but not know that
>>> tim-boxed is also defined (for my purposes) at [1]?
>>>
>>> And, strictly, what do the blue lines indicate?
>>>
>>>
>>> Some context:
>>> I am actually using 

Re: [racket-users] format-id and blue arrows

[Alex Knauth]

I just happened to run into that exact problem yesterday, and my solution was 
to have an `id-append` function that returned two values:
https://github.com/AlexKnauth/lens/blob/0b026923508eabdff241cad861c5e1c4008cfb19/unstable/lens/private/id-append.rkt
 


The first for the identifier, and the second for the value of the syntax 
property, which the user of the function would have to get with define-values 
and attach it someplace other that the identifier itself.

With your fix, (if I only cared about future versions of racket) would it be 
able to return the identifier with the syntax property on it instead of doing 
this two-value stuff?

Alex Knauth


> On Dec 4, 2015, at 11:15 AM, Robby Findler  
> wrote:
> 
> I've pushed a fix to DrRacket to look for the property on occurrences
> of binding identifiers.
> 
> Thanks!
> 
> Robby
> 
> On Fri, Dec 4, 2015 at 7:45 AM, Tim Brown  wrote:
>> Robby,
>> 
>> Thanks for that.
>> 
>> The following works splendidly for me (and is ripped pretty well
>> straight off from the Check_Syntax page you quoted below):
>> ~
>> (define-syntax (def-a/boxed-a stx)
>>  (syntax-case stx ()
>>[(_ base-name base-val)
>> (let ()
>>   (define boxed-name
>> (format-id #'base-name #:source #'base-name "~a-boxed"
>>(syntax-e #'base-name)))
>>   (define base-len
>> (string-length (symbol->string (syntax-e #'base-name
>>   #`(begin
>>   (define base-name base-val)
>>   #,(syntax-property
>>  #`(define #,boxed-name (box base-val))
>>  'sub-range-binders
>>  (list
>>   (vector (syntax-local-introduce boxed-name)
>>   0 base-len 0.5 0.5
>>   (syntax-local-introduce #'base-name)
>>   0 base-len 0.5 0.5)]))
>> ~
>> 
>> I can use this, but I can’t add the syntax-property at a place that
>> would make it useful in format-id. If I understand correctly) the
>> syntax-property is being added to the whole binding of boxed-name to
>> (box base-val). If I try to add a property to boxed-name alone:
>> ~
>> (define-syntax (def-a/boxed-a:2 stx)
>>  (syntax-case stx ()
>>[(_ base-name base-val)
>> (let ()
>>   (define base-len (string-length (symbol->string (syntax-e
>> #'base-name
>>   (define boxed-name
>> (format-id #'base-name #:source #'base-name "~a-boxed"
>> (syntax-e #'base-name)))
>> 
>>   #`(begin
>>   (define base-name base-val)
>>   (define #,(syntax-property
>>  boxed-name
>>  'sub-range-binders
>>  (list
>>   (vector (syntax-local-introduce boxed-name)
>>   0 base-len 0.5 0.5
>>   (syntax-local-introduce #'base-name)
>>   0 base-len 0.5 0.5)))
>> (box base-val]))
>> 
>> (def-a/boxed-a:2 bar 22)
>> ~
>> 
>> The sub-range-bindings on bar-boxed are not recognised (although
>> bar-boxed *is* bound to (box 22)).
>> 
>> If I can’t do what I’m trying in def-a/boxed-a:2; I cannot then move the
>> wrapping up around format-id to attempt to bake it into format id (by
>> mapping it over the ‘v’ arguments, for example).
>> 
>> Is it right to be moving this annotation up into format-id in the first
>> place? (I have no opinion now I have a pattern to follow, above).
>> 
>> Suggestions on next steps?
>> 
>> 
>> Tim
>> 
>> On 04/12/15 13:06, Robby Findler wrote:
>>> Looking at the implementation of format-id, I see that it doesn't do
>>> what would be needed to be done in order to make the arrows in
>>> DrRacket show up like they do for define-syntax. I think this would be
>>> a great addition, however! It basically needs to set up some
>>> properties on the identifier.
>>> 
>>> If you (or anyone) wants to look into fixing this, these are the relevant 
>>> docs:
>>> 
>>> http://docs.racket-lang.org/tools/Check_Syntax.html
>>> 
>>> Look for the description of "sub-range-binders".
>>> 
>>> Robby
>>> 
>>> 
>>> On Fri, Dec 4, 2015 at 4:27 AM, Tim Brown  wrote:
 Folks,
 
 The following program behaves as I would expect:
 
 ;; --
 #lang racket
 (require (for-syntax racket/syntax))
 
 (define-syntax (def-a/boxed-a stx)
  (syntax-case stx ()
[(_ base-name base-val)
 (with-syntax
 ([box-name (format-id #'base-name #:source 

[racket-users] Re: racket execution

[Héctor Mc]

Hi Asumu,

Thanks for reply, the project is in https://github.com/hmcab/anauj.git , and 
the server run from generacion-datos/codegen.rkt on the bottom the file. Read 
the readme file before the execution.

At this time I have the application on amazon server to prove it, but every time
that I leave the ssh connection, and so, the application is executed with 
racket -t codegen.rkt &, this falls (no any access from the browser is 
achieved), but if I enter to the amazon server with ssh again, the process is 
still there.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Re: racket execution

[George Neuner]

On 12/4/2015 11:47 AM, Héctor Mc wrote:

... the project is in https://github.com/hmcab/anauj.git , and the server run 
from generacion-datos/codegen.rkt on the bottom the file. Read the readme file 
before the execution.

At this time I have the application on amazon server to prove it, but every time
that I leave the ssh connection, and so, the application is executed with
racket -t codegen.rkt &, this falls (no any access from the browser is 
achieved), but if I enter to the amazon server with ssh again, the process is still 
there.




Ordinarily, a background process keeps running when its controlling 
terminal is closed.  However, if the process ever writes anything to the 
terminal (stdout or stderr) and the write is not redirected into a file, 
the write will stall the process (or at least the thread that did the 
write).


The other problem is that when you log out, the process becomes an 
orphan and ownership of it is transferred to the root init process or to 
a root daemon process (system dependent).  The server may be configured 
to terminate orphaned user processes.  Terminated processes may be 
visible in the process listing for a time - at this point they are 
called "zombies" - but they aren't running.  Zombie processes eventually 
disappear, but the clean up period is configurable.


There is a command called "daemon" on some systems that will detach a 
user process from the starting terminal and allow it to keep running 
after log off.  However, the command may not be available if they don't 
want you to use it.  And if you are permitted to create daemon 
processes, understand that they will terminate when/if the server shuts 
down and will not be started again when the server reboots.



If you need your program to run whenever the server is running, you need 
root access to configure it as a service and to administer it later.   
You need to create an init.d script in  /etc/init.d  and configure the 
system to use it.  The major distros now all implement the Sys-V system  
for administering services, so the procedure is similar on every system.


Look in /etc/init.d for a simple script you can understand and modify.  
There may be an example script (sometimes called "skeleton") in the 
directory.  Copy and rename the script and edit it for your program.  
Minimally you need to implement "start", "stop" and "status" commands - 
the others are for interactive use.


Then you need to arrange for the script to be used.  On most systems 
this is done with "chkconfig".  On Ubuntu the command is "update-rc.d".


On the init.d script is installed and the system is configured to use 
it, you can administer your service using "//service  { 
start | stop | status }/*"*/


See service(8), chkconfig(8) and daemon(8)  in the man pages.  Also read 
about how to configure services for your particular distro.



Hope this helps,
George/
/

--
You received this message because you are subscribed to the Google Groups "Racket 
Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Re: racket execution

[Neil Van Dyke]

Everything George said.

Alternatively, if you are in a prototyping mode right now, you can just 
run your program from the command line in a detached `tmux` or `screen` 
session, which you can reattach when you want to mess with the server.  
You can also combine the tmux/screen with 
"http://www.neilvandyke.org/rackonsole/;, if you like that, but the 
important part is the detached and reattachable tmux/screen part.


But what George said is usually the best practice for single production 
servers, and often for multiple VM production provisioning.


Neil V.

--
You received this message because you are subscribed to the Google Groups "Racket 
Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[racket-users] Re: racket execution

[Héctor Mc]

El jueves, 3 de diciembre de 2015, 21:22:01 (UTC-5), Héctor Mc escribió:

Finally I could create a subsystem initialization script in /etc/init.d and the 
symbolic link with update-rc.d, and now this work. Thanks a everyone for your 
time.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Syntax checker suggestion

[Asumu Takikawa]

On 2015-12-04 08:02:40 -0800, brendan wrote:
> ...Y'know, let me concentrated my obvious noobness in one post :) and ask a
> silly question: why is "free-identifier=?" so named? It compares identifier
> bindings, which obviously implies that the identifiers are not "free" at all.
> I only got the hang of that one when I started mentally renaming it to
> "identifier-binding-site=?".

I agree that the name isn't great because it's technical jargon from
programming languages (PL).

It comes from how PL people refer to variables as "bound" or "free". In an
expression like (lambda (x) x) we say that x is bound. In an expression like
(+ 1 x) or (lambda (y) x) we say that x is free.

When you use free-identifier=?, you are comparing two identifiers to see if
they would refer to the same thing if you put them in an expression as free
references like above.

Cheers,
Asumu

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.