-
Notifications
You must be signed in to change notification settings - Fork 33
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #198 from uwplse/develop
Release Herbie 1.2
- Loading branch information
Showing
165 changed files
with
6,908 additions
and
3,753 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -16,3 +16,4 @@ www/demo | |
demo.log | ||
*.class | ||
cost | ||
previous |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,43 +1,42 @@ | ||
language: c | ||
sudo: required | ||
services: | ||
- docker | ||
cache: | ||
directories: | ||
- docker-images | ||
env: | ||
global: | ||
- RACKET_DIR=~/racket | ||
matrix: | ||
- RACKET_VERSION="6.3" | ||
HERBIE_SEED="#(2749829514 1059579101 312104142 915324965 966790849 1349306526)" | ||
- RACKET_VERSION="6.4" | ||
HERBIE_SEED="#(2749829514 1059579101 312104142 915324965 966790849 1349306526)" | ||
- RACKET_VERSION="6.5" | ||
HERBIE_SEED="#(2749829514 1059579101 312104142 915324965 966790849 1349306526)" | ||
- RACKET_VERSION="6.6" | ||
TBENCHES="bench/tutorial.fpcore bench/hamming/" | ||
HERBIE_SEED="#(2749829514 1059579101 312104142 915324965 966790849 1349306526)" | ||
TSEED="racket $TRAVIS_BUILD_DIR/infra/travis.rkt --seed '${HERBIE_SEED}' $TBENCHES" | ||
TRAND="racket $TRAVIS_BUILD_DIR/infra/travis.rkt $TBENCHES" | ||
UTEST="raco test src" | ||
matrix: | ||
# separate builds for travis benches and unit tests | ||
- RACKET_VERSION="6.7" | ||
HERBIE_SEED="#(2749829514 1059579101 312104142 915324965 966790849 1349306526)" | ||
JOB="${TSEED}" | ||
- RACKET_VERSION="6.9" | ||
JOB="${TSEED}" | ||
- RACKET_VERSION="6.11" | ||
JOB="${TSEED}" | ||
- RACKET_VERSION="6.7" | ||
HERBIE_SEED="#f" | ||
JOB="${UTEST}" | ||
- RACKET_VERSION="6.9" | ||
JOB="${UTEST}" | ||
- RACKET_VERSION="6.11" | ||
JOB="${UTEST}" | ||
# remember to change the `allow_failures` key below! | ||
- RACKET_VERSION="6.11" | ||
JOB="${TRAND}" | ||
matrix: | ||
allow_failures: | ||
- env: RACKET_VERSION="6.7" | ||
HERBIE_SEED="#f" | ||
- env: RACKET_VERSION="6.11" | ||
JOB="${TRAND}" | ||
before_install: | ||
- git clone https://github.com/greghendershott/travis-racket.git ../travis-racket | ||
- cat ../travis-racket/install-racket.sh | bash | ||
- export PATH="${RACKET_DIR}/bin:${PATH}" | ||
# - docker load -i docker-images/herbie.image || true | ||
install: | ||
- raco pkg install --auto $TRAVIS_BUILD_DIR/src | ||
# - docker build -t herbie . | ||
script: | ||
- raco test src | ||
- racket $TRAVIS_BUILD_DIR/infra/travis.rkt --seed "${HERBIE_SEED}" bench/tutorial.fpcore bench/hamming/ | ||
#before_cache: | ||
# - docker save -o docker-images/herbie.image herbie | ||
- echo ${JOB} && eval ${JOB} | ||
notifications: | ||
slack: | ||
secure: QB8ib/gxZWZ8rY9H54BktIgx8LfjdqabSAkmWip0VHlUhrh2ULG566XgmB5h75eNzCil2cw76ma5wfSC0MNIQ1iDHKCxAgTE0+gcPcZAYGfucQ28sKGBG2wcuJfvBLG6lVDxj+luGUh3XohouTLYI9cg509JBgTgpcrXVexYAaE= |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
FROM jackfirth/racket:6.8 | ||
FROM jackfirth/racket:6.12 | ||
MAINTAINER Pavel Panchekha <[email protected]> | ||
RUN apt-get update \ | ||
&& apt-get install -y libcairo2-dev libjpeg62 libpango1.0-dev \ | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,46 +1,22 @@ | ||
![Herbie](logo.png) | ||
|
||
Herbie synthesizes floating-point programs from real-number programs, | ||
automatically handling simple numerical instabilities. | ||
Visit [our website](https://herbie.uwplse.org) for tutorials, | ||
documentation, and an online demo. | ||
|
||
Current Status | ||
-------------- | ||
|
||
[![Build Status](https://travis-ci.org/uwplse/herbie.svg?branch=master)](https://travis-ci.org/uwplse/herbie) | ||
|
||
Herbie can improve the accuracy of many real-world programs, and is | ||
used by scientists in many disciplines. It has lead to two patches | ||
(for | ||
complex [square roots](https://github.com/josdejong/mathjs/pull/208) | ||
and | ||
[trigonometric functions](https://github.com/josdejong/mathjs/pull/247)), | ||
in [math.js](http://mathjs.org/) an open-source mathematics library. | ||
Herbie has semi-regular releases twice a year, maintains backwards | ||
compatibility, and uses standardized formats. | ||
|
||
Helping Out | ||
----------- | ||
|
||
Herbie development is organized on our | ||
[mailing list](https://mailman.cs.washington.edu/mailman/listinfo/herbie) | ||
where we discuss work in progress and announce major improvements. | ||
[Email us](mailto:[email protected]) to get involved! | ||
|
||
We use [Github](https://github.com/uwplse/herbie) | ||
and [Trello](https://trello.com/b/lh7b33Dr/herbie) to organize some | ||
development goals Our test results | ||
are [archived](http://herbie.uwplse.org/reports/). | ||
Herbie synthesizes floating-point programs from real-number programs, | ||
automatically handling simple numerical instabilities. Visit [our | ||
website](https://herbie.uwplse.org) for tutorials, documentation, and | ||
an online demo. Herbie has semi-regular releases twice a year, | ||
maintains backwards compatibility, and uses standardized formats. | ||
|
||
Installing | ||
---------- | ||
|
||
For full details on installing Herbie, please see the | ||
[tutorial](http://herbie.uwplse.org/doc/latest/installing-herbie.html). | ||
[tutorial](http://herbie.uwplse.org/doc/latest/installing.html). | ||
|
||
Herbie requires Racket 6.3 or later, and supports Linux and OS X. | ||
Install it with: | ||
Herbie requires Racket 6.7 or later, and supports Windows, OS X, and | ||
Linux. Install it with: | ||
|
||
raco pkg install herbie | ||
|
||
|
@@ -66,9 +42,10 @@ Run Herbie from the top-level directory of the repo, and enter the | |
cancellation test: | ||
|
||
$ herbie shell | ||
Seed: #(1046809171 2544984934 1871826185 4237421819 4093186437 162666889) | ||
Herbie 1.2 with seed #(349461420 3681359142 2680361770 2900531005 1939065059 1779362427) | ||
Find help on <https://herbie.uwplse.org/>, exit with Ctrl-D | ||
herbie> (FPCore (x) (- (+ 1 x) x)) | ||
(FPCore (x) 1) | ||
(FPCore (x) ... 1) | ||
|
||
The output is Herbie's improved, more-accurate expression, in this case | ||
the constant `1`. | ||
|
@@ -79,6 +56,18 @@ Consult the | |
[documentation](http://herbie.uwplse.org/doc/latest/options.html). | ||
for more. | ||
|
||
Helping Out | ||
----------- | ||
|
||
Herbie development is organized on our | ||
[mailing list](https://mailman.cs.washington.edu/mailman/listinfo/herbie) | ||
where we discuss work in progress and announce major improvements. | ||
[Email us](mailto:[email protected]) to get involved! | ||
|
||
We use [Github](https://github.com/uwplse/herbie) | ||
and [Trello](https://trello.com/b/lh7b33Dr/herbie) to organize some | ||
development goals. | ||
|
||
Running Tests | ||
------------- | ||
|
||
|
@@ -92,17 +81,15 @@ projects, examples emailed to the developers, and from numerical | |
analysis textbooks. This suite is found in `bench/`. The full test can | ||
be run with | ||
|
||
herbie report bench/ | ||
herbie report bench/ graphs/ | ||
|
||
This full test can take several hours to run. We often test Herbie on | ||
basic but representative examples with: | ||
The output is an HTML report in `graphs/`. This full test can take | ||
several hours to run. We often test Herbie on basic but representative | ||
examples with: | ||
|
||
herbie report bench/hamming/ | ||
herbie report bench/hamming/ graphs/ | ||
|
||
This takes approximately 15 minutes. | ||
|
||
Test results are collected on | ||
[uwplse.org](http://herbie.uwplse.org/reports/). If you have an | ||
account on this server, you can publish your test results with | ||
|
||
make publish | ||
Historic and nightly test results are collected on | ||
[uwplse.org](http://herbie.uwplse.org/reports/). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,24 @@ | ||
; -*- mode: scheme -*- | ||
|
||
; Herbie cannot sample enough input points for these tests. | ||
|
||
(FPCore (x) | ||
:name "Random Jason Timeout Test 001" | ||
(+ x (asin (cosh x)))) | ||
|
||
(FPCore (x y) | ||
:name "Random Jason Timeout Test 009" | ||
(fabs (fmod y (asin (- 2.821952756469356e+184 x))))) | ||
|
||
(FPCore (a b c) | ||
:pre (and (< 0 a) (< 0 b) (< 0 c)) | ||
:name "Area of a triangle" | ||
(sqrt (* (* (* (/ (+ (+ a b) c) 2) (- (/ (+ (+ a b) c) 2) a)) | ||
(- (/ (+ (+ a b) c) 2) b)) | ||
(- (/ (+ (+ a b) c) 2) c)))) | ||
|
||
(FPCore (n U t l Om U*) | ||
:name "Toniolo and Linder, Equation (13)" | ||
(sqrt (* (* (* 2 n) U) | ||
(- (- t (* 2 (/ (* l l) Om))) | ||
(* (* n (pow (/ l Om) 2)) (- U U*)))))) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
; -*- mode: scheme -*- | ||
|
||
; Herbie cannot evaluate these tests fast enough with MPFR. | ||
; In contrast to challenge/timeout.fpcore, these tests do | ||
; not finish sampling input points (sometimes varying with seed). | ||
|
||
(FPCore (a b) | ||
:name "Random Jason Timeout Test 003" | ||
(sin (pow (sqrt (atan2 b b)) (- b a)))) | ||
|
||
(FPCore (a b) | ||
:name "Random Jason Timeout Test 015" | ||
(sin (pow (sqrt (atan2 b b)) (- b a)))) | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
(FPCore (lo hi x) | ||
:pre (and (< lo -1e308) (> hi 1e308)) | ||
(/ (- x lo) (- hi lo))) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,20 @@ | ||
; -*- mode: scheme -*- | ||
|
||
; Herbie requires too much MPFR precision for these tests. | ||
|
||
(FPCore (c) | ||
:name "Random Jason Timeout Test 002" | ||
(fmod (sinh c) (- c (pow -2.9807307601812193e+165 2)))) | ||
|
||
(FPCore (a c) | ||
:name "Random Jason Timeout Test 004" | ||
(fmod (cosh c) (log1p a))) | ||
|
||
(FPCore (a) | ||
:name "Random Jason Timeout Test 012" | ||
(acos (pow (fmod (cosh a) (* a a)) (log1p a)))) | ||
|
||
(FPCore (c) | ||
:name "Random Jason Timeout Test 014" | ||
(fmod (sinh c) (- c (pow -2.9807307601812193e+165 2)))) | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
; -*- mode: scheme -*- | ||
|
||
; Herbie times out on these tests, but gets past sampling. | ||
|
||
(FPCore (a) | ||
:name "Random Jason Timeout Test 006" | ||
(fabs (fmod (atan2 (expm1 (sin (expm1 a))) (atan a)) a))) | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,44 @@ | ||
; -*- mode: scheme -*- | ||
|
||
; TODO: exp function unimplemented. | ||
#;(FPCore (xre xim) | ||
:name "exp with complex power real part (p55)" | ||
(let ([x (complex xre xim)]) | ||
(re (/ (+ (exp x) (exp (- x))) (complex 2 0))))) | ||
|
||
#;(FPCore (xre xim) | ||
:name "exp with complex power imaginary part (p55)" | ||
(let ([x (complex xre xim)]) | ||
(im (/ (+ (exp x) (exp (- x))) (complex 2 0))))) | ||
|
||
#;(FPCore (x y) | ||
:name "Euler formula real part (p55)" | ||
(let ([a (/ (+ (exp x) (exp (- x))) 2)] | ||
[b (/ (- (exp x) (exp (- x))) 2)]) | ||
(re (complex (* a (cos y)) (* b (sin y)))))) | ||
|
||
#;(FPCore (x y) | ||
:name "Euler formula imaginary part (p55)" | ||
(let ([a (/ (+ (exp x) (exp (- x))) 2)] | ||
[b (/ (- (exp x) (exp (- x))) 2)]) | ||
(im (complex (* a (cos y)) (* b (sin y)))))) | ||
|
||
(FPCore () | ||
:name "3.9.1 real part (p56)" | ||
(let ([x (complex -1 1)]) | ||
(re (+ (* x x x x x x) (* (complex 6 0) x x x x x) (* (complex 15 0) x x x x) (* (complex 20 0) x x x) (* (complex 15 0) x x) (* (complex 6 0) x) (complex 1 0))))) | ||
|
||
(FPCore () | ||
:name "3.9.1 imaginary part (p56)" | ||
(let ([x (complex -1 1)]) | ||
(im (+ (* x x x x x x) (* (complex 6 0) x x x x x) (* (complex 15 0) x x x x) (* (complex 20 0) x x x) (* (complex 15 0) x x) (* (complex 6 0) x) (complex 1 0))))) | ||
|
||
(FPCore () | ||
:name "3.9.2 real part (p56)" | ||
(let ([x (complex (/ (- 1) 2) (/ (sqrt 3) 2))]) | ||
(re (+ (* x x x x) (* (complex (- 2) 0) x x x) (* (complex 5 0) x x) (* (complex 4 0) x) (complex 7 0))))) | ||
|
||
(FPCore () | ||
:name "3.9.2 imaginary part (p56)" | ||
(let ([x (complex (/ (- 1) 2) (/ (sqrt 3) 2))]) | ||
(im (+ (* x x x x) (* (complex (- 2) 0) x x x) (* (complex 5 0) x x) (* (complex 4 0) x) (complex 7 0))))) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.