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:
{
- 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.
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.
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].
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.
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.
- 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.
-
- 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
-
-
- (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:
-
- 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.
-
- 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.