From a7b551f8ac1e8910ea615ed2e400c544dee8c04b Mon Sep 17 00:00:00 2001 From: Emina Torlak Date: Wed, 3 Feb 2021 10:53:56 -0800 Subject: [PATCH] Enable the updated parts of the doc to be built from the command line. --- .../scribble/essentials/essentials-log.txt | 100 +++++++------- .../scribble/essentials/essentials.scrbl | 2 +- .../scribble/forms/rosette-forms-log.txt | 126 ++++++++++-------- rosette/guide/scribble/rosette-guide.scrbl | 14 +- 4 files changed, 125 insertions(+), 117 deletions(-) diff --git a/rosette/guide/scribble/essentials/essentials-log.txt b/rosette/guide/scribble/essentials/essentials-log.txt index 2fe084d9..c94a49de 100644 --- a/rosette/guide/scribble/essentials/essentials-log.txt +++ b/rosette/guide/scribble/essentials/essentials-log.txt @@ -3,7 +3,7 @@ (b ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -17,7 +17,7 @@ ((vector b 1) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -29,7 +29,7 @@ ((not b) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -52,7 +52,7 @@ ((eq? (dynamic) (dynamic)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -68,7 +68,7 @@ ((eq? (static) (yet-another-x)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -86,7 +86,7 @@ ((spec-asserts (vc)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -106,7 +106,7 @@ ((spec-assumes (vc)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -119,7 +119,7 @@ ((spec-asserts (vc)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -143,7 +143,7 @@ ((int32 1) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -192,7 +192,7 @@ (cex ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -209,7 +209,7 @@ ((list cl ch) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -234,7 +234,7 @@ (m ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -248,7 +248,7 @@ ((int32 (quotient (+ il ih) 2)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -262,7 +262,7 @@ ((bvadd cl ch) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -285,7 +285,7 @@ ((verify (check-mid bvmid-no-overflow l h)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -303,7 +303,7 @@ ((3) 0 () 0 () () (c values c (void))) #"" #"") -((require (only-in "bvmid.rkt" bvmid-fast)) +((require (only-in rosette/guide/scribble/essentials/bvmid bvmid-fast)) ((3) 0 () 0 () () (c values c (void))) #"" #"") @@ -319,7 +319,7 @@ (sol ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -356,7 +356,7 @@ (sol ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -371,7 +371,7 @@ ((evaluate (bvand l h) sol) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -383,7 +383,7 @@ ((evaluate (bvmid-fast l h) sol) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -412,7 +412,7 @@ ((time (verify (check-mid bvmid l h))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -422,12 +422,12 @@ values c (0 (u . "(model\n [l (bv #x394f0402 32)]\n [h (bv #x529e7c00 32)])")))) - #"cpu time: 2 real time: 38 gc time: 0\n" + #"cpu time: 1 real time: 38 gc time: 0\n" #"") ((time (verify (check-mid-slow bvmid l h))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -437,19 +437,19 @@ values c (0 (u . "(model\n [l (bv #x2faef9a1 32)]\n [h (bv #x5eefb8dd 32)])")))) - #"cpu time: 15 real time: 171 gc time: 0\n" + #"cpu time: 4 real time: 183 gc time: 0\n" #"") ((time (verify (check-mid bvmid-no-overflow l h))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 () () (c values c (0 (u . "(unsat)")))) - #"cpu time: 5 real time: 155 gc time: 0\n" + #"cpu time: 1 real time: 159 gc time: 0\n" #"") ((error 'call-with-deep-time-limit "out of time") ((3) 0 () 0 () () (q exn "call-with-deep-time-limit: out of time")) @@ -460,7 +460,7 @@ ((time (verify (check-mid-slow bvmid l h))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -470,25 +470,25 @@ values c (0 (u . "(model\n [l (bv #x00000001 32)]\n [h (bv #x7fffffff 32)])")))) - #"cpu time: 2 real time: 24 gc time: 0\n" + #"cpu time: 3 real time: 24 gc time: 0\n" #"") ((time (verify (check-mid-slow bvmid-no-overflow l h))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 () () (c values c (0 (u . "(unsat)")))) - #"cpu time: 5 real time: 155 gc time: 0\n" + #"cpu time: 1 real time: 159 gc time: 0\n" #"") ((current-bitwidth 32) ((3) 0 () 0 () () (c values c (void))) #"" #"") ((time (verify (check-mid-slow bvmid l h))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -500,7 +500,7 @@ ((time (verify (check-mid-slow bvmid-no-overflow l h))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -510,13 +510,13 @@ values c (0 (u . "(model\n [l (bv #x71979fa3 32)]\n [h (bv #x76b91b88 32)])")))) - #"cpu time: 11 real time: 149 gc time: 0\n" + #"cpu time: 1 real time: 151 gc time: 0\n" #"") ((current-bitwidth 512) ((3) 0 () 0 () () (c values c (void))) #"" #"") ((time (verify (check-mid-slow bvmid l h))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -526,19 +526,19 @@ values c (0 (u . "(model\n [l (bv #x70000006 32)]\n [h (bv #x73fffffa 32)])")))) - #"cpu time: 29 real time: 380 gc time: 19\n" + #"cpu time: 1 real time: 381 gc time: 0\n" #"") ((time (verify (check-mid-slow bvmid-no-overflow l h))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 () () (c values c (0 (u . "(unsat)")))) - #"cpu time: 20 real time: 426 gc time: 0\n" + #"cpu time: 1 real time: 438 gc time: 0\n" #"") ((current-bitwidth #f) ((3) 0 () 0 () () (c values c (void))) #"" #"") ((require rosette/solver/smt/z3) @@ -552,7 +552,7 @@ ((time (verify (check-mid bvmid l h))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -562,7 +562,7 @@ values c (0 (u . "(model\n [l (bv #x394f0402 32)]\n [h (bv #x529e7c00 32)])")))) - #"cpu time: 245 real time: 288 gc time: 0\n" + #"cpu time: 5 real time: 36 gc time: 0\n" #"") ((time (verify (check-mid-slow bvmid l h))) ((3) @@ -591,7 +591,7 @@ ((bvsqrt (int32 3)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -603,7 +603,7 @@ ((bvsqrt (int32 4)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -615,7 +615,7 @@ ((bvsqrt (int32 15)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -627,7 +627,7 @@ ((bvsqrt (int32 16)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -644,7 +644,7 @@ (n ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -660,7 +660,7 @@ (n ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -676,7 +676,7 @@ (n ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -695,7 +695,7 @@ (n ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -749,7 +749,7 @@ #"") ((define cex (time (verify (check-sqrt bvsqrt l)))) ((3) 0 () 0 () () (c values c (void))) - #"cpu time: 283 real time: 1256 gc time: 0\n" + #"cpu time: 6 real time: 1039 gc time: 0\n" #"") ((bvsqrt (evaluate l cex)) ((3) 0 () 0 () () (q exn "[assert] Out of fuel.")) @@ -760,12 +760,12 @@ ((time (verify (check-sqrt bvsqrt l))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 () () (c values c (0 (u . "(unsat)")))) - #"cpu time: 1961 real time: 68196 gc time: 60\n" + #"cpu time: 15 real time: 69086 gc time: 10\n" #"") diff --git a/rosette/guide/scribble/essentials/essentials.scrbl b/rosette/guide/scribble/essentials/essentials.scrbl index 3425ade6..009e5857 100644 --- a/rosette/guide/scribble/essentials/essentials.scrbl +++ b/rosette/guide/scribble/essentials/essentials.scrbl @@ -295,7 +295,7 @@ Using this grammar, we can sketch a fast implementation of the midpoint calculat (eval:alts (define (bvmid-fast lo hi) (fast-int32 lo hi #:depth 2)) - (require (only-in "bvmid.rkt" bvmid-fast)))] + (require (only-in rosette/guide/scribble/essentials/bvmid bvmid-fast)))] The above sketch describes the space of all expressions from the @racket[fast-int32] grammar that have parse trees of depth at most 2. The depth argument is optional. If ommitted, Rosette will use the value of the @racket[(current-grammar-depth)] parameter to bound the depth of the expressions drawn from the grammar. diff --git a/rosette/guide/scribble/forms/rosette-forms-log.txt b/rosette/guide/scribble/forms/rosette-forms-log.txt index 5d2b10a0..72ea9283 100644 --- a/rosette/guide/scribble/forms/rosette-forms-log.txt +++ b/rosette/guide/scribble/forms/rosette-forms-log.txt @@ -6,7 +6,7 @@ ((always-same) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -18,7 +18,7 @@ ((always-same) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -35,7 +35,7 @@ ((always-same-3) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -47,7 +47,7 @@ ((always-same-3) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -61,7 +61,15 @@ #"" #"") ((lambda (n) (define-symbolic y integer? #:length n) y) - ((3) 0 () 0 () () (q exn "define-symbolic: expected a natural? for #:length")) + ((3) + 0 + () + 0 + () + () + (q + exn + "eval:9.0: define-symbolic: expected a natural? for #:length\n at: (define-symbolic y integer? #:length n)\n in: (define-symbolic y integer? #:length n)")) #"" #"") ((define (always-different) (define-symbolic* x integer?) x) @@ -71,7 +79,7 @@ ((always-different) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -83,7 +91,7 @@ ((always-different) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -95,7 +103,7 @@ ((eq? (always-different) (always-different)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -111,7 +119,7 @@ ((always-different-n 2) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -123,7 +131,7 @@ ((always-different-n 3) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -135,7 +143,7 @@ ((equal? (always-different-n 4) (always-different-n 4)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -152,7 +160,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -166,7 +174,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -182,7 +190,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -195,7 +203,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -207,7 +215,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -221,7 +229,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -235,7 +243,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -251,7 +259,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -264,7 +272,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -280,7 +288,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -292,7 +300,7 @@ ((verify (assert a)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -304,7 +312,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -318,7 +326,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -330,7 +338,7 @@ ((verify (begin (assume c) (assert d))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -342,7 +350,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -354,7 +362,7 @@ ((verify (assert a)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -367,7 +375,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -379,7 +387,7 @@ ((verify (assert a)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -393,7 +401,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -409,7 +417,7 @@ (begin (assume (even? x)) (assert (odd? (+ x c))))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -421,7 +429,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -434,7 +442,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -446,7 +454,7 @@ ((synthesize #:forall (list x) #:guarantee (assert (odd? (+ x c)))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -458,7 +466,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -474,7 +482,7 @@ (begin (assume (even? x)) (assert (odd? (+ x c))))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -487,7 +495,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -503,7 +511,7 @@ (begin (assume (even? x)) (assert (odd? (+ x c))))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -518,7 +526,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -530,7 +538,7 @@ ((solve (assert y)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -542,7 +550,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -554,7 +562,7 @@ ((solve (assert (not x))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -567,7 +575,7 @@ ((vc) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -579,7 +587,7 @@ ((solve (assert (not x))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -594,7 +602,7 @@ ((inc (< x y)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -606,7 +614,7 @@ ((inc (> x 5)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -618,7 +626,7 @@ ((inc (< y 4)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -630,7 +638,7 @@ ((inc 1) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -642,7 +650,7 @@ ((inc (< y 9)) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -673,7 +681,7 @@ (begin (assume (< x 2)) (assert (< (- y x) 1)))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -693,7 +701,7 @@ ((solve (assert (= x 3.5))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -705,7 +713,7 @@ ((solve (assert (= x 64))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -717,7 +725,7 @@ ((solve (assert (and (= x 64) (= x 0)))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -754,7 +762,7 @@ ((solve (assert (= x 3.5))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -766,7 +774,7 @@ ((solve (assert (= x 64))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -778,7 +786,7 @@ ((solve (assert (and (= x 64) (= x 0)))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -790,7 +798,7 @@ ((solve (assert (forall (list x) (= x (+ x y))))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -802,7 +810,7 @@ ((solve (assert (= x (f x)))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 @@ -819,7 +827,7 @@ (assert (or (= (/ i j) 2) (= (/ j i) 2))))) ((3) 1 - ((#"/Users/emina/Projects/rosette4/rosette/guide/scribble/util/lifted.rkt" + (((lib "rosette/guide/scribble/util/lifted.rkt") . deserialize-info:opaque-v0)) 0 diff --git a/rosette/guide/scribble/rosette-guide.scrbl b/rosette/guide/scribble/rosette-guide.scrbl index 8796125c..513fc609 100644 --- a/rosette/guide/scribble/rosette-guide.scrbl +++ b/rosette/guide/scribble/rosette-guide.scrbl @@ -29,13 +29,13 @@ Chapters @seclink["ch:syntactic-forms"]{3}-@seclink["ch:libraries"]{6} define th @include-section["welcome/welcome.scrbl"] @include-section["essentials/essentials.scrbl"] @include-section["forms/forms.scrbl"] -@include-section["datatypes/builtin-datatypes.scrbl"] -@include-section["datatypes/defined-datatypes.scrbl"] -@include-section["libs/libraries.scrbl"] -@include-section["reflection/symbolic-reflection.scrbl"] -@include-section["unsafe/unsafe.scrbl"] -@include-section["performance/performance.scrbl"] -@include-section["error-tracing/error-tracing.scrbl"] +@;include-section["datatypes/builtin-datatypes.scrbl"] +@;include-section["datatypes/defined-datatypes.scrbl"] +@;include-section["libs/libraries.scrbl"] +@;include-section["reflection/symbolic-reflection.scrbl"] +@;include-section["unsafe/unsafe.scrbl"] +@;include-section["performance/performance.scrbl"] +@;include-section["error-tracing/error-tracing.scrbl"] @(require (only-in "refs.scrbl" generate-bibliography)) @(define bib @(generate-bibliography #:tag "refs" #:sec-title "References"))