-
Notifications
You must be signed in to change notification settings - Fork 0
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 #47 from herbie-fp/fptaylor-oneclick
Add server deploy scripts and instructions for FPTaylor + FPBench
- Loading branch information
Showing
15 changed files
with
1,499 additions
and
26 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 |
---|---|---|
|
@@ -3,3 +3,5 @@ dist | |
node_modules | ||
.vscode-test/ | ||
*.vsix | ||
.vscode/ | ||
.vscode/settings.json |
This file was deleted.
Oops, something went wrong.
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,2 @@ | ||
fpbench/ | ||
fptaylor/ |
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,30 @@ | ||
## Release checklist for maintainers (server deployment) | ||
* [ ] Update the Herbie server to the most recent stable commit on `main` | ||
* [ ] Clone the Odyssey repo to the server and make sure `node` and `npm` are installed | ||
* [ ] `cd server` to this directory, then run `npm install` to install dependencies. | ||
* [ ] Run `./install.sh` to install FPTaylor and FPBench binaries in the current directory. | ||
* [ ] Run `./fptaylor-server.sh` to run the FPTaylor server on port 8001. See the script to configure the port. See below for CURL requests to test the server. This could be configured to run as a service with systemd. | ||
* [ ] Run `./fpbench-server.sh` to run the FPBench server on port 8002. See the script to configure the port. See below for CURL requests to test the server. This could be configured to run as a service with systemd. | ||
* [ ] On your server, ensure `https://herbie.uwplse.org/fptaylor` points to port 8001 and `https://herbie.uwplse.org/fpbench` points to port 8002 | ||
* [ ] You can confirm the servers are operating correctly by running CURL requests like the following: | ||
``` | ||
curl -X POST http://localhost:8001/exec \ | ||
-H "Content-Type: application/json" \ | ||
-d '{ | ||
"fptaylorInput": "{\nVariables\n\tfloat64 x in [0, 10];\n\nExpressions\n\tex0 = rnd64(rnd64(1) / rnd64(rnd64(sqrt(rnd64(rnd64(1) + x))) + rnd64(sqrt(x))));\n}\n" | ||
}' | ||
curl -X POST http://localhost:8002/exec \ | ||
-H "Content-Type: application/json" \ | ||
-d '{"formulas":["(FPCore (x) :pre (<= 0 x 10) (/ 1 (+ (sqrt (+ 1 x)) (sqrt x))))"]}' | ||
``` | ||
## Setting up Odyssey on the FPBench server | ||
* The Odyssey client can be configured to use different servers for any of its tools. | ||
|
||
* At the time of writing, the Odyssey demo running on "https://herbie-fp.github.io/odyssey/" points to the Herbie server at | ||
"https://herbie.uwplse.org/demo" and also now expects an FPTaylor server (which we provide and describe setup for below) | ||
to be running at "https://herbie.uwplse.org/fptaylor", and an FPBench server (also provided) to be running at "https://herbie.uwplse.org/fpbench". | ||
|
||
* Before each release, the Herbie demo server should be updated to match the version Odyssey was developed against (usually just main). | ||
|
||
* The other tool servers are simple Node servers that use Express to handle requests and execute command line tools in a shell. Care was taken to prevent command injection. |
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,87 @@ | ||
const fs = require('fs'); | ||
const path = require('path'); | ||
const https = require('https'); | ||
const http = require('http'); | ||
const AdmZip = require('adm-zip'); | ||
|
||
const downloadFile = async (uri, dest, maxRedirects = 10) => { | ||
const parsedUrl = new URL(uri); | ||
const protocol = parsedUrl.protocol === 'https:' ? https : http; | ||
|
||
const handleRedirects = async (res, redirectsLeft) => { | ||
if (res.statusCode >= 300 && res.statusCode < 400 && res.headers.location) { | ||
if (redirectsLeft > 0) { | ||
const newUrl = new URL(res.headers.location, uri).href; | ||
console.log(`Redirecting to ${newUrl}`); | ||
return await downloadFile(newUrl, dest, redirectsLeft - 1); | ||
} else { | ||
throw new Error('Too many redirects'); | ||
} | ||
} else if (res.statusCode === 200) { | ||
const file = fs.createWriteStream(dest); | ||
return new Promise((resolve, reject) => { | ||
res.pipe(file); | ||
file.on('finish', () => { | ||
file.close((err) => { | ||
if (err) { | ||
reject(err); | ||
} else { | ||
resolve(); | ||
} | ||
}); | ||
}); | ||
}); | ||
} else { | ||
throw new Error(`Failed to get '${uri}' (${res.statusCode})`); | ||
} | ||
}; | ||
|
||
return await (new Promise((resolve, reject) => { | ||
const request = protocol.get(uri, async (response) => { | ||
try { | ||
await handleRedirects(response, maxRedirects); | ||
resolve(); | ||
} catch (err) { | ||
reject(err); | ||
} | ||
}).on('error', (err) => { | ||
fs.unlink(dest, () => reject(err)); | ||
}); | ||
})); | ||
}; | ||
|
||
const unzipFile = (zipPath, outPath) => { | ||
try { | ||
const zip = new AdmZip(zipPath); | ||
zip.extractAllTo(outPath, true); | ||
fs.unlinkSync(zipPath); | ||
} catch (err) { | ||
throw new Error(`Failed to unzip file: ${err.message}`); | ||
} | ||
}; | ||
|
||
const main = async () => { | ||
const uri = process.argv[2]; | ||
const outPath = process.argv[3]; | ||
|
||
if (!uri || !outPath) { | ||
console.error('Usage: node script.js <URI> <OUT_PATH>'); | ||
process.exit(1); | ||
} | ||
|
||
const zipPath = path.join(outPath, 'downloaded.zip'); | ||
|
||
try { | ||
fs.mkdirSync(outPath, { recursive: true }); | ||
await downloadFile(uri, zipPath); | ||
console.log('Downloaded file'); | ||
unzipFile(zipPath, outPath); | ||
console.log('Unzipped file'); | ||
process.exit(0); | ||
} catch (err) { | ||
console.error(`Error: ${err.message}`); | ||
process.exit(1); | ||
} | ||
}; | ||
|
||
main(); |
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 @@ | ||
node tool-server.js --port 8002 --tool fpbench --path fpbench/linux/fpbench-compiled/bin/fpbench |
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 @@ | ||
node tool-server.js --port 8001 --tool fptaylor --path fptaylor/linux/fptaylor-compiled/fptaylor |
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,4 @@ | ||
node download-and-unzip.js https://github.com/herbie-fp/odyssey/releases/download/fptaylor-component/fptaylor-dist.zip fptaylor | ||
chmod +x fptaylor/linux/fptaylor-compiled/fptaylor | ||
node download-and-unzip.js https://github.com/herbie-fp/odyssey/releases/download/fptaylor-component/fpbench-dist.zip fpbench | ||
chmod +x fpbench/linux/fpbench-compiled/bin/fpbench |
Oops, something went wrong.