<div dir="ltr">That is a bug in redex-check. You can work around it by passing #:ad-hoc to redex-check (this goes back to the old behavior).<div><br></div><div>Robby</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">
On Wed, Mar 26, 2014 at 6:33 PM, Stephen Chang <span dir="ltr"><<a href="mailto:stchang@ccs.neu.edu" target="_blank">stchang@ccs.neu.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Not sure if this is related, but if I have a call to redex-check that<br>
is suddenly producing the error:<br>
<br>
generate-term: #:i-th does not support "side-condition" patterns<br>
<br>
What are some possible causes? (still trying to distill to a small example).<br>
<div class="im HOEnZb"><br>
On Wed, Mar 26, 2014 at 1:10 PM, Robby Findler<br>
<<a href="mailto:robby@eecs.northwestern.edu">robby@eecs.northwestern.edu</a>> wrote:<br>
</div><div class="HOEnZb"><div class="h5">> Just to confirm: Redex isn't doing anything wrong, right?<br>
><br>
> Redex is now using the in-order enumeration generation in a default<br>
> configuration (for a little while before adding some of the old-style random<br>
> generated terms).<br>
><br>
> So if you want to see what kinds of things it generates, you can use<br>
> generate-term with the #:i-th argument.<br>
><br>
> Robby<br>
><br>
><br>
><br>
> On Wed, Mar 26, 2014 at 12:03 PM, Eric Dobson <<a href="mailto:eric.n.dobson@gmail.com">eric.n.dobson@gmail.com</a>><br>
> wrote:<br>
>><br>
>> Looks like what is actually happening is that redex is actually<br>
>> generating reals for this program now.<br>
>><br>
>> #lang racket<br>
>><br>
>> (require redex/reduction-semantics)<br>
>> (define-language tr-arith<br>
>> [n real])<br>
>><br>
>> (redex-check tr-arith n #t<br>
>> #:prepare (lambda (x) (displayln x) x))<br>
>><br>
>> Before we were only getting small integers.<br>
>><br>
>> On Wed, Mar 26, 2014 at 9:46 AM, Eric Dobson <<a href="mailto:eric.n.dobson@gmail.com">eric.n.dobson@gmail.com</a>><br>
>> wrote:<br>
>> > This push has started breaking the random TR tests. I think the issue<br>
>> > is that TR assumed that redex wouldn't generate so large numbers that<br>
>> > it exceeded the flonum range. Could that have changed in this commit?<br>
>> > Or changed so that were generated earlier in random testing? If so the<br>
>> > issue is definitely on the TR side, but just want to confirm that the<br>
>> > theory is likely.<br>
>> ><br>
>> > On Wed, Mar 26, 2014 at 4:58 AM, <<a href="mailto:drdr@racket-lang.org">drdr@racket-lang.org</a>> wrote:<br>
>> >> DrDr has finished building push #28413 after 1.20h.<br>
>> >><br>
>> >> <a href="http://drdr.racket-lang.org/28413/" target="_blank">http://drdr.racket-lang.org/28413/</a><br>
>> >><br>
>> >> A file you are responsible for has a condition that may need<br>
>> >> inspecting.<br>
>> >> stderr:<br>
>> >><br>
>> >> <a href="http://drdr.racket-lang.org/28413/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/tr-random-testing.rkt" target="_blank">http://drdr.racket-lang.org/28413/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/tr-random-testing.rkt</a><br>
>> >><br>
>> >> unclean:<br>
>> >><br>
>> >> <a href="http://drdr.racket-lang.org/28413/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/tr-random-testing.rkt" target="_blank">http://drdr.racket-lang.org/28413/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/tr-random-testing.rkt</a><br>
>> >><br>
>> >><br>
><br>
><br>
><br>
</div></div><div class="HOEnZb"><div class="h5">> _________________________<br>
> Racket Developers list:<br>
> <a href="http://lists.racket-lang.org/dev" target="_blank">http://lists.racket-lang.org/dev</a><br>
><br>
</div></div></blockquote></div><br></div>