Re: [racket-users] [Redex] "Got nothing"
Dear Robby, Thank you. Yes, the cycles were a problem. BR, Anton Podkopaev podkopaev.net On Wed, Mar 9, 2016 at 1:50 AM, Robby Findler wrote: > It is possible you're using the #:cycles-ok argument, as in the > program below? If so, that means that the reduction graph has no > irreducible terms. So you would need to pass no "expected" arguments > to test-->> in order for the test case to pass. > > Robby > > #lang racket > (require redex/reduction-semantics) > > (define-language L > (e ::= (loop))) > > (define red > (reduction-relation >L >(--> (loop) (loop > > (test-->> red #:cycles-ok (term (loop)) 5) > > > On Tue, Mar 8, 2016 at 12:03 PM, Anton Podkopaev > wrote: > > Dear colleagues, > > > > I'm working on a semantics using Redex. > > I've got a strange message from "test-->>" function --- "got nothing". > > It is strange, because a term, which I run "test-->>" on, definitely can > be > > reduced. > > For example, I can see lots of its productions in "traces" or "stepper". > > > > My assumption, that in Redex there is some bound (parameter?) on how many > > productions in a trace chain can be. Am I right? Unfortunately, I failed > to > > find > > corresponding information in the Redex reference. > > > > BR, > > Anton Podkopaev > > podkopaev.net > > > > -- > > 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.
[racket-users] [Redex] "Got nothing"
Dear colleagues, I'm working on a semantics using Redex. I've got a strange message from "test-->>" function --- "got nothing". It is strange, because a term, which I run "test-->>" on, definitely can be reduced. For example, I can see lots of its productions in "traces" or "stepper". My assumption, that in Redex there is some bound (parameter?) on how many productions in a trace chain can be. Am I right? Unfortunately, I failed to find corresponding information in the Redex reference. BR, Anton Podkopaev podkopaev.net -- 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] Macros for custom -->
Dear Robby, Thank you for the response. It is what I expected. I think for current goal typesetting isn't that important, so I'll define a macro for reduction-relation. Thank you a lot, Anton BR, Anton Podkopaev podkopaev.net On Thu, Feb 25, 2016 at 3:41 PM, Robby Findler wrote: > reduction-relation doesn't expand its body, it just looks at it and > processes it. So if you write: > > #lang racket > (require redex) > > (define-language L > (E ::= (list v ... E e ...) (car E) (cdr E) hole) > (v ::= (list v ...) natural) > (e ::= (list e ...) (car e) (cdr e) natural)) > > (define-syntax-rule (==> a b) (--> (in-hole E a) (in-hole E b))) > > (define red > (reduction-relation >L >(==> (car (list v_1 v_2 ...)) v_1) >(==> (cdr (list v_1 v_2 ...)) (list v_2 ... > > (test-->> red > (term (list (car (cdr (cdr (cdr (list 0 1 2 3 4))) > (term (list 3))) > > > then redex is going to ignore your macro definition. > > In general, redex doesn't work well with macros like this because of > typesetting reasons. But if you don't want to typeset the model, then > you can use a macro that expands into the entire reduction-relation. > (I recommend typesetting not because it is beautiful enough (yet) but > because it avoids errors in transcription later when you publish your > model.) > > For the specific example above and maybe in you use-case, you can use > 'with', removing the define-syntax-rule and writing this definition of > red instead: > > (define red > (reduction-relation >L >(==> (car (list v_1 v_2 ...)) v_1) > (==> (cdr (list v_1 v_2 ...)) (list v_2 ...)) >with >[(--> (in-hole E a) (in-hole E b)) > (==> a b)])) > > Robby > > > On Thu, Feb 25, 2016 at 6:13 AM, Anton Podkopaev > wrote: > > Dear colleagues, > > > > I'm working on a semantics in Redex, which reduction rules have a lot in > > common. > > To reduce duplicate code I want to define a macros (say `==>`) for > reduction > > rule definition. > > Unfortunately, I haven't managed to do that: > > I've got "reduction-relation: the ==> relation is not defined". > > Could anyone help me with it? > > > > BR, > > Anton Podkopaev > > podkopaev.net > > > > -- > > 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.
[racket-users] [Redex] Macros for custom -->
Dear colleagues, I'm working on a semantics in Redex, which reduction rules have a lot in common. To reduce duplicate code I want to define a macros (say `==>`) for reduction rule definition. Unfortunately, I haven't managed to do that: I've got "reduction-relation: the ==> relation is not defined". Could anyone help me with it? BR, Anton Podkopaev podkopaev.net -- 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] test-->>E and trace
Robby, Thank you very much! BR, Anton Podkopaev BR, Anton Podkopaev On Wed, Feb 10, 2016 at 4:34 PM, Anton Podkopaev wrote: > Robby, > > Thank you very much! > > BR, > Anton Podkopaev > > On Wed, Feb 10, 2016 at 3:50 PM, Robby Findler < > ro...@eecs.northwestern.edu> wrote: > >> Sure. The trick is to use the #:reduce argument and then just ignore >> the actual reduction relation. A revision of the earlier code >> demonstrates, as below. >> >> Robby >> >> #lang racket >> >> (require redex) >> >> (define-language L (n ::= natural)) >> (define red >> (reduction-relation >>L >>(--> n ,(max 0 (min 20 (+ (term n) 3 >>(--> n ,(max 0 (min 20 (- (term n) 1)) >> >> (define (find-path red from to) >> (define parents (make-hash)) >> (let/ec done >> (let loop ([t from]) >> (define nexts (apply-reduction-relation red t)) >> (for ([next (in-list (remove-duplicates nexts))]) >> (cond >> [(equal? next to) >>(hash-set! parents to t) >>(done)] >> [(hash-ref parents next #f) >>(void)] >> [else >>(hash-set! parents next t) >>(loop next)] >> parents) >> >> (define parents (find-path red 0 10)) >> (define children >> (for/hash ([(k v) (in-hash parents)] >> #:unless (equal? k 0)) >> (values v k))) >> >> (traces red 0 >> #:reduce >> (λ (_ t) >> (let/ec k >> (list (list #f (hash-ref children t (λ () (k '() >> >> On Wed, Feb 10, 2016 at 4:08 AM, Anton Podkopaev >> wrote: >> > Robby, >> > >> > Thank you, it mostly works for my semantics, and I know how to change >> the >> > algorithm for some corner cases. >> > >> > Then I have one more question --- then I get terms (a result of >> > `find-path'), is there a way to show them (and only them) using GUI >> tools >> > like `traces' and `stepper'? >> > >> > >> > >> > BR, >> > Anton Podkopaev >> > >> > On Wed, Feb 10, 2016 at 2:42 AM, Robby Findler < >> ro...@eecs.northwestern.edu> >> > wrote: >> >> >> >> I'm sorry it took me so long to get back to this. I'm not sure there >> >> is a good thing to be added to Redex for this problem. Overall, it >> >> seems like a graph search problem and there are multiple different >> >> strategies depending on properties of the graph that you're searching. >> >> It's not too hard to code these up in Racket and then find the best >> >> one for your task, I would say. And redex's current support is pretty >> >> simplistic, tailored to models with much less interesting reduction >> >> graphs than yours has, I think. >> >> >> >> If you find what seems to be a particularly useful and general purpose >> >> search strategy and want it to be included in Redex, I'd be delighted >> >> if you would make a pull request. In the meantime, I've offered one >> >> that may or may not work well for your model, below. >> >> >> >> hth, >> >> Robby >> >> >> >> #lang racket >> >> (require redex/reduction-semantics) >> >> (define-language L (n ::= natural)) >> >> (define red >> >> (reduction-relation >> >>L >> >>(--> n ,(max 0 (min 20 (+ (term n) 3)))) >> >>(--> n ,(max 0 (min 20 (- (term n) 1)) >> >> >> >> (define (find-path red from to) >> >> (define parents (make-hash)) >> >> (let/ec done >> >> (let loop ([t from]) >> >> (define nexts (apply-reduction-relation red t)) >> >> (for ([next (in-list (remove-duplicates nexts))]) >> >> (cond >> >> [(equal? next to) >> >>(hash-set! parents to t) >> >> (done)] >> >> [(hash-ref parents next #f) >> >>(void)] >> >> [else >> >>(hash-set! parents next t) >> >> (loop next)] >> >> (let loop ([term to]) >> >> (cond >> >> [(equal? term from) (list from)] >> >> [else (cons
Re: [racket-users] [Redex] test-->>E and trace
Robby, Thank you, it mostly works for my semantics, and I know how to change the algorithm for some corner cases. Then I have one more question --- then I get terms (a result of `find-path'), is there a way to show them (and only them) using GUI tools like `traces' and `stepper'? BR, Anton Podkopaev On Wed, Feb 10, 2016 at 2:42 AM, Robby Findler wrote: > I'm sorry it took me so long to get back to this. I'm not sure there > is a good thing to be added to Redex for this problem. Overall, it > seems like a graph search problem and there are multiple different > strategies depending on properties of the graph that you're searching. > It's not too hard to code these up in Racket and then find the best > one for your task, I would say. And redex's current support is pretty > simplistic, tailored to models with much less interesting reduction > graphs than yours has, I think. > > If you find what seems to be a particularly useful and general purpose > search strategy and want it to be included in Redex, I'd be delighted > if you would make a pull request. In the meantime, I've offered one > that may or may not work well for your model, below. > > hth, > Robby > > #lang racket > (require redex/reduction-semantics) > (define-language L (n ::= natural)) > (define red > (reduction-relation >L >(--> n ,(max 0 (min 20 (+ (term n) 3 >(--> n ,(max 0 (min 20 (- (term n) 1)) > > (define (find-path red from to) > (define parents (make-hash)) > (let/ec done > (let loop ([t from]) > (define nexts (apply-reduction-relation red t)) > (for ([next (in-list (remove-duplicates nexts))]) > (cond > [(equal? next to) >(hash-set! parents to t) >(done)] > [(hash-ref parents next #f) >(void)] > [else >(hash-set! parents next t) >(loop next)] > (let loop ([term to]) > (cond > [(equal? term from) (list from)] > [else (cons term (loop (hash-ref parents term)))]))) > > (find-path red 0 10) > > > On Sun, Dec 20, 2015 at 6:26 AM, Anton Podkopaev > wrote: > > Unfortunately, I need something else, because my semantics is highly > > non-deterministic, and I want to be able to see only paths, which lead > to a > > certain term. > > > > BR, > > Anton Podkopaev > > > > 2015-12-18 20:49 GMT+03:00 Robby Findler : > >> > >> I think you may want to call apply-reduction-relation* with a > >> #:stop-when argument instead? > >> > >> Robby > >> > >> > >> On Fri, Dec 18, 2015 at 5:33 AM, Anton Podkopaev > >> wrote: > >> > Hello, colleagues! > >> > > >> > Is there any way to get a term trace from successful test-->>E in > Redex? > >> > > >> > BR, > >> > 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] [Redex] test-->>E and trace
Unfortunately, I need something else, because my semantics is highly non-deterministic, and I want to be able to see only paths, which lead to a certain term. BR, Anton Podkopaev 2015-12-18 20:49 GMT+03:00 Robby Findler : > I think you may want to call apply-reduction-relation* with a > #:stop-when argument instead? > > Robby > > > On Fri, Dec 18, 2015 at 5:33 AM, Anton Podkopaev > wrote: > > Hello, colleagues! > > > > Is there any way to get a term trace from successful test-->>E in Redex? > > > > BR, > > 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.
[racket-users] [Redex] test-->>E and trace
Hello, colleagues! Is there any way to get a term trace from successful test-->>E in Redex? BR, 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.
Re: [racket-users] Redex Engine Internals
>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, it's really interesting. Thank you! BR, Anton Podkopaev 2015-12-04 20:05 GMT+03:00 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 >> <https://github.com/anlun/OperationalSemanticsC11>, but they are here >> <https://github.com/anlun/OperationalSemanticsC11/blob/master/test%2FrelAcqNaRlxPost_t1.rkt> >> : >> - `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 Ra
Re: [racket-users] Redex Engine Internals
> I think you want to do this: > (current-cache-all? #t) Thank you, Robby! It mostly solves my problems. BR, Anton Podkopaev 2015-12-04 20:33 GMT+03:00 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 tri
Re: [racket-users] Redex Engine Internals
> 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 <https://github.com/anlun/OperationalSemanticsC11>, but they are here <https://github.com/anlun/OperationalSemanticsC11/blob/master/test%2FrelAcqNaRlxPost_t1.rkt> : - `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 > >> versi
Re: [racket-users] Redex Engine Internals
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.
[racket-users] Redex Engine Internals
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.
[racket-users] Redex, Tests, and Travis
Hello! I'm trying to use a build server (Travis) with my Redex project. It compiles without errors, but for all test files a `raco test` returns Gtk initialization failed for display ":0" context...: /usr/racket/share/pkgs/gui-lib/mred/private/wx/gtk/queue.rkt: [running body] /usr/racket/share/pkgs/gui-lib/mred/private/wx/gtk/init.rkt: [traversing imports] /usr/racket/share/pkgs/gui-lib/mred/private/mred.rkt: [traversing imports] There are no 'stepper' or 'traces' commands. I was using #lang racket/gui in one file, but commenting it out hasn't solved the situation. Is there anything what I can do about this problem? BR, 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.
Re: [racket-users] Redex, traces and Graphviz
Robby, thank you very much!
BR,
Anton Podkopaev
2015-09-23 23:48 GMT+03:00 Robby Findler :
> Yes, but only in a fairly complex way. Your rendering function would
> have to call out to graphviz, get the results back as a png, use
> read-bitmap to get the png back into Racket, create an image snip and
> then insert that into the editor, using the more complex version of
> the `pp` argument.
>
> Here's an example.
>
> Robby
>
> #lang racket/gui
>
> (define (dot-render t)
> (define-values (dot-input-in dot-input-out) (make-pipe))
> (define-values (dot-output-in dot-output-out) (make-pipe))
> (thread
>(λ ()
> (define n 0)
> (define (next) (set! n (+ n 1)) (format "x~a" n))
> (fprintf dot-input-out "digraph {\n")
> (let loop ([t t])
> (define me (next))
> (match t
> [`(,e1 ,e2 ,e3)
>(fprintf dot-input-out " ~a [label=\"\" width=.2 height=.2]\n"
> me)
>(fprintf dot-input-out " ~a -> ~a\n" me (loop e1))
>(fprintf dot-input-out " ~a -> ~a\n" me (loop e2))
>(fprintf dot-input-out " ~a -> ~a\n" me (loop e3))
>me]
> [_
>(fprintf dot-input-out " ~a [shape=point]\n" me)
>me]))
> (fprintf dot-input-out "}\n")
> (close-output-port dot-input-out)))
> (thread (λ ()
> (parameterize ([current-output-port dot-output-out]
>[current-input-port dot-input-in])
> (system "/usr/local/bin/dot -T png"))
> (close-output-port dot-output-out)))
> (read-bitmap dot-output-in))
>
> (require redex)
> (define-language L
> (e ::= (e e e) ⊥))
> (define red
> (reduction-relation
>L
> (--> e (e ⊥ ⊥))
>(--> e (⊥ e ⊥))
>(--> e (⊥ ⊥ e
>
> (traces red
> (term ⊥)
> #:pp
> (λ (t port n txt)
> (send txt insert (make-object image-snip% (dot-render t)
>
>
>
> On Wed, Sep 23, 2015 at 12:05 PM, Anton Podkopaev
> wrote:
> > Hello!
> >
> > I'm working on an operational semantics using PLT Redex. I use `traces`
> a lot to debug my semantics. To represent states in a nice way I'm using a
> pretty printer, but I want more -- I want to use Graphviz. Is it somehow
> possible to call Graphviz from my pretty printer, and incorporate a result
> of rendering into a pretty-printed text?
> >
> > BR,
> > 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.
[racket-users] Redex, traces and Graphviz
Hello! I'm working on an operational semantics using PLT Redex. I use `traces` a lot to debug my semantics. To represent states in a nice way I'm using a pretty printer, but I want more -- I want to use Graphviz. Is it somehow possible to call Graphviz from my pretty printer, and incorporate a result of rendering into a pretty-printed text? BR, 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.
