leo/.github/workflows/acl2.yml

84 lines
2.5 KiB
YAML
Raw Normal View History

2021-07-30 15:36:43 +03:00
name: Leo-ACL2
on:
2021-08-18 17:51:50 +03:00
pull_request:
push:
branches:
- master
- staging
- trying
paths-ignore:
- 'docs/**'
- 'documentation/**'
2021-07-30 15:36:43 +03:00
env:
RUST_BACKTRACE: 1
2021-08-18 17:51:50 +03:00
# This job can only be run on linux (Ubuntu)
2021-07-30 15:36:43 +03:00
jobs:
acl2:
name: leo-acl2
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v2
2021-08-17 13:27:23 +03:00
- name: Install Rust
uses: actions-rs/toolchain@v1
with:
profile: minimal
toolchain: stable
override: true
2021-07-30 15:36:43 +03:00
2021-08-17 13:27:23 +03:00
- name: Generate asts
run: |
cargo run -p leo-test-framework --bin tgc
2021-07-30 15:36:43 +03:00
2021-08-17 13:27:23 +03:00
# Pull the latest release from the leo-acl2-bin repo, and put it into the
# repo/acl2 directory. After it's done, unpack the tgz file locally.
2021-08-18 17:51:50 +03:00
- name: Pull tgc executable
2021-07-30 15:36:43 +03:00
run: |
2021-08-17 13:27:23 +03:00
mkdir acl2 && cd acl2;
wget $(curl -s https://api.github.com/repos/AleoHQ/leo-acl2-bin/releases/latest \
| grep "browser_download_url.*.tgz" \
| cut -d : -f 2,3 \
| tr -d \" \
| xargs)
2021-08-17 10:44:44 +03:00
2021-08-17 13:27:23 +03:00
tar -xvzf $(ls)
# Using the prepared ASTs and the pulled and unzipped tgc run theorem generation.
2021-08-18 17:51:50 +03:00
- name: Run tgc over ASTs
2021-08-17 13:27:23 +03:00
run: |
canonicalization_errors=();
type_inference_errors=();
2021-08-17 13:27:23 +03:00
for dir in `ls tmp/tgc`;
do
cd tmp/tgc/$dir; # enter the directory
./../../../acl2/tgc canonicalization initial_ast.json canonicalization_ast.json canonicalization-theorem.lisp > canonicalization_result.out || canonicalization_errors+=("$dir");
./../../../acl2/tgc type-inference canonicalization_ast.json type_inferenced_ast.json type-inference-theorem.lisp > type_inference_result.out || type_inference_errors+=("$dir");
2021-08-17 13:27:23 +03:00
cd ../../..
done;
2021-08-18 14:53:18 +03:00
if [ ${#canonicalization_errors[@]} -eq 0 ]; then
echo "Canonicalization - Success!"
2021-08-18 14:53:18 +03:00
else
echo "Canonicalization Failures:";
for i in ${canonicalization_errors[@]};
2021-08-18 14:53:18 +03:00
do
echo $i;
cat tmp/tgc/$dir/canonicalization_result.out
done;
exit 1
fi
if [ ${#type_inference_errors[@]} -eq 0 ]; then
echo "Type Inference - Success!"
else
echo "Type Inference Failures:";
for i in ${type_inference_errors[@]};
do
echo $i;
cat tmp/tgc/$dir/type_inference_result.out
2021-08-18 14:53:18 +03:00
done;
exit 1
fi