forked from UCSD-PL/proverbot9001
-
Notifications
You must be signed in to change notification settings - Fork 0
/
.test.sh
44 lines (25 loc) · 1018 Bytes
/
.test.sh
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
#!/bin/bash
date
git rev-parse HEAD
echo Hello from lambda.
# install rust
curl https://static.rust-lang.org/rustup/dist/x86_64-unknown-linux-gnu/rustup-init > /tmp/rustup-init
chmod +x /tmp/rustup-init
/tmp/rustup-init -y
export PATH=$PATH:~/.cargo/bin:~/.local/bin
# need a virtualenv or else maturin won't run
# use site packages so we don't have to reinstall
# pytorch & friends
python3 -m venv --system-site-packages .
source bin/activate
# run setup
make setup
# okay, we've got an install.
make data/compcert-scrape.txt -j `nproc`
python3 ./src/proverbot9001.py tokens data/compcert-scrape.txt tokens.txt &
python3 ./src/proverbot9001.py tactics data/compcert-scrape.txt tactics.txt &
wait # generate tokens and tactics concurrently before proceeding to training
make compcert-train
python src/search_file.py -j 1 --prelude ./CompCert/ lib/Parmov.v --weightsfile=data/polyarg-weights.dat --no-generate-report
echo proofs succeeded:
cat search-report/Parmov-proofs.txt | grep SUCCESS | wc -l