[racket-dev] managing packages
I hear that Racket is having some trouble determining who broke what in the package ecosystem. I do not know the specifics of this problem, but there was a recent discussion on the OCaml mailing list about OPAM's method of tracking package compatibility that may be relevant: http://lists.ocaml.org/pipermail/opam-devel/2014-September/000654.html In particular, the second message (of 26) in the thread has a link to a survey paper on the formal aspects of package systems. http://www.dicosmo.org/Articles/2012-DiCosmoTreinenZacchiroli-Fmco.pdf _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
On Sun, Jan 18, 2015 at 9:44 AM, Greg Hendershott greghendersh...@gmail.com wrote: Is there a similarly simple/standard way to disable contracts? I'd love a #lang like that. Never mind Tony Hoare's metaphor about sailing. For now, I'm attaching a small patch that'll disable contracts (as far as I can tell) on the current build; it's adapted from Leif's commits at [1]. ;; --- Please keep the bug reports coming! It looks like the built-in function expt isn't defined correctly: (module f racket (provide (contract-out [f (integer? . - . integer?)])) (define (f n) (expt n n))) Contract violation: 'f' violates 'expt'. Wrong arity An example module that breaks it: (module user racket (require (submid .. f)) (f 0)) (verification takes 0.035s) [1] https://github.com/LeifAndersen/racket/tree/no-conracts From e3a07fa756f47e0eb93be0811f245f1f814f028e Mon Sep 17 00:00:00 2001 From: ben ty...@ccs.neu.edu Date: Sun, 18 Jan 2015 18:51:48 -0500 Subject: [PATCH] imported leif's no-contract changes --- racket/collects/racket/contract/private/base.rkt | 7 +- .../collects/racket/contract/private/provide.rkt | 80 +++--- 2 files changed, 43 insertions(+), 44 deletions(-) diff --git a/racket/collects/racket/contract/private/base.rkt b/racket/collects/racket/contract/private/base.rkt index c7bb61c..cf0ca33 100644 --- a/racket/collects/racket/contract/private/base.rkt +++ b/racket/collects/racket/contract/private/base.rkt @@ -35,13 +35,10 @@ (define-syntax (contract stx) (syntax-case stx () [(_ c v pos neg name loc) - (syntax/loc stx - (apply-contract c v pos neg name loc))] + (syntax/loc stx v)] [(_ c v pos neg) (with-syntax ([name (syntax-local-infer-name stx)]) - (syntax/loc stx -(apply-contract c v pos neg 'name -(build-source-location #f] + (syntax/loc stx v))] [(_ c v pos neg src) (raise-syntax-error 'contract (string-append diff --git a/racket/collects/racket/contract/private/provide.rkt b/racket/collects/racket/contract/private/provide.rkt index 5356a64..b020493 100644 --- a/racket/collects/racket/contract/private/provide.rkt +++ b/racket/collects/racket/contract/private/provide.rkt @@ -350,42 +350,44 @@ (raise-syntax-error #f expected an identifier stx #'new-id)) (unless (identifier? #'orig-id) (raise-syntax-error #f expected an identifier stx #'orig-id)) - (define-values (pos-blame-party-expr srcloc-expr) -(let loop ([kwd-args (syntax-list #'(kwd-args ...))] - [pos-blame-party-expr #'(quote-module-path)] - [srcloc-expr #f]) - (cond -[(null? kwd-args) (values pos-blame-party-expr - (or srcloc-expr (stx-srcloc-expr stx)))] -[else - (define kwd (car kwd-args)) - (cond - [(equal? (syntax-e kwd) '#:pos-source) -(when (null? (cdr kwd-args)) - (raise-syntax-error #f expected a keyword argument to follow #:pos-source - stx)) -(loop (cddr kwd-args) - (cadr kwd-args) - srcloc-expr)] - [(equal? (syntax-e kwd) '#:srcloc) -(when (null? (cdr kwd-args)) - (raise-syntax-error #f expected a keyword argument to follow #:srcloc - stx)) -(loop (cddr kwd-args) - pos-blame-party-expr - (cadr kwd-args))] - [else -(raise-syntax-error #f expected either the keyword #:pos-source of #:srcloc -stx -(car kwd-args))])]))) - (internal-function-to-be-figured-out #'ctrct - #'orig-id - #'orig-id - #'new-id - #'new-id - srcloc-expr - 'define-module-boundary-contract - pos-blame-party-expr))])])) + (define new-id orig-id) + ;; (define-values (pos-blame-party-expr srcloc-expr) + ;; (let loop ([kwd-args (syntax-list #'(kwd-args ...))] + ;; [pos-blame-party-expr #'(quote-module-path)] + ;; [srcloc-expr #f]) + ;; (cond + ;; [(null? kwd-args) (values pos-blame-party-expr + ;; (or srcloc-expr (stx-srcloc-expr stx)))] + ;; [else + ;;(define kwd (car
Re: [racket-dev] Announcing Soft Contract Verification tool
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 x))) (define (divides? a b) (cond [(= 0 b) #t] [( b a) #f] [else (divides? a (- b a))])) ) On Thu, Jan 15, 2015 at 3:14 PM, David Van Horn dvanh...@cs.umd.edu wrote: 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 coming in here. Can you explain more? On further inspection, the counterexample is wrong. (There are counterexamples due to the model of =/c, but the one that reported is not an actual one.) This will be fixed shortly. David _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] A proposal for parametric opaque types in Typed Racket
This has bothered me too, but I've realized that I was on the wrong track. The string a and symbol 'b are not different types. A struct (Foo a 'b), or (list a 'b), is a homogeneous data structure of type (U String Symbol) just like Alexander said. This really upsets me -- I like the Hindley Milner world where the compiler warns me if I make a list [1, two] and forces me to wrap the int and string into a new datatype. But Typed Racket is not HM. About the proposal, I'm confused about what the syntax in Section 2.1 should do -- what is a first class member of Typed Racket's type system? - Should an A only be a base type like String or Symbol - Do you mean to infer the type of the first thing put into the struct as the exact type for everything else? - Would first class members prevent me from filling a struct with members of (define-type (Option A) (U 'None (Some A))), where Some is a struct with one field? I totally agree that something needs fixing, but I'm not sure what. On Thu, Jan 29, 2015 at 10:13 PM, Alexis King lexi.lam...@gmail.com wrote: Or Any for that matter. I know. The fact that it could be literally anything was sort of the point. On Jan 29, 2015, at 19:10, Alexander D. Knauth alexan...@knauth.org wrote: Um, for this: (module http://docs.racket-lang.org/reference/module.html#%28form._%28%28quote._~23~25kernel%29._module%29%29 typed typed/racket/base(provide http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._provide%29%29 (struct-out http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._struct-out%29%29 Foo))(struct http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._struct%29%29 [A] Foo ([x : http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._~3a%29%29 A] [y : http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._~3a%29%29 A]) #:transparent)) (Foo a 'b) Should be fine because Foo could be instantiated at the type (U String Symbol). On Jan 29, 2015, at 9:25 PM, Alexis King lexi.lam...@gmail.com wrote: I recently ran into a problem in which opaque types (types imported from untyped code) cannot by parameterized by Typed Racket. I initially encountered this problem in my attempt to port 2htdp/image to TR https://github.com/lexi-lambda/racket-2htdp-typed/issues/1. After some further consideration, I’m interested in adding support to make something like this possible, which would certainly have additional benefits beyond this specific use-case. I’ve outlined my proposal here: http://lexi-lambda.github.io/racket-parametric-opaque-types/ Any feedback, suggestions, or advice would be appreciated, especially from those who are familiar with Typed Racket’s internals. Thank you, Alexis _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
