Re: [racket-dev] Announcing Soft Contract Verification tool

2015-01-18 Thread Benjamin Greenman
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

2015-01-18 Thread Greg Hendershott
This looks really exciting!

Imagining using this reminds me of something.

Typed Racket has a simple/standard way to disable type-checking (while
retaining the type declarations for documentation value as well as
potential re-enabling): #lang typed/racket/no-check and #lang
typed/racket/base/no-check.

Is there a similarly simple/standard way to disable contracts?

Last I checked, I couldn't find one. So I think we each write our own
my-define/contract and my-contract-out sort of macros? It's not
difficult. But it's idiosyncratic. Also: tools.

Why not e.g. #lang racket/no-check, and a racket/contract/no-check to
require for use with #lang racket/base?

Although I guess a tool like SCV is more in the business of disabling
individual contracts; not so much whole-file granularity?
_
  Racket Developers list:
  http://lists.racket-lang.org/dev