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 (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)))))) - exprexpr 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 @@ - - - - - Herbie HTTP API Endpoints - - - - - -
-

HTTP API

- - -
- -

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.

- -

Format for all endpoints

- -

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
-    
- -

/api/sample

- -
- Example input & output - -

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.

- -

/api/exacts

- -
- Example input & output - -

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.

- -

/api/calculate

- -
- Example inputs & outputs - -

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].

- -

/api/analyze

- -
- Example inputs & outputs - -

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.

- -

/api/alternatives

- -
- Example inputs & outputs -

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.

- -

/api/mathjs

- -
- Example inputs & outputs -

Request:

- -
{
-  formula: <FPCore expression>
-}
- -

Response:

- -
{
-  mathjs: <mathjs expression>
-}
-
- -

The mathjs endpoint allows the user to translate - FPCore expressions into mathjs expressions.

- -

/api/local-error

- Forthcoming. - - - diff --git a/www/doc/2.1/diagrams.html b/www/doc/2.1/diagrams.html deleted file mode 100644 index 38ff22f2b..000000000 --- a/www/doc/2.1/diagrams.html +++ /dev/null @@ -1,41 +0,0 @@ - - - - - Diagrams - - - - - -
-

Diagrams

- - -
- -
- System diagram of Herbie -
- -

- 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 on Docker - - - - - -
-

Installing with Docker

- - -
- -

- 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. -

- -

Installing Herbie via Docker

- -

- 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.

- -

Running the web interface

- -

- 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. -

- -

Generating files and reports

- -

- 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. -

- -

Building the Docker image

- -

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.

- - - diff --git a/www/doc/2.1/egg-rr-seed-variance.png b/www/doc/2.1/egg-rr-seed-variance.png deleted file mode 100644 index a5322710b..000000000 Binary files a/www/doc/2.1/egg-rr-seed-variance.png and /dev/null differ diff --git a/www/doc/2.1/error.html b/www/doc/2.1/error.html deleted file mode 100644 index 1084db3f6..000000000 --- a/www/doc/2.1/error.html +++ /dev/null @@ -1,184 +0,0 @@ - - -Herbie Input Format - - - - -
-

What is Error?

- - -
- -

- 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? -

- -

The summary

- -

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.

- -

Why rounding matters

- -

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.

- -

Bits of error

- -

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.

- -

Percentage accuracy

- -

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.

- -

Valid inputs

- -

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. An output can fail to exist for an input if that input does - something like divide by zero or take the square root of a - negative number. Then that input is invalid.
  2. -
  3. An input can fail to satisfy the user's precondition. - Preconditions can be basically anything, but most often they - specify a range of inputs. For example, if the precondition - is (< 1 x 2), then the input x = 3 is - invalid.
  4. -
  5. Finally, and most rarely, Herbie can fail to compute the output - for a particular input. For example, the computation (/ (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.
  6. -
- -

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.

- -

Sampling inputs

- -

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.

diff --git a/www/doc/2.1/faq.html b/www/doc/2.1/faq.html deleted file mode 100644 index f4f79edff..000000000 --- a/www/doc/2.1/faq.html +++ /dev/null @@ -1,143 +0,0 @@ - - - - - Herbie FAQ - - - - - -
-

Common Errors and Warnings

- - -
- -

Herbie automatically transforms floating - point expressions into more accurate forms. This page troubleshoots - common Herbie errors, warnings, and known issues.

- - -

Common errors

- -

- Herbie error messages refer to this second for additional - information and debugging tips. -

- -

Invalid syntax

- -

- 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. -

- -

Cannot sample enough valid points

- -

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. -

- -

No valid values

- -

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.

- - -

Common warnings

- -

Herbie warnings refer to this section for explanations and common - actions to take.

- -

Infinite outputs for N% of points.

- -

- 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. -

- -

Could not determine a ground truth

- -

- 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. -

- -

Could not uniquely print val

- -

- 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. -

- -

Unsound rule application detected

- -

- 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. -

- -

Unused variable var

- -

- The input FPCore contains a variable that is not - used in the body expression. -

- -

Strange variable var

- -

- The input expression contains a variable that is similar in name - to named constants, e.g. e instead of E. -

- -

Known bugs

- -

Bugs that cannot be directly fixed are documented in this section.

- -

Missing reports chart on Chrome

- -

- 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. -

- - - diff --git a/www/doc/2.1/input.html b/www/doc/2.1/input.html deleted file mode 100644 index 55e7b6583..000000000 --- a/www/doc/2.1/input.html +++ /dev/null @@ -1,257 +0,0 @@ - - - - - Herbie Input Format - - - - - -
-

The Input Format

- - -
- -

- Herbie uses - the FPCore format to specify an - input program, and has extensive options for precisely describing - its context. -

- -

Math format

- -

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.

- -

FPCore format

- -

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. -

- -

Supported functions

- -

- Herbie supports all functions - from math.h - with floating-point-only inputs and outputs. The best supported - functions include: -

- -
-
+, -, *, /, fabs
-
The usual arithmetic functions
-
sqrt, cbrt
-
Square and cube roots
-
pow, exp, log
-
Various exponentiations and logarithms
-
sin, cos, tan
-
The trigonometric functions
-
asin, acos, atan, atan2
-
The inverse trigonometric functions
-
sinh, cosh, tanh
-
The hyperbolic functions
-
asinh, acosh, atanh
-
The inverse hyperbolic functions
-
fma, expm1, log1p, hypot
-
Specialized numeric functions
-
- -

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.

- -

Conditionals

- -

FPCore uses if for conditional expressions:

- -
(if cond if-true if-false)
- -

- The conditional cond may use: -

- -
-
==, !=, <, >, <=, >=
-
The usual comparison operators
-
and, or, not
-
The usual logical operators
-
TRUE, FALSE
-
The two boolean values
-
- -

The comparison functions support chained comparisons with more than two arguments.

- -

Intermediate variables

- -

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 expressions
-
In a let 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* expressions
-
A let* 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.

- -

Specifications

- -

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.

- -

Preconditions

- -

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.

- -

Precisions

- -

Herbie supports both single- and double-precision values; you can - specify the precision with the :precision property:

- -
-
binary32
-
Single-precision IEEE-754 floating point
-
binary64
-
Double-precision IEEE-754 floating point
-
racket
-
Like 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] ...)
-
Expressions in precision 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.

- -

Miscellaneous Properties

- -

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
-
status describes whether Herbie worked: it is one - of success, timeout, error, - or crash.
-
:herbie-time ms
-
The time, in milliseconds, used by Herbie to find a more accurate formula.
-
:herbie-error-input
([pts err] ...)
-
The average error of the input program at pts points. Multiple entries correspond to Herbie's training and test sets.
-
:herbie-error-output
([pts err] ...)
-
The computed average error of the output program, similar to :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.

- - - diff --git a/www/doc/2.1/installing.html b/www/doc/2.1/installing.html deleted file mode 100644 index c1e424d84..000000000 --- a/www/doc/2.1/installing.html +++ /dev/null @@ -1,148 +0,0 @@ - - - - - - Installing Herbie - - - - - - -
-

Installing Herbie

- - -
- -

- 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.) -

- -

Installing Racket

- -

- 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)
- -

Installing Herbie from a package

- -

- 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): -

- - - -

- 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

- -

- 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. -

- -

Installing Herbie with Docker

- -

- 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. -

- - - - diff --git a/www/doc/2.1/interactive-preconditions.png b/www/doc/2.1/interactive-preconditions.png deleted file mode 100644 index bc512e1c1..000000000 Binary files a/www/doc/2.1/interactive-preconditions.png and /dev/null differ diff --git a/www/doc/2.1/old-rr-seed-variance.png b/www/doc/2.1/old-rr-seed-variance.png deleted file mode 100644 index a446095b9..000000000 Binary files a/www/doc/2.1/old-rr-seed-variance.png and /dev/null differ diff --git a/www/doc/2.1/options.html b/www/doc/2.1/options.html deleted file mode 100644 index 0dcb07edb..000000000 --- a/www/doc/2.1/options.html +++ /dev/null @@ -1,272 +0,0 @@ - - - - - Herbie Command-line Options - - - - - -
-

Command-line Options

- - -
- -

The herbie command has - subcommands and options that influence both its user interface and - the quality of its output.

- -

Herbie commands

- -

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
-
Use Herbie through your browser. - The herbie web command runs Herbie on your local - machine and opens its main page in your browser.
- -
herbie shell
-
Use Herbie via a command-line shell. - Enter an FPCore expression and Herbie - will print its more-accurate version.
- -
herbie improve input output
-
Run Herbie on the expressions in the file or - directory input. The results are written - to output, a single file in FPCore format.
- -
herbie report input output
-
Run Herbie on the expressions in the file or - directory input. The results are written - to output, a directory of - HTML reports. These pages can be viewed - in any browser (though with a quirk - for Chrome).
-
- -

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.

- -

General options

- -

- 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
-
The random seed, which changes the randomly-selected points - that Herbie evaluates candidate expressions on. The seed is a - number between 0 and 231 (exclusive both ends). This - option can be used to make Herbie's results reproducible or to - compare two different runs. Seeds are not preserved across - runs.
- -
--num-points N
-
The number of input points Herbie uses to evaluate candidate - expressions. The default, 256, is a good balance for most - programs. Increasing this option, say to 512 or 1024, will slow - Herbie down but may make its results more consistent.
- -
--num-iters N
-
The number of times Herbie attempts to improve accuracy. The - default, 4, suffices for most programs and helps keep Herbie - fast; in practice iterations beyond the first few rarely lead to - lower error. Increase this option, say to 6, to check that there - aren't further improvements that Herbie could seek out.
- -
--num-analysis N
-
The number of input subdivisions to use when searching for - valid input points. The default is 12. Increasing this option - will slow Herbie down, but may fix the - "Cannot sample enough - valid points" error.
- -
--num-enodes N
-
The number of equivalence graph nodes to use when doing - algebraic reasoning. The default is 8000. Increasing this option - will slow Herbie down, but may improve results slightly.
- -
--timeout T
-
The timeout to use per-input, in seconds. A fractional number - of seconds can be given.
- -
--threads N (for the improve and report tools)
-
Enables multi-threaded operation. By default, no threads are - used. A number can be passed to this option to use that many - threads, or yes can be passed to tell Herbie to use - all of the hardware threads.
- -
--no-pareto
-
Disables cost-aware search. Herbie will only return a single - program, which optimizes exclusively for accuracy. Herbie will be - slightly faster as a result.
-
- -

Web shell options

- -

The web tool runs Herbie and connects to it from - your browser. It has options to control the underlying web - server.

- -
-
--port N
-
The port the Herbie server runs on. The default port is 8000.
- -
--save-session dir
-
Save all the reports to this directory. The directory also - caches previously-computed expressions.
- -
--log file
-
Write an access log to this file, formatted like an Apache - log. This log does not contain crash tracebacks.
- -
--quiet
-
By default, but not when this option is set, a browser is - automatically started to show the Herbie page. This option also - shrinks the text printed on start up.
- -
--public
-
When set, users on other computers can connect to the demo and - use it. (In other words, the server listens - on 0.0.0.0.). Essential when Herbie is run - from Docker.
-
- -

Rulesets

- -

- 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 GroupTopic of rewrite rules
arithmeticBasic arithmetic facts
polynomialsFactoring and powers
fractionsFraction arithmetic
exponentsExponentiation identities
trigonometryTrigonometric identities
hyperbolicHyperbolic trigonometric identities
boolsBoolean operator identities
branchesif statement simplification
specialThe gamma, Bessel, and error functions
numericsNumerical compounds expm1, log1p, fma, and hypot
- -

Search options

- -

- 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
-
This option, on by default, uses interval subdivision search - to help compute ground truth for complicated expressions. If - turned off, Herbie will be slightly faster, but may hit the - "Cannot sample enough valid - points" error more often. Instead of turning this option off, - you may want to adjust the --num-analysis flag - instead.
- -
setup:simplify
-
This option, on by default, simplifies the expression before - starting the Herbie improvement loop. If turned off, Herbie's - results will likely be somewhat worse, but its output program may - be more similar to the input program.
- -
generate:rr
-
This option, on by default, uses Herbie's recursive rewriting - algorithm to generate candidate programs. If turned off, Herbie - will use a non-recursive rewriting algorithm, which will - substantially limit Herbie's creativity.
- -
generate:taylor
-
This option, on by default, uses series expansion to produce - new candidates during the main improvement loop. If turned off, - Herbie will not use series expansion. If turned off, Herbie's - results will more likely be algebraically equivalent to the input - expression, but may be less accurate.
- -
generate:simplify
-
This option, on by default, simplifies candidates during the - main improvement loop. If turned off, candidates will not be - simplified, which typically results in much less accurate - expressions.
- -
generate:proofs
-
This option, on by default, generates step-by-step derivations - for HTML reports. If turned off, the step-by-step derivations will - be absent, and Herbie will be slightly faster.
- -
reduce:regimes
-
This option, on by default, uses Herbie's regime inference - algorithm to branch between several program candidates. If turned - off, branches will not be inferred and the output program will be - straight-line code (if the input was). Turn this option off if - your programming environment makes branches very expensive, such - as on a GPU.
- -
reduce:avg-error
-
This option, on by default, causes Herbie to output the - candidate with the best average error over the chosen inputs. If - turned off, Herbie will choose the candidate with the least - maximum error instead. This usually produces programs with worse - overall accuracy. Turn this option off if worst-case accuracy is - more important to you than overall accuracy.
- -
reduce:binary-search
-
This option, on by default, uses binary search to refine the - values used in inferred branches. If turned off, different runs of - Herbie will be less consistent, and accuracy near branches will - suffer.
- -
reduce:branch-expressions
-
This option, on by default, allows Herbie to branch on - expressions, not just variables. This slows Herbie down, - particularly for large programs. If turned off, Herbie will only - try to branch on variables.
-
- - - diff --git a/www/doc/2.1/pareto-screenshot.png b/www/doc/2.1/pareto-screenshot.png deleted file mode 100644 index 79e0769a0..000000000 Binary files a/www/doc/2.1/pareto-screenshot.png and /dev/null differ diff --git a/www/doc/2.1/plugins.html b/www/doc/2.1/plugins.html deleted file mode 100644 index b589bef0f..000000000 --- a/www/doc/2.1/plugins.html +++ /dev/null @@ -1,444 +0,0 @@ - - - - - Herbie Plugins - - - - - -
-

Plugins

- - -
- -

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.

- -

Posit arithmetic

- -

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.

- - -

Complex numbers

- -

The complex-herbie plugin has been removed as of Herbie 1.6. - This plugin may be brought back in the future. - -

Generic floating-point numbers

- -

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). -

- -

Generic fixed-point numbers

- -

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). -

- -

Developing plugins

- -

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) -
-
Adds a new type with the unique identifier 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?)
-
-
-
Adds a new representation with the unique identifier 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.

- - The other four arguments are single-argument procedures that implement different conversions. - The first two convert between a value in your representation and a Racket - bigfloat - (you need to import 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]) -
-
-
-
Adds a new operator. Operators describe pure mathematical functions, - i.e. + 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]
...)
-
-
-
Implements 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]
...)
-
-
-
Defines a set of rewrite rules. - The 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]
...)
-
-
-
Like 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)
-
Takes a representation name and returns a representation object. - Do not call this function before the associated representation has been registered! -
-
- -

The following procedures handle generators:

- -
-
(register-generator! gen)
-
Adds a representation generator procedure to Herbie's set of generators. - Representation generator procedures take the name of a representation and - return the associated representation object if it successfully created the - operators, constants, and rules for that representation. - In the case that your plugin does not register the requested representation, - the generator procedure need not do anything and should just return - false. -
-
- -
-
(register-conversion-generator! gen)
-
Adds a conversion generator procedure to Herbie's set of generators. - Conversion generator procedures take the names of two representations - and returns 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?)
-
-
-
Like define-representation, but used within generators.
- -
- - - -
(register-representation-alias! name repr)
-
-
-
Adds an alias name for an existing representation repr. - If two representations are equivalent, e.g. (float 8 32) and binary32, - this procedure can be used to declare the two representations equivalent. -
- -
- (register-operator! op name itype-names - otype-name attribs) -
-
Like 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) -
-
Like 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) -
-
Like 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) ...). -
- -
- - - diff --git a/www/doc/2.1/problematic-highlight.png b/www/doc/2.1/problematic-highlight.png deleted file mode 100644 index 7eb6afb27..000000000 Binary files a/www/doc/2.1/problematic-highlight.png and /dev/null differ diff --git a/www/doc/2.1/problematic-improved-accuracy.png b/www/doc/2.1/problematic-improved-accuracy.png deleted file mode 100644 index 64910f58b..000000000 Binary files a/www/doc/2.1/problematic-improved-accuracy.png and /dev/null differ diff --git a/www/doc/2.1/problematic-improved-speed.png b/www/doc/2.1/problematic-improved-speed.png deleted file mode 100644 index ad14244e2..000000000 Binary files a/www/doc/2.1/problematic-improved-speed.png and /dev/null differ diff --git a/www/doc/2.1/problematic-pareto-table.png b/www/doc/2.1/problematic-pareto-table.png deleted file mode 100644 index b5fb80aac..000000000 Binary files a/www/doc/2.1/problematic-pareto-table.png and /dev/null differ diff --git a/www/doc/2.1/problematic-xim.png b/www/doc/2.1/problematic-xim.png deleted file mode 100644 index 3714db44f..000000000 Binary files a/www/doc/2.1/problematic-xim.png and /dev/null differ diff --git a/www/doc/2.1/problematic-xre.png b/www/doc/2.1/problematic-xre.png deleted file mode 100644 index 9ccac6c1a..000000000 Binary files a/www/doc/2.1/problematic-xre.png and /dev/null differ diff --git a/www/doc/2.1/quadp-old-branch.png b/www/doc/2.1/quadp-old-branch.png deleted file mode 100644 index 1e0c9fe83..000000000 Binary files a/www/doc/2.1/quadp-old-branch.png and /dev/null differ diff --git a/www/doc/2.1/quadp-short-branch.png b/www/doc/2.1/quadp-short-branch.png deleted file mode 100644 index cb60d12cc..000000000 Binary files a/www/doc/2.1/quadp-short-branch.png and /dev/null differ diff --git a/www/doc/2.1/range-input-2.png b/www/doc/2.1/range-input-2.png deleted file mode 100644 index 70f14c7b2..000000000 Binary files a/www/doc/2.1/range-input-2.png and /dev/null differ diff --git a/www/doc/2.1/range-input.png b/www/doc/2.1/range-input.png deleted file mode 100644 index 68831dcbc..000000000 Binary files a/www/doc/2.1/range-input.png and /dev/null differ diff --git a/www/doc/2.1/release-notes.html b/www/doc/2.1/release-notes.html deleted file mode 100644 index 87350ed58..000000000 --- a/www/doc/2.1/release-notes.html +++ /dev/null @@ -1,153 +0,0 @@ - - - - - Herbie 2.0 Release Notes - - - - - - -
-

Herbie 2.0 Release Notes

- - -
- -

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.

- - The Herbie 2.0 team at UW and U of U - -

Join us! Join the Herbie developers on the - FPBench Slack, at the monthly - FPBench community meetings, and at - FPTalks 2023. - -

Speed-accuracy trade-offs

- -
- The Accuracy vs Speed section of a Herbie report, which has an accuracy vs speedup Pareto plot on the left and a tabular view of the accuracy and speed of each of Herbie's alternatives on the right. -
- Herbie's new Accuracy vs Speed view, showing how multiple - alternatives found by Herbie compare on these different axes. -
-
- -

- 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. -

- -

New Metrics and Redesign

- -
- The metrics shown at the top of each Herbie report: percentage accurate, time, alternatives, and speedup. -
- The metrics now being showcased on a Herbie results page: - percentage accuracy replaces the old "bits of error" metric, - while "speedup" now highlights the speed of the fastest - alternative found by Herbie that is also more accurate than the - initial program. -
-
- -

- 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. -

- -

Derivations

- -
- The derivation section shown for each alternative produced by Herbie, which show step by step how the initial program was transformed into the alternative. -
- New "Step-by-step derivation" buttons show how a transformation - was done by Herbie, with each step annotated with its mathematical - axiom from Herbie's database. -
-
- -

- 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. -

- -

Foundations for a Herbie Workbench

- -

- 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. -

- -

Other improvements

- - -

Try it out!

- -

- 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 @@ - - - - - - Herbie reports - - - - - - -
-

Herbie reports

-
- -
- -

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.

- -
- -
Summary numbers from a Herbie report.
-
- -
-
Percentage Accurate
-
The percentage accuracy of the - initial program and what Herbie thinks is its most accurate - alternative.
-
Time
-
The time it took Herbie to generate all of the alternatives.
-
Alternatives
-
The number of alternatives found.
-
Speedup
-
The speed of the fastest alternative that is more accurate - than the initial program, relative to the initial program.
-
- -

Specification

- -

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.

- - -

Local Percentage Accuracy graph

- -

- 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.

- -

Accuracy vs Speed

-

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.

- -

Initial program and Alternatives

- -

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.

- -
- -
- -

Reproduction

- -

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 Tutorial - - - - -
-

Herbie Tutorial

- - -
- -

- 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. -

- -

Giving Herbie expressions

- -

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: -

- -
- The program input field in the Herbie web UI. -
- -

- 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. -

- -
- The input range field in the Herbie web UI. -
- -

- 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: -

- -
- Statistics and error measures for this Herbie run. -
- -

- 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. -

- -

Programming with Herbie

- -

- 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.) -

- -

Finding the problematic expression

- -

- 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.

- -

Converting problematic code to Herbie input

- -

- 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: - -

- Restricting the input range to xim >= 0. -
- - This asks Herbie to consider only non-negative - values of xim when improving the accuracy of this - expression.

- -

Herbie's results

- -

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.

- -

Using Herbie's alternatives

- -

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.

- -

Next steps

- -

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 @@ - - - - - Using Herbie from the Command Line - - - - - -
-

Shell and Batch Mode

- - -
- -

Herbie can be used from the command-line or - from the browser. This page covers - using Herbie from the command line.

- -

The Herbie shell

- -

- 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.

- -

Batch processing FPCores

- -

- 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 @@ - - - - - Using Herbie from the Browser - - - - - -
-

The Browser UI

- - -
- -

- 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

- -

- 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.
- -
- A screenshot of the Herbie web shell main page. -
- -

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. -

- - -

Batch report generation

- -

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