diff --git a/.github/workflows/api-endpoint.yml b/.github/workflows/api-endpoint.yml index 870bfe6d4..109d62aeb 100644 --- a/.github/workflows/api-endpoint.yml +++ b/.github/workflows/api-endpoint.yml @@ -15,7 +15,7 @@ jobs: - name: "Install Racket" uses: Bogdanp/setup-racket@v1.8 with: - version: 8.10 + version: 8.5 - name: Install Rust compiler uses: actions-rs/toolchain@v1 with: @@ -51,4 +51,4 @@ jobs: # run: node -e "fetch('https://google.com')" - name: "Test the endpoint" - run: node infra/testApi.mjs + run: node infra/testApi.mjs \ No newline at end of file diff --git a/.github/workflows/distribute.yml b/.github/workflows/distribute.yml index 19fe8819c..1c8c5ca92 100644 --- a/.github/workflows/distribute.yml +++ b/.github/workflows/distribute.yml @@ -18,7 +18,7 @@ jobs: - name: "Install Racket" uses: Bogdanp/setup-racket@v1.9 with: - version: 8.10 + version: 8.7 - name: Install Rust compiler uses: actions-rs/toolchain@v1.0.6 with: diff --git a/.github/workflows/egg-herbie.yml b/.github/workflows/egg-herbie.yml index aedea02dd..abce1d2ee 100644 --- a/.github/workflows/egg-herbie.yml +++ b/.github/workflows/egg-herbie.yml @@ -15,7 +15,7 @@ jobs: - name: "Install Racket" uses: Bogdanp/setup-racket@v1.9 with: - version: 8.10 + version: 8.7 - name: Install Rust compiler uses: actions-rs/toolchain@v1.0.6 with: diff --git a/.github/workflows/plugins.yml b/.github/workflows/plugins.yml index dfdf39d0a..f0eab03f8 100644 --- a/.github/workflows/plugins.yml +++ b/.github/workflows/plugins.yml @@ -6,6 +6,36 @@ env: RUST_BACKTRACE: full jobs: + softposit: + name: "Plugin tests (Posits)" + runs-on: ubuntu-latest + steps: + - name: "Install Packages" + run: sudo apt-get install -y libmpfr6 libmpfr-dev + - name: "Install Racket" + uses: Bogdanp/setup-racket@v1.9 + with: + version: 8.7 + - name: Install Rust compiler + uses: actions-rs/toolchain@v1.0.6 + with: + toolchain: stable + default: true + override: true + components: rustfmt, clippy + - uses: actions/checkout@master + - name: "Install dependencies" + run: make install + - name: "Check out softposit-herbie master" + uses: actions/checkout@master + with: + repository: herbie-fp/softposit-herbie + path: plugin + - name: "Install SoftPosit support" + run: raco pkg install --no-cache --auto --name softposit-herbie plugin/ + - name: "Run posit benchmarks" + run: racket infra/travis.rkt --precision posit16 --seed 0 plugin/bench/posits.fpcore + softposit-pherbie: name: "Plugin tests (Posits, Pherbie)" runs-on: ubuntu-latest @@ -15,7 +45,7 @@ jobs: - name: "Install Racket" uses: Bogdanp/setup-racket@v1.8 with: - version: 8.10 + version: 8.5 - name: Install Rust compiler uses: actions-rs/toolchain@v1 with: diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 0eac3f5c5..22ea18d5e 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -45,7 +45,7 @@ jobs: - name: Install Racket uses: Bogdanp/setup-racket@v1.9 with: - version: 8.10 + version: 8.7 - name: Install Rust compiler uses: actions-rs/toolchain@v1.0.6 diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 2a1cc4488..4d2d774fa 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -11,7 +11,7 @@ jobs: runs-on: ubuntu-latest strategy: matrix: - racket-version: [ '8.2', '8.10' ] + racket-version: [ '8.0', '8.7' ] precision: [ 'binary32', 'binary64' ] steps: - name: "Install Packages" @@ -41,7 +41,7 @@ jobs: - name: "Install Racket" uses: Bogdanp/setup-racket@v1.9 with: - version: 8.10 + version: 8.7 - name: Install Rust compiler uses: actions-rs/toolchain@v1.0.6 with: diff --git a/.github/workflows/tools.yml b/.github/workflows/tools.yml index ac82867d4..974d0a827 100644 --- a/.github/workflows/tools.yml +++ b/.github/workflows/tools.yml @@ -15,7 +15,7 @@ jobs: - name: "Install Racket" uses: Bogdanp/setup-racket@v1.9 with: - version: 8.10 + version: 8.7 - name: Install Rust compiler uses: actions-rs/toolchain@v1.0.6 with: @@ -38,7 +38,7 @@ jobs: - name: "Install Racket" uses: Bogdanp/setup-racket@v1.9 with: - version: 8.10 + version: 8.7 - name: Install Rust compiler uses: actions-rs/toolchain@v1.0.6 with: @@ -61,7 +61,7 @@ jobs: - name: "Install Racket" uses: Bogdanp/setup-racket@v1.9 with: - version: 8.10 + version: 8.7 - name: Install Rust compiler uses: actions-rs/toolchain@v1.0.6 with: diff --git a/.github/workflows/unit-test.yml b/.github/workflows/unit-test.yml index f348bae28..0267aa233 100644 --- a/.github/workflows/unit-test.yml +++ b/.github/workflows/unit-test.yml @@ -15,7 +15,7 @@ jobs: - name: "Install Racket" uses: Bogdanp/setup-racket@v1.9 with: - version: 8.10 + version: 8.7 - name: Install Rust compiler uses: actions-rs/toolchain@v1.0.6 with: diff --git a/bench/hamming/rearrangement.fpcore b/bench/hamming/rearrangement.fpcore index 4d8acf274..2f16eaa44 100644 --- a/bench/hamming/rearrangement.fpcore +++ b/bench/hamming/rearrangement.fpcore @@ -38,7 +38,6 @@ (FPCore (x) :name "2frac (problem 3.3.1)" - (- (/ 1 (+ x 1)) (/ 1 x))) (FPCore (x eps) @@ -52,7 +51,6 @@ :name "3frac (problem 3.3.3)" :herbie-target (/ 2 (* x (- (* x x) 1))) - :herbie-expected 2 (+ (- (/ 1 (+ x 1)) (/ 2 x)) (/ 1 (- x 1)))) diff --git a/bench/haskell.fpcore b/bench/haskell.fpcore index 57163c386..f00d6c63b 100644 --- a/bench/haskell.fpcore +++ b/bench/haskell.fpcore @@ -1403,10 +1403,9 @@ :name "Numeric.SpecFunctions:log1p from math-functions-0.1.5.2, A" (* x (- 1.0 (* x y)))) -;; TODO: Trello Benchmark Sources - Numeric.SpecFunctions:log1p from math-functions-0.1.5.2, B -;; (FPCore (x) -;; :name "Numeric.SpecFunctions:log1p from math-functions-0.1.5.2, B" -;; (* x (- 1.0 (* x 0.5)))) +(FPCore (x) + :name "Numeric.SpecFunctions:log1p from math-functions-0.1.5.2, B" + (* x (- 1.0 (* x 0.5)))) (FPCore (x y z t a b) :name "Numeric.SpecFunctions:logBeta from math-functions-0.1.5.2, A" diff --git a/src/core/localize.rkt b/src/core/localize.rkt index 9fc41c08c..46d56fd8d 100644 --- a/src/core/localize.rkt +++ b/src/core/localize.rkt @@ -28,13 +28,11 @@ (if (null? exprs) empty (compute-local-errors exprs ctx))) (for/list ([expr (in-list exprs)] [errs (in-list errss)]) (sort - (sort - (reap [sow] - (for ([(expr err) (in-hash errs)]) - (unless (andmap (curry = 1) err) - (sow (cons err expr))))) - > #:key (compose errors-score car)) - expr #:key cdr))) + (reap [sow] + (for ([(expr err) (in-hash errs)]) + (unless (andmap (curry = 1) err) + (sow (cons err expr))))) + > #:key (compose errors-score car)))) ; Compute local error or each sampled point at each node in `prog`. (define (compute-local-errors exprs ctx) diff --git a/src/core/reduce.rkt b/src/core/reduce.rkt index 2e56c9dfe..31e61340e 100755 --- a/src/core/reduce.rkt +++ b/src/core/reduce.rkt @@ -186,10 +186,8 @@ (for ([term terms]) (let ([sum (hash-ref! h (cadr term) (λ () 0))]) (hash-set! h (cadr term) (+ (car term) sum)))) - (sort - (reap [sow] - (hash-for-each h (λ (k v) (when (not (= v 0)) (sow (cons v k)))))) - expr #:key cdr))) + (reap [sow] + (hash-for-each h (λ (k v) (when (not (= v 0)) (sow (cons v k)))))))) (define (combine-mterms terms) (cons @@ -198,10 +196,8 @@ (for ([term (cdr terms)]) (let ([sum (hash-ref! h (cdr term) (λ () 0))]) (hash-set! h (cdr term) (+ (car term) sum)))) - (sort - (reap [sow] - (hash-for-each h (λ (k v) (when (not (= v 0)) (sow (cons v k)))))) - expr #:key cdr)))) + (reap [sow] + (hash-for-each h (λ (k v) (when (not (= v 0)) (sow (cons v k))))))))) (define (aterm->expr term) (match term diff --git a/src/mainloop.rkt b/src/mainloop.rkt index 0c6950741..55721c3c1 100644 --- a/src/mainloop.rkt +++ b/src/mainloop.rkt @@ -136,7 +136,7 @@ [(err expr) (in-dict loc-errs)] [i (in-range (*localize-expressions-limit*))]) (timeline-push! 'locations (~a expr) (errors-score err) - (not (patch-table-has-expr? expr)) (~a (representation-name repr))) + (not (patch-table-has-expr? expr)) (format "~a" (representation-name repr))) expr)) ; low-error locations (Pherbie-only with multi-precision) @@ -300,13 +300,23 @@ (list (*context*)))) (cons domain (apply mk-pcontext pts+exs))) -(define (initialize-alt-table! alternatives context pcontext) - (match-define (cons initial simplified) alternatives) - (*start-prog* (alt-expr initial)) - (define table (make-alt-table pcontext initial context)) - (define simplified* (append-map (curryr starting-alts context) simplified)) - (define-values (errss costs) (atab-eval-altns table simplified* context)) - (^table^ (atab-add-altns table simplified* errss costs))) +(define (initialize-alt-table! prog pcontext ctx) + (define alt (make-alt prog)) + (*start-prog* prog) + (define table (make-alt-table (*pcontext*) alt ctx)) + + ; Add starting alt in every precision + (^table^ + (if (*pareto-mode*) + (let ([new-alts (starting-alts alt ctx)]) + (define-values (errss costs) (atab-eval-altns table new-alts ctx)) + (atab-add-altns table new-alts errss costs)) + table)) + + (when (flag-set? 'setup 'simplify) + (reconstruct! (patch-table-run-simplify (atab-active-alts (^table^)))) + (finalize-iter!) + (^next-alts^ #f))) ;; This is only here for interactive use; normal runs use run-improve! (define (run-improve vars prog iters @@ -320,23 +330,22 @@ (define original-points (setup-context! vars (or specification prog) precondition repr)) (run-improve! iters prog specification preprocess original-points repr)) -(define (run-improve! initial specification context pcontext) +(define (run-improve! expression context pcontext rules iterations #:specification [specification #f]) (timeline-event! 'preprocess) - (define-values (simplified preprocessing) - (find-preprocessing initial specification context)) + (define preprocessing (find-preprocessing (or specification expression) context rules)) (timeline-push! 'symmetry (map ~a preprocessing)) (define pcontext* (preprocess-pcontext context pcontext preprocessing)) - (match-define (and alternatives (cons (alt best _ _) _)) - (mutate! simplified context pcontext* (*num-iterations*))) + (match-define (and alternatives (cons best _)) + (mutate! expression iterations pcontext*)) (timeline-event! 'preprocess) (define preprocessing* - (remove-unnecessary-preprocessing best context pcontext preprocessing)) + (remove-unnecessary-preprocessing (alt-expr best) context pcontext preprocessing)) (values alternatives preprocessing*)) -(define (mutate! simplified context pcontext iterations) +(define (mutate! prog iters pcontext) (*pcontext* pcontext) - (initialize-alt-table! simplified context pcontext) - (for ([iteration (in-range iterations)] #:break (atab-completed? (^table^))) + (initialize-alt-table! prog (*pcontext*) (*context*)) + (for ([iter (in-range iters)] #:break (atab-completed? (^table^))) (run-iter!)) (extract!)) diff --git a/src/patch.rkt b/src/patch.rkt index 9f5cb1867..462d819b0 100644 --- a/src/patch.rkt +++ b/src/patch.rkt @@ -7,6 +7,7 @@ (provide (contract-out [patch-table-has-expr? (-> expr? boolean?)] + [patch-table-run-simplify (-> (listof alt?) (listof alt?))] [patch-table-run (-> (listof expr?) (listof expr?) (listof alt?))])) ;;;;;;;;;;;;;;;;;;;;;;;;;;;; Patch table ;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -287,3 +288,10 @@ (simplify!) (begin0 (apply append (^final^) (map patch-table-get cached)) (patch-table-clear!))])) + +(define (patch-table-run-simplify altns) + (^rewrites^ (append altns (if (^rewrites^) (^rewrites^) '()))) + (simplify!) + (begin0 (^final^) + (patch-table-clear!))) + diff --git a/src/preprocess.rkt b/src/preprocess.rkt index 33ffd698d..fb85c003b 100644 --- a/src/preprocess.rkt +++ b/src/preprocess.rkt @@ -1,80 +1,46 @@ #lang racket (require "core/egg-herbie.rkt" "core/simplify.rkt" - "syntax/rules.rkt" "syntax/syntax.rkt" "syntax/types.rkt" - "alternative.rkt" "common.rkt" "programs.rkt" "points.rkt" - "timeline.rkt" "float.rkt") + "syntax/syntax.rkt" "syntax/types.rkt" "alternative.rkt" "common.rkt" + "programs.rkt" "points.rkt" "timeline.rkt" "float.rkt") (provide find-preprocessing preprocess-pcontext remove-unnecessary-preprocessing) ;; See https://pavpanchekha.com/blog/symmetric-expressions.html -(define (find-preprocessing initial specification context) - (define even-identities - (for/list ([variable (in-list (context-vars context))] - [representation (in-list (context-var-reprs context))]) +(define (find-preprocessing expression context rules) + ;; Here `*` means a test identity that *may* be equal to `expression`, and + ;; `~` means the simplest form of an expression. + (define variables (context-vars context)) + (define variable-representations (context-var-reprs context)) + (define evens* + (for/list ([variable (in-list variables)] + [representation (in-list variable-representations)]) ;; TODO: Handle case where neg isn't supported for this representation (define negate (get-parametric-operator 'neg representation)) - (replace-vars (list (cons variable (list negate variable))) specification))) - (define pairs (combinations (context-vars context) 2)) - (define swap-identities + (replace-vars (list (cons variable (list negate variable))) expression))) + (define pairs (combinations variables 2)) + (define swaps* (for/list ([pair (in-list pairs)]) (match-define (list a b) pair) - (replace-vars (list (cons a b) (cons b a)) specification))) - (define query - (make-egg-query - (list* - initial - specification - (append even-identities swap-identities)) - (*simplify-rules*))) - (match-define - (cons - ;; The first element of the list returned by `simplify-batch` will be a list - ;; containing progressively simpler versions of `initial` at each iteration - ;; of the e-graph, the first of which will always be the unsimplified - ;; `initial` from iteration 0, which we want to exclude here to avoid adding - ;; it twice to the alt-table. - (app rest initials) - (app (curry map last) - (cons - specification* - (app (curryr split-at (length even-identities)) evens* swaps*)))) - (simplify-batch query)) - (define alternative (make-alt initial)) - (define simplified - (cons - ;; We excluded the first element of `initials` above so that we can add it - ;; here manually, but without a self-referential history. - alternative - (remove-duplicates - (for/list ([expression (in-list initials)]) - (alt - expression - (list 'simplify null query #f #f) - (list alternative))) - alt-equal?))) - (define components - (connected-components - (context-vars context) - (filter-map - (lambda (pair swap*) (and (equal? specification* swap*) pair)) - pairs - swaps*))) + (replace-vars (list (cons a b) (cons b a)) expression))) + (define query (make-egg-query (cons expression (append evens* swaps*)) rules)) + (match-define (cons expression~ rest~) (map last (simplify-batch query))) + (define-values (evens~ swaps~) (split-at rest~ (length evens*))) + (define swaps (filter-map + (lambda (pair swap~) (and (equal? expression~ swap~) pair)) + pairs + swaps~)) + (define components (connected-components variables swaps)) (define abs-instructions - (for/list ([variable (in-list (context-vars context))] - [even* (in-list evens*)] - #:when (equal? specification* even*)) + (for/list ([variable (in-list variables)] [even~ (in-list evens~)] + #:when (equal? expression~ even~)) (list 'abs variable))) (define sort-instructions (for/list ([component (in-list components)] #:when (> (length component) 1)) (cons 'sort component))) - (values - (if (flag-set? 'setup 'simplify) - simplified - (list (make-alt initial))) - ;; Absolute value should happen before sorting - (append abs-instructions sort-instructions))) + ;; Absolute value should happen before sorting + (append abs-instructions sort-instructions)) (define (connected-components variables swaps) (define components (disjoint-set (length variables))) diff --git a/src/sandbox.rkt b/src/sandbox.rkt index c7d3601ce..32104ac45 100644 --- a/src/sandbox.rkt +++ b/src/sandbox.rkt @@ -138,7 +138,10 @@ (define-values (train-pcontext test-pcontext) (partition-pcontext pcontext context)) ;; TODO: Ignoring all user-provided preprocessing right now (define-values (alternatives preprocessing) - (run-improve! (test-input test) (test-spec test) (*context*) train-pcontext)) + (run-improve! + ;; If the specification is given, it is used for sampling points + (test-input test) (*context*) train-pcontext (*simplify-rules*) + (*num-iterations*) #:specification (test-spec test))) (define test-pcontext* (preprocess-pcontext (*context*) test-pcontext preprocessing)) (when seed (set-seed! seed)) @@ -163,7 +166,10 @@ (split-pcontext joint-pcontext (*num-points*) (*reeval-pts*))) ;; TODO: Ignoring all user-provided preprocessing right now (define-values (end-alts preprocessing) - (run-improve! (test-input test) (test-spec test) (*context*) train-pcontext)) + (run-improve! + ;; If the specification is given, it is used for sampling points + (test-input test) ctx train-pcontext (*simplify-rules*) (*num-iterations*) + #:specification (test-spec test))) (define test-pcontext* (preprocess-pcontext ctx test-pcontext preprocessing)) (when seed (set-seed! seed)) diff --git a/src/web/timeline.rkt b/src/web/timeline.rkt index 8ffd14b13..1bbc6fc2f 100644 --- a/src/web/timeline.rkt +++ b/src/web/timeline.rkt @@ -110,8 +110,8 @@ (format-percent (hash-ref domain-info tag 0) total))]))))))) (define (render-phase-locations locations) - `((dt "Localize:") - (dd (p "Found " ,(~a (length locations)) " expressions with local error:") + `((dt "Local Accuracy") + (dd (p "Found " ,(~a (length locations)) " expressions with local accuracy:") (table ([class "times"]) (thead (tr (th "New") (th "Accuracy") (th "Program"))) ,@(for/list ([rec (in-list locations)]) @@ -259,7 +259,7 @@ (define (render-phase-error min-error-table) (match-define (list min-error repr) (car min-error-table)) - `((dt "Accuracy") + `((dt "Accurracy") (dd ,(format-accuracy min-error (representation-total-bits (get-representation (string->symbol repr))) #:unit "%") ""))) (define (render-phase-rules rules) diff --git a/www/doc/2.1/api-endpoints.html b/www/doc/2.1/api-endpoints.html deleted file mode 100644 index 50a5e2b5d..000000000 --- a/www/doc/2.1/api-endpoints.html +++ /dev/null @@ -1,231 +0,0 @@ - - -
- -The Herbie API allows applications to - interface with Herbie using HTTP requests. The API is designed to - be stateless: the order in which endpoints are called shouldn't - matter.
- -All the endpoints listed below respond to POST requests unless - otherwise specified. A typical example of sending a POST request - to a running Herbie server is:
- -curl -X POST -d \ - '{"formula": "(FPCore (x) (- (sqrt (+ x 1))))",\ - "seed": 5})}' \ - -H 'Content-Type: application/json' \ - http://127.0.0.1:8000/api/sample -- -
Request:
- -{ - formula: <FPCore expression>, - seed: <random seed for point generation> - }- -
Response:
- -{ - points: [[point, exact], ... ] - }-
The sample
endpoint allows the user to request a
- sample of points given the FPCore expression and a seed.
Returns a collection of points and the exact evaluation of each
- point with the given spec. The results are returned through the
- "points" field and are represented by an array of point-exact
- pairs with the first value representing the point and the second
- value representing the exact evaluation; the exact value of
- point n
is points[n][1]
.
Herbie calculates the "ground truth" by calculating the values - with more precise numbers. This can be slow.
- -Request:
- -{ - formula: <FPCore expression>, - sample: [point, ... ] - }- -
Response:
- -{ - points: [[point, exact], ... ] - }-
The exacts
endpoint allows the user to request the
- exact value of a set of points evaluated at a real number
- specification given as an FPCore expression.
Some points may not be calculable given the FPCore - expression.
- -Returns a collection of points and the exact evaluation of each
- point with the given spec. The results are returned through the
- "points" field and are represented by an array of point-exact
- pairs with the first value representing the point and the second
- value representing the exact evaluation; the exact value of
- point n
is points[n][1]
.
Herbie calculates the "ground truth" by calculating the values - with more precise numbers. This can be slow.
- -Request:
- -{ - formula: <FPCore expression>, - sample: [point ... ] - }- -
Response:
- -{ - points: [[point, exact], ... ] - }-
The calculate
endpoint allows the user to request
- the evaluation of a set of points evaluated at a floating-point
- implementation given as an FPCore expression.
Some points may not be calculable given the FPCore expression.
- -Returns a collection of points and the evaluation of each point
- using the given FPCore as a floating-point implementation. The
- results are returned through the "points" field and are
- represented by an array of point-exact pairs with the first value
- representing the point and the second value representing the
- evaluated value; the evaluated value of point n
- is points[n][1]
.
Request:
- -{ - formula: <FPCore expression>, - sample: [[point, exact], ... ] -}- -
Response:
- -{ - points: [[point, error], ... ] -}-
The analyze
endpoint allows the user to request
- error analysis of a set of point-exact pairs and a given
- floating-point implementation.
Given a collection of points, their exact values, and an FPCore
- expression to analyze on, the analyze
endpoint
- returns the error for each point for that expression. The error
- value returned is Herbie's internal error heuristic.
Request:
- -{ - formula: <FPCore expression>, - sample: [[point, exact], ... ] -}- -
Response:
- -{ - alternatives: [alt, ... ], - histories: [history, ... ], - splitpoints: [splitpoint, ... ] -}-
The alternatives
endpoint allows the user to
- request rewrites from Herbie given an expression to rewrite and a
- set of point-exact pairs.
Returns a list of alternatives represented by FPCore - expressions through the "alternatives" field.
- -Returns a list of derivations of each alternative through the
- "histories" field where history[n]
corresponds
- to alternatives[n]
.
Returns a list of splitpoints for each alternative through the
- "splitpoints" field where splitpoints[n]
corresponds
- to alternatives[n]
. splitpoints[n]
will
- only contain information about the corresponding alternative.s
- splitpoints if the alternative is a branch-expression.
Request:
- -{ - formula: <FPCore expression> -}- -
Response:
- -{ - mathjs: <mathjs expression> -}-
The mathjs
endpoint allows the user to translate
- FPCore expressions into mathjs expressions.
- High-level system diagram of Herbie. It highlights Herbie's core architecture, - external libraries, and user interactions. - Basic flow: Herbie passes user input (expression, precondition, etc.) to the - mainloop (scheduler) which alternates between generate and test phases multiple times, - maintaining and improving a set of accurate expressions at each iteration. - Once the generate-and-test phase is complete, Herbie extracts either - one or many output expressions using an algorithm called regime inference. - Regime inference chooses the "best" (usually most accurate) - generated candidate expression or combines multple candidates, - each "best" on a smaller part of the input range, with a branch condition. -
- - - diff --git a/www/doc/2.1/docker.html b/www/doc/2.1/docker.html deleted file mode 100644 index 555f69734..000000000 --- a/www/doc/2.1/docker.html +++ /dev/null @@ -1,164 +0,0 @@ - - - - -- Herbie is available - through Docker, which is - sort of like a virtual machine. This page describes how to install - the official Docker - image for Herbie. -
- -- Herbie can also be installed from - package or source. Herbie via Docker is only recommended if - you already have Docker experience. -
- -
- First, install
- Docker. Docker supports Windows, macOS, and Linux. Depending
- on how you install Docker, you may need to prefix
- the docker
commands with sudo
or run them
- as the administrative user.
-
With Docker installed, you can run the Herbie shell with:
- -docker run -it uwplse/herbie shell- -
This will download the Herbie image and then run - its shell tool.
- -Herbie in Docker is more limited; for example, it will not - recognize plugins installed outside the Docker container.
- -- You can run the Herbie web server locally with - -
docker run -it --rm -p 8000:80 uwplse/herbie- - and access the server at http://localhost:8000. - -
- (Herbie's Docker image binds to port 80 by
- default; this command uses the -p <hostport>:80
option to expose Herbie on port 8000.)
-
- If you are using the --log
- or --save-session
flags for the web shell,
- you will also need to mount the relevant directories into the
- Docker container using the -v
Docker option, as in
- the examples below.
-
- To use Herbie in batch mode, you will - need to mount the input in the Docker container. Do that with: -
- -docker run -it --rm \ - -v in-dir:/in \ - -v out-dir:/out \ - -u $USER \ - uwplse/herbie improve /in/in-file /out/out-file- -
- In this command, you are asking Herbie to read input - from in-file in in-dir, and write output - to out-file in out-dir. The command looks - the same if you want Herbie to read input from a directory; - just leave in-file blank. -
- -- To generate reports from Herbie, you can run: -
- -docker run -it --rm \ - -v in-dir:/in \ - -v out-dir:/out \ - -u $USER \ - uwplse/herbie report /in/in-file /out/- -
- As before, the input and output directories must be mounted inside - the Docker container. Note that both here and above, the user is - set to the current user. This is to ensure that the files Herbie creates - have the correct permissions set. -
- -This section is primarily of interest for the Herbie developers.
- -
- Clone the repo and confirm that Herbie builds correctly
- with make install
.
-
- Next, examine the Dockerfile and Makefile together. The Dockerfile
- should follow a process exactly like the Makefile, except a clean
- initial environment is assumed. The build may be split into 2 or
- more stages to limit the size of the resulting image. Each stage
- consists of a FROM
command and a series of further
- commands to build up the desired environment, and later stages can
- refer to earlier stages by name—for example, COPY
- --from=earlier-stage ...
can copy files compiled in earlier
- images. You may need to do things like bumping the version of Rust
- used for binary compilation or the version of Racket used in
- production, or adjusting paths to match the newest version of the
- repo.
-
Once you are ready to build, run this command from the repository root:
- -docker build -t uwplse/herbie:test .- -
This builds a new test image and tags
- it uwplse/herbie:test
. You can run this image with:
docker run -p 8000:80 -it uwplse/herbie:test- -
The web demo should now be visiable at http://localhost:8000
.
To open a shell in a running container for testing, first get the container ID with:
- -docker ps- -
Then open a root shell in that container with
- -docker exec -it <CONTAINER ID> sh- -
The code and egg-herbie binaries should be
- under /src
.
- Herbie helps you identify and correct floating - point error in your numeric programs. But what is floating point - error, and how does Herbie measure it? -
- -When Herbie reports a "percentage accuracy" number like 92.3%, it's -usually best to think of that as the percentage of floating-point -inputs where the expression is reasonably accurate.
- -The impact of this error on your application will depend a lot -on which 7.7% of inputs are inaccurate, and what kind of -error that is. You can find this out using -the accuracy graph in Herbie reports. You -can also use preconditions to restrict the inputs Herbie is -considering.
- -In mathematics, we work with real numbers, but on a computer, we -typically use floating-point numbers. Because there are infinitely -many real numbers, but only finitely many floating-point numbers, some -real numbers can't be accurately represented. This means that every -time you do an operation, the true result typically has to -be rounded to a representable one.
- -Take an extreme example: the code 1e100 + 1
, which
-increments a huge number in IEEE 754 double-precision floating-point.
-There's an exact real-number answer, a one followed by 99 zeros and
-then another 1, but the closest floating-point value is the
-same as 1e100
.
Errors like this can cause problems. In the example above, the
-answers differ by one part per googol, which is pretty small. But the
-error can grow. For example, since 1e100 + 1
rounds to
-the same value as 1e100
, the larger computation
-
-
(1e100 + 1) - 1e100- -returns
0
instead of the correct answer, 1
.
-Now the difference is pretty stark, and can grow even bigger through
-later operations.
-
-There are lots of ways to measure how much rounding error -there is in a computation. Most people find the notions of absolute -and relative error most intuitive, but Herbie internally uses a more -complex notion called bits of error.
- -The bits of error metric imagines you have a list of all of the -possible floating-point numbers, from largest to smallest. In that -list, compare the floating-point value you computed to the one closest -to the true answer. If they are the same, that's called 0 bits of -error; if they are one apart, that's called one bit of error; three -apart is two bits of error; and so on.
- -In general, if the two floating-point values are n items
-apart, Herbie says they have log2(n + 1)
bits of error.
-Values like 0
and -0
are treated as having 0
-bits of error, and NaN
is considered to have the maximum
-number of bits of error against non-NaN
values. While
-there's all sorts of theoretical justifications, Herbie mainly uses
-this error metric because we've found it to give the best
-results.
On a single input, the best way to interpret the "bits of error" -metric is that it tells you roughly how many bits of the answer, -starting at the end, are useless. With zero bits of error, you have -the best answer possible. With four bits, that's still pretty good -because it's four out of 64. But with 40 or 50 bits of error, you're -getting less accuracy out of the computation than even a -single-precision floating-point value. And it's even possible to have -something like 58 or 60 bits of error, in which case even the sign and -exponent bits (which in double-precision floating-point occupy the top -12 bits of the number) are incorrect.
- -Because different number representations have different numbers of -bits, Herbie shows the percentage of bits that are accurate instead of -the bits of error. With double-precision floats, for example, 75% -accurate means 16 bits of error.
- -Bits of error measures the error of a computation for some specific -input. But usually you're interested in the error of a computation -across many possible inputs. Herbie therefore averages the accuracy -percentage across many randomly-sampled valid inputs.
- -Typically, inputs points are either very accurate or not accurate -at all. So when computing percentage accuracy, Herbie's averaging a -lot of points with near-100% accuracy and a lot of points with near-0% -accuracy. In that sense, you can think of percentage accuracy as -measuring mostly what percentage of inputs are accurate. If -Herbie says your computation is 75% accurate what it's really saying -is that about a quarter of inputs produce usable outputs.
- -Since percentage accuracy averages over many points, it depends on -what points it is averaging over, and how is samples among them. -Herbie samples among valid inputs, uniformly distributed.
- -Herbie considers an input valid if it is a floating-point value in -the appropriate precision and its true, real-number output 1) exists; -2) satisfies the user's precondition; and 3) can be computed. Let's -dive into each requirement.
- -(< 1 x 2)
, then the input x = 3
is
- invalid.(/ (exp
- 1e9) (exp 1e9))
, which divides two identical but gargantuan
- numbers, does have an exact real-number answer (one), but Herbie
- can't compute that exact answer because the intermediate steps are
- too large. This input is also invalid.Herbie's percentage accuracy metric only averages over valid -points. This means that when you change your precondition, you change -which points are valid, and that can change the percentage accuracy -reported by Herbie. This is useful: if you know there's a rare error, -but Herbie thinks error is low, you can change your precondition to -focus on the points of interest.
- -When randomly sampling inputs, Herbie considers each valid input -equally likely. Importantly, this does not mean that it uses a uniform -distribution, because floating-point values themselves are not -uniformly distributed.
- -For example, there are as many floating-point values between 1 and -2 as there are between one and one half, because floating-point values -use an exponential encoding. But that means that if you're looking at -a computation where the input comes from the interval [0.5, -2], Herbie will weight the first third of that range twice as -high as the other two thirds.
- -This can produce unintuitive results, especially for intervals that -cross 0. For example, in the interval [0, 1], the second -half of that interval (from one half to one) has a tiny proportion of -the weight (in double-precision floating-point, about 0.1%). If Herbie -can improve accuracy by a little bit between zero and one half, while -dramatically reducing accuracy between one half and one, it will think -that that's an accuracy improvement. You might disagree.
- -Unfortunately, there's no way for Herbie to intuit exactly what you
-mean, so understanding this error distribution is essential to
-understanding Herbie's outputs. For example, if Herbie reports that
-accuracy improved from 75% to 76%, it's essential to know: is the
-improvement happening on inputs between one half and one, or
-between 1e-100
and 2e-100
? To answer this
-question, it's important to look over
-the reports and graphs generated by
-Herbie.
Herbie automatically transforms floating - point expressions into more accurate forms. This page troubleshoots - common Herbie errors, warnings, and known issues.
- - -- Herbie error messages refer to this second for additional - information and debugging tips. -
- -
- This error means you mis-formatted Herbie's input. Common errors
- include misspelled function names and parenthesized expressions
- that should not be parenthesized. For example, in
- (- (exp (x)) 1)
, the expression x
is a
- variable so shouldn't be parenthesized. (- (exp x) 1)
- would be the correct way to write that expression.
- The input format documentation has more
- details on Herbie's syntax.
-
This error occurs when Herbie is unable to find enough valid
- points. For example, the expression (acos (+ 1000 x))
- is invalid unless (<= -1001 x -999)
, a rather narrow
- range. The simplest fix is to increase
- the --num-analysis
flag.
- Specifying the range of valid points as
- a precondition can also help.
-
This error indicates that your input has no valid inputs, usually
- due to an overly restriction precondition. For example, the
- precondition (< 3 x 2)
excludes all inputs. The
- solution is to fix the precondition or input program.
Herbie warnings refer to this section for explanations and common - actions to take.
- -
- Sometimes, an input to your expression produces an output so large
- that it's best represented by a floating-point infinity. For
- example, (exp 1000)
is over 10434, so it's
- much larger than the largest floating-point value. Herbie raises
- this warning when too many inputs (more than 20% of them) are this
- large, because that usually indicates you should set a more
- restrictive precondition.
-
- Herbie raises this warning when some inputs require more than
- 10,000 bits to compute an exact ground truth. For example, to
- compute (/ (exp x) (exp x))
for very
- large x
, absurdly large numbers would be required.
- Herbie discards such inputs and raises this warning. If you see
- this warning, you should add a restrictive precondition, such
- as :pre (< -100 x 100)
, to prevent large inputs.
-
- Herbie will raise this warning when it needs more than 10,000 bits - to produce a string representation for a given value. This is - likely the result of a bug in a third-party plugin. -
- -- Herbie uses a set of algebraic rewrite rules in order to simplify - expressions, but these rules can sometimes lead to a - contradiction. Herbie will automatically compensate for this, and - in most cases nothing needs to be done. However, Herbie may have - failed to simplify the output. -
- -- The input FPCore contains a variable that is not - used in the body expression. -
- -- The input expression contains a variable that is similar in name - to named constants, e.g. e instead of E. -
- -Bugs that cannot be directly fixed are documented in this section.
- -
- When using Chrome to view web pages on your local machine, Herbie
- reports cannot draw the arrow chart due to security restrictions.
- Run
- Chrome with --allow-file-access-from-files
to fix
- this error.
-
- Herbie uses - the FPCore format to specify an - input program, and has extensive options for precisely describing - its context. -
- -The Herbie web shell takes input in a subset of - the math.js - syntax. The web shell automatically checks for syntax errors, - and provides a graphical user interface for specifying the input - domain. The web shell converts the mathematical expression and input - ranges into FPCore before sending it to Herbie.
- -Herbie's command-line and batch-mode tools - use FPCore format to describe - mathematical expressions. FPCore looks like this:
- -(FPCore (inputs ...) properties ... expression)-
(FPCore name (inputs ...) properties ... expression)- -
- Each input is a variable name, like x
,
- used in the expression. Properties are used to specify
- additional information about the expression's context.
- If name is specified, the function can be referenced in
- subsequent FPCore declarations in the file.
-
- The expression is written in prefix form, with every function call - parenthesized, as in Lisp. For example, the formula for the - hypotenuse of a triangle with legs a and b is: -
- -(FPCore (a b) (sqrt (+ (* a a) (* b b))))- -
- The semicolon (;) character introduces a line comment.
- We recommend the .fpcore
file extension for Herbie input files.
-
- Herbie supports all functions - from math.h - with floating-point-only inputs and outputs. The best supported - functions include: -
- -+
, -
, *
, /
, fabs
sqrt
, cbrt
pow
, exp
, log
sin
, cos
, tan
asin
, acos
, atan
, atan2
sinh
, cosh
, tanh
asinh
, acosh
, atanh
fma
, expm1
, log1p
, hypot
Herbie also supports the constants PI
- and E
. The arithmetic operators associate to the left,
- and -
is used for both subtraction and negation.
Herbie links against your computer's libm
to
- evaluate these functions. So, each function has the same behavior in
- Herbie as in your code. You can instead use
- the racket
precision if you
- instead want reproducible behavior.
FPCore uses if
for conditional expressions:
(if cond if-true if-false)- -
- The conditional cond
may use:
-
==
, !=
, <
, >
, <=
, >=
and
, or
, not
TRUE
, FALSE
The comparison functions support chained comparisons with more than two arguments.
- -Intermediate variables can be defined
- using let
and let*
:
(let ([variable value] ...) body)-
(let* ([variable value] ...) body)- -
In both let
and let*
,
- each variable is bound to its value and can be
- used in the body. The difference between let
- and let*
is what order the values are
- evaluated in:
let
expressionslet
expression, all the values are evaluated
- in parallel, before they are bound to their variables. This
- means that later values can't refer to earlier variables in the
- same let
block.let*
expressionslet*
block looks the same as a let
- block, except the values are evaluated one at a time, and later
- values can refer to earlier variables.Unless you have a lot of Lisp experience, you'll probably
- find let*
more intuitive.
Internally, Herbie treats intermediate values only as a - notational convenience, and inlines their values before improving - the formula's accuracy. Using intermediate variables will therefore - not produce a more accurate result or help Herbie run faster.
- -In some cases, your input program is an approximation of some
- more complex mathematical expression. The :spec
(for
- “specification”) lets you specify the more complex ideal case.
- Herbie will then try to modify the input program to make it more
- accurately evaluate the specification.
For example, suppose you want to evaluate sin(1/x)
- via a series expansion. Write:
(FPCore (x) - :spec (sin (/ 1 x)) - (+ (/ 1 x) (/ 1 (* 6 (pow x 3)))))- -
Herbie will only use the :spec
expression to
- evaluate error, not to search for accurate expressions.
By default, the arguments to formulas are assumed to be
- arbitrarily large or small floating-point numbers. However, in most
- programs a smaller range of argument values is possible.
- The :pre
property (for “precondition”) describes this
- smaller range.
Preconditions use comparison and boolean operators, just - like conditional statements:
- -(FPCore (x) :pre (< 1 x 10) (/ 1 (- x 1)))- -
Herbie is particularly efficient when when the precondition is
- an and
of ranges for each variable, but more complex
- preconditions also work.
Herbie supports both single- and double-precision values; you can
- specify the precision with the :precision
property:
binary32
binary64
racket
binary64
, but using Racket math functions
- rather than your computer's libm
.By default, binary64
is assumed. Herbie also has
- a plugin system to load additional
- precisions.
Herbie won't produce mixed-precision code unless you allow it to
- do so, using the :herbie-conversions
property:
:herbie-conversions
([prec1 prec2] ...)
prec1
, can be rewriten
- to use precision prec2
, and vice versa.All conversions are assumed to be bidirectional. For example, if
- you specify :herbie-conversions ([binary64 binary32])
,
- Herbie will be able to add conversions between single- and
- double-precision floating-point.
Herbie uses the :name
property to name FPCores in
- its UI. Its value ought to be a string.
Herbie's output provide additional information in custom - properties:
- -:herbie-status status
success
, timeout
, error
,
- or crash
.:herbie-time ms
:herbie-error-input
([pts err] ...)
:herbie-error-output
([pts err] ...)
:herbie-error-input
.Herbie's benchmark suite also uses properties such
- as :herbie-target
for continuous integration, but these
- are not officially supported and their use is discouraged.
- Herbie supports Linux, macOS, and Windows - (though, on Windows, you will need to install Make). It - can be installed from a package or from source. To start, install - Racket, which Herbie is - written in. Then install Herbie. (Herbie can also be installed - from source or via a Docker image.) -
- -- Install Racket either using - the official - installer or distro-provided packages. Versions as old as 8.2 - are supported, but more recent versions are faster. -
- -- Please note: on Linux, we recommend the official Racket installer - over installing Racket via Snap. If you must install Racket from - Snap, make sure Herbie and all packages are located in your home - directory or another allow-listed directory. -
- -- Test that Racket is installed correctly and has a correct version: -
- -racket -Welcome to Racket v8.10 [cs]. -> (exit)- -
- This installation method supports Windows, macOS, and Linux for
- x86-64. It won't work for ARM computers, including recent Apple
- computers. You may also need a working version
- of make
; on Windows, that might have to be installed
- separately.
First install Racket, as above. Then install Herbie from a package with:
- -raco pkg install --auto herbie- - - -
- This command installs Herbie and its dependencies, compiles it for
- faster startup, and places the herbie
executable in
- your Racket user path (example paths for Racket 8.10):
-
AppData\Roaming\Racket\8.10\bin
in your user folder.Library/Racket/8.10/bin
in your home folder..local/share/racket/8.10/bin
in your home directory.
- You can run herbie
from that directory, or add it to
- your executable path. Please note that the path of the binary will
- be different on Linux if you have opted to use Snap. Once Herbie
- is installed and working correctly, check out
- the tutorial.
-
- Installing Herbie from source is best if you plan to develop - Herbie or Herbie plugins, or if you are - on an ARM machine.
- -- Install Racket. - Then install Rust, using rustup or via some other means. - Versions as old as 1.60.0 are supported. -
- -- Once Racket and Rust are installed, download the Herbie source - from GitHub with: -
- -git clone https://github.com/uwplse/herbie- -
- Change to the herbie
directory;
- you should see a README.md
file, a directory named src
,
- a directory named bench/
, and a few other directories.
- Install Herbie on your system with:
-
make install- -
- This command installs Herbie and its dependencies, compiles it for
- faster startup, and places the herbie
executable in
- your Racket user path, just like the package installation.
- Once Herbie is installed and working correctly, check out
- the tutorial.
-
- Docker is a container manager, - which is sort of like a virtual machine. Herbie in Docker is more - limited; we do not recommend using Herbie through Docker without - prior Docker experience. -
- -
- The Docker documentation describes how
- to install and run the official uwplse/herbie
image.
-
The herbie
command has
- subcommands and options that influence both its user interface and
- the quality of its output.
There are a few different methods for interacting with Herbie, which we call - tools. For example, Herbie can be run both interactively or in batch mode, and - can generate output intended for the command line - or for the web. Herbie provides four of these - tools as subcommands:
- -
herbie web
herbie web
command runs Herbie on your local
- machine and opens its main page in your browser.herbie shell
herbie improve input output
herbie report input output
We recommend using report
and web
,
- which produce reports with lots of
- information about floating-point accuracy, including graphs of input values
- versus error and plots comparing cost and accuracy. This can help you
- understand whether Herbie's improvements matter for your use case.
Use herbie tool --help
to view available
- command-line options for a tool. This command also shows unsupported
- options not listed on this page.
- These options can be set on any tool. Pass them after the tool - name but before other arguments, like this: -
- -herbie report --timeout 60 in.fpcore out/- -
Arguments cannot go before options.
- ---seed S
--num-points N
--num-iters N
--num-analysis N
--num-enodes N
--timeout T
--threads N
(for the improve
and report
tools)yes
can be passed to tell Herbie to use
- all of the hardware threads.--no-pareto
The web
tool runs Herbie and connects to it from
- your browser. It has options to control the underlying web
- server.
--port N
--save-session dir
--log file
--quiet
--public
0.0.0.0
.). Essential when Herbie is run
- from Docker.
- Herbie uses rewrite rules to change programs and improve accuracy.
- The --disable rules:group
- and --enable rules:group
options turn rule
- sets on and off. In general, turning a ruleset on makes Herbie
- produce more accurate but more confusing programs.
-
The full list of rule groups is:
- -Rule Group | Topic of rewrite rules |
---|---|
arithmetic | Basic arithmetic facts |
polynomials | Factoring and powers |
fractions | Fraction arithmetic |
exponents | Exponentiation identities |
trigonometry | Trigonometric identities |
hyperbolic | Hyperbolic trigonometric identities |
bools | Boolean operator identities |
branches | if statement simplification |
special | The gamma, Bessel, and error functions |
numerics | Numerical compounds expm1 , log1p , fma , and hypot |
- These options change the types of transformations that Herbie uses - to find candidate programs. We recommend sticking to the defaults. -
- -
- Each option can be turned off with the -o
- or --disable
command-line flag and on with
- +o
or --enable
. Turning an option off
- typically results in less-accurate results, while turning a option
- on typically results in more confusing output expressions.
-
setup:search
setup:simplify
generate:rr
generate:taylor
generate:simplify
generate:proofs
reduce:regimes
reduce:avg-error
reduce:binary-search
reduce:branch-expressions
Herbie plugins define new functions, add - rewrite rules, and even implement number representations.
- -Herbie plugins are installed separately. Herbie then - automatically loads and uses them.
- -The softposit-herbie plugin implements support - for posit arithmetic. Install it - with:
- -raco pkg install --auto softposit-herbie- -
This plugin uses the SoftPosit library, only supported on Linux.
- Even then is reported to misbehave on some machines. The plugin
- support arithmetic operations, sqrt
, and quires.
Once softposit-herbie is installed,
- specify :precision posit16
to inform Herbie that it
- should assume the core's inputs and outputs are posit numbers. Other
- posit sizes (with 8 or 32 bits) and also quires (for 8, 16, and 32
- bit posits) are available, but are poorly supported.
The complex-herbie plugin has been removed as of Herbie 1.6. - This plugin may be brought back in the future. - -
The float-herbie plugin implements support for any IEEE-754 - binary floating-point number. To install, check out the - source code - and run -
- -raco pkg install- -
- at the top-level directory of the repository.
- Once float-herbie is installed,
- specify :precision (float ex nb)
- to inform Herbie that it should assume the core's inputs and outputs are
- floating-point numbers with ex exponent bits and nb total bits
- (sign bit + mantissa bits + exponent bits).
-
The fixedpoint-herbie plugin implements support for any fixed-point number. - To install, check out the - source code - and run -
- -raco pkg install- -
- at the top-level directory of the repository.
- Once fixedpoint-herbie is installed,
- specify :precision (fixed nb sc)
- to inform Herbie that it should assume the core's inputs and outputs are
- signed fixed-point numbers with nb total bits and a scaling factor of
- 2sc (integer formats have a scaling factor of 20).
- This plugin also supports unsigned fixed-point numbers specified by
- :precision (ufixed nb sc)
and provides
- simpler aliases for integer formats with :precision (integer nb)
- and :precision (uinteger nb)
.
-
The following is a guide to creating a Herbie plugin. - Plugins are considered experimental and may change considerably - between releases. - If you run into issues, please - file a bug. - Be sure to check out the - built-in plugins in the Herbie repository before getting started.
- -First Steps
-
- All plugins are implemented as Racket packages. The easiest way to
- initialize a new Racket package is to run
-
-
raco pkg new pkg-name- - in a new folder. Make sure the folder name is the same as the package name! - This will initialize a Racket package with all the necessary files. - Read the official Racket documentation on the - - raco tool for more information. - -
A single entry needs to be added to the package manifest stored in info.rkt
,
- and add (define herbie-plugin 'name)
to the bottom of the file
- where name is a unique symbol that doesn't conflict with other Herbie plugins.
- As a suggestion, this should just be the package name.
Next, edit the main.rkt
file by erasing everything except the
- language specifier on the first line, and add the line (require herbie/plugin)
.
- This gives the package access to the Herbie plugin interface.
- Optionally add the following for debugging purposes
- (eprintf "Loading pkg-name support...\n")
- directly after the require statement.
Finally, run the following in the folder containing info.rkt
- and main.rkt
:
-
-
raco pkg install- - This should install your package and check for errors. - Now everything is set up! - Of course, your plugin is empty and doesn't add any useful features. - If you added the debugging line in
main.rkt
, you should see the string
- when you run Herbie.
-
-
- Adding Features
-
- Now that you have an empty plugin, you can begin adding new functions, rewrite
- rules, and number representatons.
- The procedures exported by the Herbie plugin interface can be roughly divided into
- two categories: unique and parameterized.
- Whether or not you use the unique or parameterized half of the interface
- (or maybe both!) depends entirely on the number representation a feature is being
- implemented for.
- First, identify if your number representation is unique or parameterized.
- For example, if you are adding features for double
precision
- (or rather binary64
), the representation is unique.
- If you are adding features for a generic floating point format, say
- (float ebits nbits)
, then the representation is parameterized.
Plugin Interface (Unique)
-
- The following are the signatures and descriptions of the
- plugin procedures for unique representations.
- These procedures are required to be at the top-level of
- main.rkt
rather than inside a function.
(define-type name (exact? inexact?)
- exact->inexact inexact->exact)
- name
.
- The arguments exact?
and inexact?
- return true if a value is an exact or high-precision approximate representation.
- For Herbie's real
type, exact?
is implemented
- with real?
and inexact?
is implemented
- with bigfloat?
. The procedures exact->inexact
and
- inexact->exact
convert between exact?
- and inexact?
values.
-
-
- (define-representation (name type repr?)
- bigfloat->repr
- repr->bigfloat
- ordinal->repr
- repr->ordinal
- width
- special?)
-
-
- name
.
- The representation will inherit all rewrite rules defined for type
.
- By default, Herbie defines two types: real
and bool
.
- Your representation will most likely inherit from real
.
- The width
argument should be the bitwidth of the representation,
- e.g. 64 for binary64
.
- The argument repr?
is a procedure that accepts any argument and returns
- true if the argument is a value in the representation, e.g. an integer representation
- should use Racket's integer?
, while special?
takes a
- value in the representation and returns true if it is not finite, e.g. NaN or infinity.math/bigfloat
).
- The last two convert between a value in your representation and its corresponding ordinal value.
- Ordinal values for any representation must be within the interval [0, 2width - 1].
- Check Racket's definition of
-
- ordinals for floats.
- Note that those ordinal values can be negative.
-
-
- (define-operator (name itype-names ...) otype-name
- [bf bf-fn]
- [ival ival-fn])
-
-
- +
or sin
.
- The parameters itype-names
and otype-name
- are the input type(s) and output type names.
- For example, +
takes two real
inputs and produces
- one real
output.
- The bf-fn
argument is the
- bigfloat implementation of your operator.
- The ival-fn
argument is the Rival
- implementation of your operator. This is optional but improves the quality of Herbie's output.
- If you don't want to implement this, set ival-fn
to false
.
- To define operators with an unknown number of arguments, e.g. comparators,
- add the attribute [itype itype]
.
- This will override the input type names defined by itype-names
.
- See the bottom of this section for support for constants.
-
-
- (define-operator-impl (op name irepr-names ...) orepr-name
- [fl fl-fn]
- ...)
-
-
- op
with input representation(s) irepr-names
- and output representation orepr-name
.
- The field name
must be unique.
- For example, Herbie implements +.f64
and +.f32
- for double- and single-precision floats.
- The argument fl-fn
is the actual procedure that does the computation.
- Like define-operator
, the input representations can be
- overridden with [itype irepr]
.
- By default, the attributes bf
and ival
- are inherited from op
but can be overridden as previously
- described.
- See the bottom of this section for support for constant implementations.
-
-
- (define-ruleset name (groups ...)
- #:type ([var repr] ...)
- [rule-name match replace]
- ...)
-
-
- name
of the ruleset as well as each rule-name
- must be a unique symbol.
- Each ruleset must be marked with a set of groups
- (read here on ruleset groups).
- Each rewrite rule takes the form match ⇝ replace
where Herbie's rewriter
- will replace match
with replace
(not vice-versa).
- Each match
and replace
is an expression whose operators are
- the names of operator implementations rather than pure mathematical operators.
- Any variable must be listed in the type information with its associated representation.
- See the softposit-herbie
plugin for a more concrete example.
-
-
- (define-ruleset* name (groups ...)
- #:type ([var type] ...)
- [rule-name match replace]
- ...)
-
-
- define-ruleset
, but it defines a ruleset for every representation that
- inherits from type
.
- Currently, every type
must be the same, e.g.
- all real
, for this procedure to function correctly.
- Unlike define-ruleset
, match
and replace
- contain the names of operators rather than operator implementations.
- Procedures for declaring constants are not a part of the plugin interface.
- Instead, constants and constant implementations are defined as
- zero-argument operators and operator implementations.
- The fields fl-fn
, bf-fn
,
- and ival-fn
should be implemented with zero-argument
- procedures (thunks).
- Similar to operator and operator implementations, constants describe pure
- mathematical values like π
or e
while constant
- implementations define an approximation of those constants in a particular
- representation.
-
Plugin Interface (Parameterized)
-
- Defining operators, constants, and representations for parameterized functions requires
- a generator procedure for just-in-time loading of features for a particular
- representation.
- When Herbie encounters a representation it does not recognize (not explicitly defined
- using define-representation
) it queries a list of generators in case the
- representation requires just-in-time loading.
-
The following procedure handles represention objects:
- -(get-representation name)
The following procedures handle generators:
- -(register-generator! gen)
false
.
- (register-conversion-generator! gen)
true
if it successfully registered conversion(s)
- between the two representations.
- Conversions are one-argument operator implementations of the cast
- operator that have one representation as an input representation and
- a different representation as an output representation.
- User-defined conversions are OPTIONAL for multi-precision optimization,
- since Herbie can synthesize these by default.
- However Herbie's implementations are often slow since they are
- representation-agnostic and work for any two representations.
- In the case that your plugin does not register the requested conversion(s),
- the generator procedure need not do anything and should just return
- false
.
- - To actually add representations, operators, etc. within a generator procedure, - you must use a set of alternate procedures. -
- -
-
- (register-representation! name
- type
- repr?
- bigfloat->repr
- repr->bigfloat
- ordinal->repr
- repr->ordinal
- width
- special?)
-
-
- define-representation
, but used within generators.
-
- (register-representation-alias! name repr)
-
-
- (register-operator! op name itype-names
- otype-name attribs)
- define-operator
, but used within generators.
- The argument itype-names
is a list of the input types
- while the argument attribs
are the same attributes for
- define-operator
, e.g. bf
.
- In this case, attribs
is an association:
- (list (cons 'bf bf-fn) ...)
.
- (register-operator-impl! op name ireprs
- orepr attribs)
- define-operator-impl
, but used within generators.
- Unlike define-operator-impl
, this procedure takes representation
- objects rather than representation names for ireprs
- and orepr
.
- Use get-representation
to produce these objects.
- See register-operator!
for a description of attribs
.
- (register-ruleset! name groups
- var-repr-names rules)
- define-ruleset
, but used within generators.
- In this case, groups
is a list of rule groups;
- var-repr-names
is an association
- pairing each variable in the ruleset with its representation, e.g.
- (list (cons 'x '(float 5 16)) ...)
;
- and rules
is a list of rules of the following
- form (list (list rule-name match replace) ...)
.
- The Herbie developers are excited to announce - Herbie 2.0! This release focuses clarity, transparency, and trade-offs.
- -What is Herbie? Herbie automatically improves the accuracy - of floating point expressions. This avoids the bugs, errors, and - surprises that so often occur with floating point arithmetic. - Visit the main page to learn more about Herbie.
- - - -Join us! Join the Herbie developers on the - FPBench Slack, at the monthly - FPBench community meetings, and at - FPTalks 2023. - -
- Two years ago, Herbie 1.5 - added the --pareto mode, wherein suggested multiple - alternatives that trade off speed and accuracy. We've made this mode - faster, clearer, and more reliable, and as a result, we've made this - mode the default. Speed-accuracy trade-offs are central to numerics, - and we're excited for Herbie to help users with these trade-offs. -
- -- We've cleaned up the report page significantly. Besides a visual - redesign—we've refreshed and standardized the new fonts, - colors, and spacing—we've switched to a - new way of measuring accuracy and speed, which we think will be - more intuitive for users and avoid some misconceptions we see users - run into. -
- -- Herbie can now explain step by step how it transformed your - original input into the final program. This can help you - understand how Herbie works, and potentially help us identify bugs - or misbehaviors. More importantly, when Herbie comes up with - something truly surprising, you can now have more confidence that - the answer is correct. -
- -- We've started building - a prototype - numerics workbench, codenamed "Odyssey". This release thus - contains the beginnings of a REST - API for interacting with Herbie. Our long-term goal is an - interactive, task-oriented interface for working with - floating-point accuracy, leveraging Herbie but also potentially - other tools. A prototype is currently available in the VS Code - store as the herbie-vscode plugin. -
- -tgamma
- and lgamma
functions was rewritten to be more
- accurate (though it remains quite slow).
- - We want Herbie to be more useful to scientists, engineers, and - programmers around the world. We've got a lot of features we're - excited to work on in the coming months. Please - report bugs - or contribute. -
-If you find Herbie - useful, let us know!
- - diff --git a/www/doc/2.1/report-accuracy.png b/www/doc/2.1/report-accuracy.png deleted file mode 100644 index 44472191d..000000000 Binary files a/www/doc/2.1/report-accuracy.png and /dev/null differ diff --git a/www/doc/2.1/report-alternative-derivation.png b/www/doc/2.1/report-alternative-derivation.png deleted file mode 100644 index 89f9b7d5c..000000000 Binary files a/www/doc/2.1/report-alternative-derivation.png and /dev/null differ diff --git a/www/doc/2.1/report-alternative.png b/www/doc/2.1/report-alternative.png deleted file mode 100644 index dd71796bf..000000000 Binary files a/www/doc/2.1/report-alternative.png and /dev/null differ diff --git a/www/doc/2.1/report-cost-accuracy.png b/www/doc/2.1/report-cost-accuracy.png deleted file mode 100644 index 924c8161a..000000000 Binary files a/www/doc/2.1/report-cost-accuracy.png and /dev/null differ diff --git a/www/doc/2.1/report-error.png b/www/doc/2.1/report-error.png deleted file mode 100644 index bfb60cad1..000000000 Binary files a/www/doc/2.1/report-error.png and /dev/null differ diff --git a/www/doc/2.1/report-initial-program.png b/www/doc/2.1/report-initial-program.png deleted file mode 100644 index 605716d86..000000000 Binary files a/www/doc/2.1/report-initial-program.png and /dev/null differ diff --git a/www/doc/2.1/report-large.png b/www/doc/2.1/report-large.png deleted file mode 100644 index 3cd5dd787..000000000 Binary files a/www/doc/2.1/report-large.png and /dev/null differ diff --git a/www/doc/2.1/report-reproduce.png b/www/doc/2.1/report-reproduce.png deleted file mode 100644 index 85bc37218..000000000 Binary files a/www/doc/2.1/report-reproduce.png and /dev/null differ diff --git a/www/doc/2.1/report-step-by-step.png b/www/doc/2.1/report-step-by-step.png deleted file mode 100644 index 58309f6ad..000000000 Binary files a/www/doc/2.1/report-step-by-step.png and /dev/null differ diff --git a/www/doc/2.1/report.html b/www/doc/2.1/report.html deleted file mode 100644 index 2158e3081..000000000 --- a/www/doc/2.1/report.html +++ /dev/null @@ -1,196 +0,0 @@ - - - - - -When used in the browser, Herbie - generates HTML reports full of information about the accuracy and relative - speed of the initial and alternative expressions.
- -The top of the report page has a right-hand menu bar with - additional links. “Metrics” give you detailed internal information - about Herbie, while “Report”, if present, takes you back to the - full Herbie report.
- -Below the menu lies a brief summary of the results. Herbie can - produce multiple alternatives to the initial program, and this - summary gives their basic statistics.
- - - -Next, the specification that you gave to Herbie. This section is - closed by default. Typically, the specification is also the - initial program, but in some cases, like if - the :spec property is used, - they can differ. The specification also includes - any preconditions given to - Herbie.
- - - -You can use the drop-down in the top left to display the - specification in an alternative syntax.
- -The colored outcome bar summarizes the sampled floating-point - inputs that produce valid, unknown, or invalid outputs. Green - outcomes are valid, broken down into finite and infinite. Unknown - outputs are red. Blue outcomes are invalid (fail precondition or - domain errors) and are ignored by Herbie.
- - -- Next, the Local Percentage Accuracy graph compares the - accuracy of the initial program to Herbie's most accurate - alternative. This is helpful for understanding the sorts of inputs - Herbie is improving accuracy on. Sometimes, Herbie improved - accuracy on some inputs at the cost of accuracy on other inputs - that you care more about. You can add a - precondition to restrict Herbie to - the more important inputs in that case.
- - - -In the plot, each individual sampled point is shown with a faint - circle, and the thick line is moving average of those individual - samples. The red line is the initial program and the blue line is - Herbie's most accurate alternative.
- -Accuracy is shown on the vertical axis, and higher is better. The - horizontal axis shows one of the variables in the input program; - the dropdown in the title switches between input variables. The - checkboxes below the graph toggle the red and blue lines on and - off.
- -If Herbie decided to insert an if
statement into the
- program, the locations of those if
statements will be
- marked with vertical bars.
Next, a Pareto graph and table list the alternatives Herbie - found.
- - - -Both the plot and the table show the same data. In the plot, - accuracy is on the vertical axis and speedup is on the horizontal - axis. Up and to the right is better. The initial program is shown - with a red square, while each of Herbie's alternatives is shown with - a blue circle. A faint line shows the Pareto frontier—that is, - it goes through all Herbie alternatives that maximize speed for - their level of accuracy. Some of Herbie's alternatives may not be on - the Pareto frontier due to differences between the training and test - set.
- -In the table, each alternative is shown along with its accuracy - and speed relative to the initial program. Values are green if they - are better than the initial program, and black otherwise. Each - alternative is linked to its description lower on the page.
- -Below the table come a series of boxes detailing the initial - program and each of Herbie's alternatives, along with their - accuracy and relative speed.
- - - -The accuracy and relative speed of each alternative is given in - the title. Below the title, the alternative expression itself is - given. The dropdown in the top right can be used to change the - syntax used.
- -By definition, the speed of the initial program is 1.0×, and it - has no derivation since it was provided by the user.
- -Each alternative also has a derivation, which can be shown by - clicking on "Derivation". The derivation shows each step Herbie - took to transform the initial program into this alternative.
- - - -Each step in the derivation gives the accuracy after that step. - Sometimes you can use that to pick a less-complex and - not-substantially-less-accurate program. The derivation will also - call out any time the input is split into cases. When a part of - the step is colored blue, that identifies the changed part of the - expression.
- -Derivations may also contain "step-by-step derivations"; you can - click on those step-by-step derivations to expand them. Each step in - the step-by-step derivation names an arithmetic law from Herbie's - database, with metadata-eval meaning that Herbie used - direct computation in a particular step.
- - - -Finally, Herbie gives a command to reproduce that result. If you - find a Herbie bug, include this code snippet when - filing an issue.
- - - -We expect the report to grow more informative with future - versions. Please get in - touch if there is more information you'd like to see.
- - - - diff --git a/www/doc/2.1/specification.png b/www/doc/2.1/specification.png deleted file mode 100644 index 774149989..000000000 Binary files a/www/doc/2.1/specification.png and /dev/null differ diff --git a/www/doc/2.1/system-1.6-changes.png b/www/doc/2.1/system-1.6-changes.png deleted file mode 100644 index aa6efb805..000000000 Binary files a/www/doc/2.1/system-1.6-changes.png and /dev/null differ diff --git a/www/doc/2.1/system-1.6.png b/www/doc/2.1/system-1.6.png deleted file mode 100644 index e36ef55c0..000000000 Binary files a/www/doc/2.1/system-1.6.png and /dev/null differ diff --git a/www/doc/2.1/team.png b/www/doc/2.1/team.png deleted file mode 100644 index be7c3befb..000000000 Binary files a/www/doc/2.1/team.png and /dev/null differ diff --git a/www/doc/2.1/toc.js b/www/doc/2.1/toc.js deleted file mode 100644 index d1f1a1671..000000000 --- a/www/doc/2.1/toc.js +++ /dev/null @@ -1,22 +0,0 @@ -function make_toc() { - var headings = document.querySelectorAll("h2"); - var toc = document.createElement("nav"); - toc.classList.add("toc") - var list = document.createElement("ul"); - for (var i = 0; i < headings.length; i++) { - var li = document.createElement("li"); - var a = document.createElement("a"); - var h = headings[i]; - if (! h.id) { - h.setAttribute("id", "heading-" + i); - } - a.setAttribute("href", "#" + h.id); - a.innerHTML = h.innerHTML; - li.appendChild(a); - list.appendChild(li); - } - toc.appendChild(list); - headings[0].parentNode.insertBefore(toc, headings[0]); -} - -window.addEventListener("load", make_toc); diff --git a/www/doc/2.1/tutorial.html b/www/doc/2.1/tutorial.html deleted file mode 100644 index cd7232fd5..000000000 --- a/www/doc/2.1/tutorial.html +++ /dev/null @@ -1,328 +0,0 @@ - - - - -- Herbie rewrites floating point expressions to - make them more accurate. Floating point arithmetic is - inaccurate; even 0.1 + 0.2 ≠ 0.3 in - floating-point. Herbie helps find and fix these mysterious - inaccuracies. -
- -- To get started, download and install - Herbie. You're then ready to begin using it. -
- -Start Herbie with:
- -herbie web- -
- After a brief wait, your web browser should open and show you - Herbie's main window. The most important part of the page is this - bit: -
- - - -
- Let's start by just looking at an example of Herbie running.
- Click "Show an example". This will pre-fill the expression
- sqrt(x + 1) - sqrt(x)
- with x
ranging from to 0 and 1.79e308.
-
- Now that you have an expression and a range for each variable, - click the "Improve with Herbie" button. You should see the entry - box gray out, and shortly thereafter some text should appear - describing what Herbie is doing. After a few seconds, you'll be - redirected to a page with Herbie's results. -
- -- The very top of this results page gives some quick statistics - about the alternative ways Herbie found for evaluating this - expression: -
- - - -- Here, you can see that Herbie's most accurate alternative has an - accuracy of 99.7%, much better than the initial program's 53.2%, - and that in total Herbie found 5 alternative. One of those - alternatives is both more accurate than the original expression - and also 1.9× faster. The rest of the - result page shows each of these alternatives, including - details like how they were derived. These details are all - documented, but for the sake of the - tutorial let's move on to a more realistic example. -
- -- You can use Herbie on expressions from source code, mathematical - models, or debugging tools. But most users use Herbie as they - write code, passing any complex floating-point tool to Herbie as - they go. Herbie has options to log all - the expressions you enter so that you can refer to them later. -
- -But to keep the tutorial focused, let's suppose you're instead - tracking down a floating-point bug in existing code. Then you'll - need to start by identifying the problematic floating-point - expression.
- -To demonstrate the workflow, let's walk through - bug 208 - in math.js, a math library for - JavaScript. The bug deals with inaccurate square roots for complex - numbers. (For a full write-up of the bug itself, check out - a blog - post by one of the Herbie authors.) -
- -- In most programs, there's a small core that does the mathematical - computations, while the rest of the program sets up parameters, - handles control flow, visualizes or prints results, and so on. The - mathematical core is what Herbie will be interested in. -
- -
- For our example, let's start
- in lib/function/
.
- This directory contains many subdirectories; each file in each
- subdirectory defines a collection of mathematical functions. The
- bug we're interested in is about complex square root, which is
- defined in
- arithmetic/sqrt.js
.
-
- This file handles argument checks, five different number types,
- and error handling, for both real and complex square roots. None
- of that is of interest to Herbie; we want to extract just the
- mathematical core. So skip down to the isComplex(x)
- case:
-
var r = Math.sqrt(x.re * x.re + x.im * x.im); -if (x.im >= 0) { - return new Complex( - 0.5 * Math.sqrt(2.0 * (r + x.re)), - 0.5 * Math.sqrt(2.0 * (r - x.re)) - ); -} -else { - return new Complex( - 0.5 * Math.sqrt(2.0 * (r + x.re)), - -0.5 * Math.sqrt(2.0 * (r - x.re)) - ); -}- -
This is the mathematical core that we want to send to Herbie.
- -
- In this code, x
is of type Complex
, a
- data structure with multiple fields. Herbie only deals with
- floating-point numbers, not data structures, so we will treat the
- input x
as two separate inputs to
- Herbie: xre
and xim
. We'll also pass
- each field of the output to Herbie separately.
-
- This code also branches between non-negative x.im
and
- negative x.im
. It's usually better to send each
- branch to Herbie separately. So in total, this code turns into four
- Herbie inputs: two output fields, for each of the two branches.
-
Let's focus on the first field of the output for the case of
- non-negative x.im
.
The variable r
is an intermediate variable in this
- code block. Intermediate variables provide Herbie with crucial
- information that Herbie can use to improve accuracy, so you want to
- expand or inline them. The result looks like this:
0.5 * sqrt(2.0 * (sqrt(xre * xre + xim * xim) + xre))- -
Recall that this code is only run when x.im
is
- non-negative (but it runs for all values of x.re
). So,
- select the full range of values for x.re
, but restrict
- the range of x.im
, like this:
-
-
-
- This asks Herbie to consider only non-negative
- values of xim
when improving the accuracy of this
- expression.
Herbie will churn for a few seconds and produce a results page. - In this case, Herbie found 4 alternatives, and we're interested in - the most accurate one, which should have an - accuracy of 84.6%:
- - - -Below these summary statistics, we can see a graph of accuracy
- versus input value. By default, it shows accuracy
- versus xim
; higher is better:
The drop in accuracy once xim
is bigger than
- about 1e150
really stands out, but you can also see
- that Herbie's alternative more accurate for smaller xim
- values, too. You can also change the graph to plot accuracy
- versus xre
instead:
This plot makes it clear that Herbie's alternative is almost
- perfectly accurate for positive xre
, but still has some
- error for negative xre
.
-
-
Herbie also found other alternatives, which are less accurate but - might be faster. You can see a summary in this table:
- - - -Herbie's algorithm is randomized, so you likely won't see the - exact same thing; you might see more or fewer alternatives, and they - might be more or less accurate and fast. That said, the most - accurate alternative should be pretty similar.
- -That alternative itself is shown lower down on the page:
- - - -A couple features of this alternative stand out immediately.
- First of all, Herbie inserted an if
statement.
- This if
statement handles a phenomenon known as
- cancellation, and is part of why Herbie's alternative is more
- accurate. Herbie also replaced the square root operation with
- the hypot
function, which computes distances more
- accurately than a direct square root operation.
If you want to see more about how Herbie derived this result, you - could click on the word "Derivation" to see a detailed, step-by-step - explanation of how Herbie did it. For now, though, let's move on to - look at another alternative.
- -The fifth alternative suggested by Herbie is much less accurate, - but it is about twice as fast as the original program:
- - - -This alternative is kind of strange: it has two branches, and
- each one only uses one of the two variables xre
- and xim
. That explains why it's fast, but it's still
- more accurate than the initial program because it avoids
- cancellation and overflow issues that plagued the original.
In this case, we were interested in the most accurate possible - implementation, so let's try to use Herbie's most accurate - alternative.
- --// Herbie version of 0.5 * sqrt(2.0 * (sqrt(xre*xre + xim*xim) + xre)) -var r = Math.hypot(x.re, x.im); -var re; -if (xre + r <= 0) { - re = 0.5 * Math.sqrt(2 * (x.im / (x.re / x.im) * -0.5)); -} else { - re = 0.5 * Math.sqrt(2 * (x.re + r)); -} -if (x.im >= 0) { - return new Complex( - re, - 0.5 * Math.sqrt(2.0 * (r - x.re)) - ); -} -else { - return new Complex( - 0.5 * Math.sqrt(2.0 * (r + x.re)), - -0.5 * Math.sqrt(2.0 * (r - x.re)) - ); -}- -
Note that I've left the Herbie query in a comment. As Herbie - gets better, you can re-run it on this original expression to see if - it comes up with improvements in accuracy.
- -By the way, for some languages, including JavaScript, you can use - the drop-down in the top-right corner of the alternative block to - translate Herbie's output to that language. However, you will - still probably need to refactor and modify the results to fit your - code structure, just like here.
- -With this change, we've made this part of the complex square - root function much more accurate, and we could repeat the same steps - for the other branches and other fields in this program. You now - have a pretty good understanding of Herbie and how to use it. - Please let us know if - Herbie has helped you, and check out - the documentation to learn more about - Herbie's various options and outputs.
- - - diff --git a/www/doc/2.1/using-cli.html b/www/doc/2.1/using-cli.html deleted file mode 100644 index 123144fb3..000000000 --- a/www/doc/2.1/using-cli.html +++ /dev/null @@ -1,97 +0,0 @@ - - - - -Herbie can be used from the command-line or - from the browser. This page covers - using Herbie from the command line.
- -- The Herbie shell lets you interact with Herbie: you type in input - expressions and Herbie prints their more accurate versions. Run - the Herbie shell with this command: -
- -herbie shell -Herbie 2.0 with seed 2098242187 -Find help on https://herbie.uwplse.org/, exit with Ctrl-D -herbie>- - -
- Herbie prints a seed, which you can use to - reproduce a Herbie run, and links you to documentation. Then, - it waits for inputs, which you can type directly into your - terminal in FPCore format: -
- -herbie> (FPCore (x) (- (+ 1 x) x)) -(FPCore - (x) - ... - 1)- -
Herbie suggests that 1
is more accurate than the
- original expression (- (+ 1 x) x)
. The
- the ... elides
- additional information provided
- by Herbie.
The Herbie shell only shows Herbie's most accurate variant.
- -- Alternatively, you can run Herbie on a file with multiple - expressions in it, writing Herbie's versions of each to a file. - This mode is intended for use by scripts. -
- -herbie improve bench/tutorial.fpcore out.fpcore -Starting Herbie on 3 problems (seed: 1551571787)... - 1/3 [ 0.882s] 30→ 0 Cancel like terms -Warning: 24.7% of points produce a very large (infinite) output. -You may want to add a precondition. -See <https://herbie.uwplse.org/doc/2.0/faq.html#inf-points> for more. - 2/3 [ 1.721s] 29→ 0 Expanding a square - 3/3 [ 2.426s] 0→ 0 Commute and associate- -
- The output file out.fpcore
contains more accurate
- versions of each program:
-
;; seed: 1551571787 - -(FPCore (x) ... 1) -(FPCore (x) ... (* x (- x -2))) -(FPCore (x y z) ... 0)- -
- Note that output file is in the same order as the input file. For - more control over Herbie, see the documentation of - Herbie's command-line options. -
- - - diff --git a/www/doc/2.1/using-web.html b/www/doc/2.1/using-web.html deleted file mode 100644 index 6ca1596cf..000000000 --- a/www/doc/2.1/using-web.html +++ /dev/null @@ -1,117 +0,0 @@ - - - - -- Herbie rewrites floating point expressions to - make them more accurate. Herbie can be used - from the command-line or from the - browser; this page is about using Herbie from the browser.
- - -- The Herbie web shell lets you interact with Herbie through your - browser, featuring a convenient input format. The web shell is the - friendliest and easiest way to use Herbie. Run the Herbie web - shell with this command: -
- -herbie web- -
After a few seconds, the web shell will rev up and direct your - browser to Herbie:
- -herbie web -Herbie 2.0 with seed 1003430182 -Find help on https://herbie.uwplse.org/, exit with Ctrl-C -Your Web application is running at http://localhost:8000/. -Stop this program at any time to terminate the Web Server.- - - -
You can type an input expressions in - standard mathematical syntax. After typing in an - expression, you will be asked to specify the range of values for each input - variable that Herbie should consider when trying to improve the expression. - Hit the "Improve with Herbie" button once you're done to run Herbie. -
- -- The web shell reports Herbie's progress and redirects to a - report once Herbie is done. -
- -- The web shell can also automatically save the generated reports, - and has many other options you might - want to explore. -
- - -A report can also be generated directly - from a file of input expressions in FPCore format:
- -herbie report bench/tutorial.fpcore output/ -Starting Herbie on 3 problems (seed: 770126425)... -Warning: 25.0% of points produce a very large (infinite) output. -You may want to add a precondition. -See https://herbie.uwplse.org/doc/latest/faq.html#inf-points for -more. - 1/3 [ 0.703s] 29→ 0 Expanding a square - 2/3 [ 1.611s] 0→ 0 Commute and associate - 3/3 [ 0.353s] 30→ 0 Cancel like terms- -
- This command asks generates a report from the input expressions
- in bench/tutorial.fpcore
and saves the report in the
- directory output/
. It's best if that directory
- doesn't exist before running this command, because otherwise
- Herbie may overwrite files in that directory.
-
- Occasionally you may also see Herbie emit warnings as shown above. - All of Herbie's warnings are listed, with explanations, in - the FAQ. -
- -
- Once generated, open output/index.html
in your
- favorite browser (but see the FAQ if you're
- using Chrome). That page summarizes Herbie's results for all
- expression in your input file, and you can click on individual
- expressions to see their report.
-
Batch report generation is the most informative way to run Herbie - on a large collection of inputs. Like the web shell, it can be - customized through command-line options, - including parallelizing Herbie with multiple threads.
- - - - diff --git a/www/doc/2.1/web-input.png b/www/doc/2.1/web-input.png deleted file mode 100644 index 5eb186332..000000000 Binary files a/www/doc/2.1/web-input.png and /dev/null differ diff --git a/www/doc/2.1/web-main.png b/www/doc/2.1/web-main.png deleted file mode 100644 index e8ac842ab..000000000 Binary files a/www/doc/2.1/web-main.png and /dev/null differ