On Jan 15, 2015, at 11:13 AM, David Van Horn dvanh...@cs.umd.edu wrote:
On 1/15/15, 11:04 AM, Matthias Felleisen wrote:
Well that got me all excited. So I tried to get the sample module
to pass the verification step -- until I realized how restricted
the grammar is!
(module f racket
On 1/15/15, 11:27 AM, Matthias Felleisen wrote:
Argh, I wanted the other way (negative). I always get the
directions confused. Sorry.
Right -- using (and/c real? (/c 0)) will also make this verify.
Thanks for trying it out!
David
On Jan 15, 2015, at 11:26 AM, David Van Horn
FWIW, (/c 0) already implies real?.
Robby
On Thu, Jan 15, 2015 at 10:30 AM, David Van Horn dvanh...@cs.umd.edu wrote:
On 1/15/15, 11:27 AM, Matthias Felleisen wrote:
Argh, I wanted the other way (negative). I always get the
directions confused. Sorry.
Right -- using (and/c real? (/c 0))
On 1/15/15, 11:04 AM, Matthias Felleisen wrote:
Well that got me all excited. So I tried to get the sample module
to pass the verification step -- until I realized how restricted
the grammar is!
(module f racket (provide (contract-out [f (real? . - .
integer?)])) (define (f n) (/ 1 (- 100
On 1/15/15, 11:17 AM, Matthias Felleisen wrote:
On Jan 15, 2015, at 11:13 AM, David Van Horn dvanh...@cs.umd.edu
wrote:
On 1/15/15, 11:04 AM, Matthias Felleisen wrote:
Well that got me all excited. So I tried to get the sample
module to pass the verification step -- until I realized
On 2015-01-15 14:13:02 -0500, Asumu Takikawa wrote:
Contract violation: 'fact' violates '='.
Value
0.105
violates predicate
real?
An example module that breaks it:
(module user racket (require (submod .. fact)) (factorial 0.105))
(Verification takes 0.05s)
Hmm,
I think this is saying that the result is going to be negative. (But
it won't, since it doesn't terminate.)
Robby
On Thu, Jan 15, 2015 at 1:13 PM, Asumu Takikawa as...@ccs.neu.edu wrote:
On 2015-01-14 19:11:59 -0500, David Van Horn wrote:
If you have questions, comments, bugs, or any other
On 2015-01-14 19:11:59 -0500, David Van Horn wrote:
If you have questions, comments, bugs, or any other feedback, let us
know, or just file bug reports on the GitHub source code.
Nice tool! I like the web interface too.
I was confused by this interaction though. Clicking verify on this:
Can you randomly make up programs from your grammar, get example
errors from the tool, and then run those programs to see if you find
bugs in the analysis like that one?
That said, I don't see how the bug in =/c is coming in here. Can you
explain more?
Robby
On Thu, Jan 15, 2015 at 1:42 PM,
As an update, I’ve made a bit more progress on this. I’ve implemented an
impersonate-async-channel function, and I’ve actually included this in the
exports from racket/contract. I also realized the blame information is correct,
it works fine. Most of the other issues remain, as well as a few
Sorry, I wasn’t clear. The chaperone/impersonate-async-channel functions are
exported from racket/async-channel. The async-channel contracts, however, are
exported from racket/contract.
On Jan 15, 2015, at 14:41, Robby Findler ro...@eecs.northwestern.edu wrote:
Just a small nit: why export
I think they should probably all be exported from racket/async-channel.
Unless there is some reason to modify the internals of racket/contract
to support them?
Robby
On Thu, Jan 15, 2015 at 4:50 PM, Alexis King lexi.lam...@gmail.com wrote:
Sorry, I wasn’t clear. The
Just a small nit: why export that function from racket/contract and
not an async-channel library?
Robby
On Thu, Jan 15, 2015 at 3:33 PM, Alexis King lexi.lam...@gmail.com wrote:
As an update, I’ve made a bit more progress on this. I’ve implemented an
impersonate-async-channel function, and
On Thu, Jan 15, 2015 at 4:33 PM, Alexis King lexi.lam...@gmail.com wrote:
As an update, I’ve made a bit more progress on this. I’ve implemented an
impersonate-async-channel function, and I’ve actually included this in the
exports from racket/contract. I also realized the blame information is
Yes, I see some of this at the bottom of the chapter 16 in the guide, and
the recursion supported with
(require
http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._require%29%29
(for-meta
Sure thing, done. I’ve moved everything into racket/async-channel, added the
missing functions, and added some tests. I squashed my commits into one, and
the result is here:
https://github.com/lexi-lambda/racket/commit/0074ba13b712a87c9d05948ae075bcd74c7651e7
Warning I am still a Racket intermediate user but I've been studying
syntactic extensions a lot the past several months.
The problem here is macros in Racket have lexical scope just like
procedures, they are hygienic macros. The identifiers you introduced in the
with-tables macro only exist or
But I think it’s important that it doesn’t use gensym or something like that,
it uses syntax-marks, which means you can break these lexical scoping rules if
you want/need to by using either syntax-local-introduce or datum-syntax:
#lang racket
(require syntax/parse/define)
(define-simple-macro
On 1/15/15, 2:13 PM, Asumu Takikawa wrote:
On 2015-01-14 19:11:59 -0500, David Van Horn wrote:
If you have questions, comments, bugs, or any other feedback, let
us know, or just file bug reports on the GitHub source code.
Nice tool! I like the web interface too.
I was confused by this
On 1/15/15, 2:48 PM, Robby Findler wrote:
Can you randomly make up programs from your grammar, get example
errors from the tool, and then run those programs to see if you
find bugs in the analysis like that one?
Yes, we're planning to do this.
That said, I don't see how the bug in =/c is
Thank you for that nice explanation. I'm reminded of the scope variables
carried in Ruby. In Mathematica the renaming of module variables is
explicit. There do not appear to be run phases there. Also thanks for the
working example using syntax parse. Thus far I have working examples using
I tried writing a small program, but got stuck pretty early on. When I try
verifying the divides? function below, the tool times out. What's
happening?
(module div racket
(provide (contract-out [divides? (- positive? positive? boolean?)]))
(define (positive? x)
(and (integer? x) (= 0
22 matches
Mail list logo
