mirror of
https://github.com/ProvableHQ/leo.git
synced 2024-12-23 10:12:21 +03:00
tgc parsing for testnet3
This commit is contained in:
parent
3c00cf5b5f
commit
2d365c49b5
67
.github/workflows/acl2.yml
vendored
67
.github/workflows/acl2.yml
vendored
@ -21,7 +21,18 @@ jobs:
|
|||||||
|
|
||||||
- name: Generate asts
|
- name: Generate asts
|
||||||
run: |
|
run: |
|
||||||
cargo -q run -p leo-test-framework --bin tgc
|
# This currently has to be on testnet3 to work:
|
||||||
|
cd compiler/parser
|
||||||
|
cargo -q install --path . --example parser
|
||||||
|
# To ensure full file tests,
|
||||||
|
# just do compiler tests and remove expectation: Fail tests
|
||||||
|
cd ../../tests/compiler
|
||||||
|
find . -type f -exec grep -q 'expectation *: *Fail' {} \; -delete
|
||||||
|
find . -name '*.leo' -execdir parser {} \; > /dev/null
|
||||||
|
# Show how many there are:
|
||||||
|
echo "Counts (.leo / .json):"
|
||||||
|
find . -name '*.leo' -print | wc -l
|
||||||
|
find . -name '*.json' -print | wc -l
|
||||||
|
|
||||||
# Pull the latest release from the leo-acl2-bin repo, and put it into the
|
# 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.
|
# repo/acl2 directory. After it's done, unpack the tgz file locally.
|
||||||
@ -29,7 +40,7 @@ jobs:
|
|||||||
run: |
|
run: |
|
||||||
mkdir acl2 && cd acl2;
|
mkdir acl2 && cd acl2;
|
||||||
wget $( curl -s https://api.github.com/repos/AleoHQ/leo-acl2-bin/releases/latest \
|
wget $( curl -s https://api.github.com/repos/AleoHQ/leo-acl2-bin/releases/latest \
|
||||||
| jq -r '.assets[0].browser_download_url' )
|
| jq -r '.assets[].browser_download_url|scan("^.*leo-acl2--v.*\\.tgz$")' )
|
||||||
|
|
||||||
echo "Unpacking $(ls):"
|
echo "Unpacking $(ls):"
|
||||||
tar -xvzf $(ls)
|
tar -xvzf $(ls)
|
||||||
@ -37,28 +48,31 @@ jobs:
|
|||||||
# Run theorem generation and checking using the prepared ASTs and the pulled and unzipped leo-acl2 tarball.
|
# Run theorem generation and checking using the prepared ASTs and the pulled and unzipped leo-acl2 tarball.
|
||||||
- name: Run tgc over ASTs
|
- name: Run tgc over ASTs
|
||||||
run: |
|
run: |
|
||||||
canonicalization_errors=();
|
parsing_errors=();
|
||||||
type_inference_errors=();
|
num_cases=0;
|
||||||
num_dirs=0;
|
# Note that PWD gets reset at the beginning of each the step
|
||||||
for dir in `ls tmp/tgc`;
|
# to /home/runner/work/leo/leo
|
||||||
|
acl2dir="${PWD}"/acl2
|
||||||
|
cd tests/compiler;
|
||||||
|
for tc in `find ${PWD} -name '*.leo' -print`;
|
||||||
do
|
do
|
||||||
cd tmp/tgc/$dir; # enter the directory
|
cd "${tc%/*}"; # enter the directory
|
||||||
num_dirs=$((num_dirs + 1));
|
leofile="${tc##*/}";
|
||||||
./../../../acl2/tgc canonicalization initial_ast.json canonicalization_ast.json canonicalization-theorem.lisp > canonicalization_result.out || canonicalization_errors+=("$dir");
|
jsonfile="${leofile%.leo}.json";
|
||||||
./../../../acl2/tgc type-inference canonicalization_ast.json type_inferenced_ast.json type-inference-theorem.lisp > type_inference_result.out || type_inference_errors+=("$dir");
|
num_cases=$((num_cases + 1));
|
||||||
cd ../../..
|
"$acl2dir"/tgc parsing "$leofile" "$jsonfile" parsing-theorem.lisp > parsing_result.out || parsing_errors+=("$tc");
|
||||||
done;
|
done;
|
||||||
|
|
||||||
echo "----------------"
|
echo "----------------"
|
||||||
echo "Ran tgc in ${num_dirs} directories."
|
echo "Ran tgc on ${num_cases} programs."
|
||||||
echo "----------------"
|
echo "----------------"
|
||||||
if [ ${#canonicalization_errors[@]} -eq 0 ]; then
|
if [ ${#parsing_errors[@]} -eq 0 ]; then
|
||||||
echo "Canonicalization - Success!"
|
echo "Parsing - Total Success!"
|
||||||
else
|
else
|
||||||
echo "Canonicalization Failures (total: ${#canonicalization_errors[@]}):"
|
echo "Parsing Failures (total: ${#parsing_errors[@]}):"
|
||||||
for dir in ${canonicalization_errors[@]};
|
for tc in ${parsing_errors[@]};
|
||||||
do
|
do
|
||||||
echo $dir
|
echo $tc
|
||||||
done;
|
done;
|
||||||
|
|
||||||
#echo "Attaching logs:"
|
#echo "Attaching logs:"
|
||||||
@ -69,24 +83,7 @@ jobs:
|
|||||||
#done;
|
#done;
|
||||||
fi
|
fi
|
||||||
|
|
||||||
echo "----------------"
|
if [[ ${#parsing_errors[@]} -ne 0 ]]; then
|
||||||
if [ ${#type_inference_errors[@]} -eq 0 ]; then
|
|
||||||
echo "Type Inference - Success!"
|
|
||||||
else
|
|
||||||
echo "Type Inference Failures (total: ${#type_inference_errors[@]}):"
|
|
||||||
for dir in ${type_inference_errors[@]};
|
|
||||||
do
|
|
||||||
echo $dir
|
|
||||||
done;
|
|
||||||
|
|
||||||
#echo "Attaching logs:"
|
|
||||||
#for dir in ${type_inference_errors[@]};
|
|
||||||
#do
|
|
||||||
# cat tmp/tgc/$dir/type_inference_result.out
|
|
||||||
#done;
|
|
||||||
fi
|
|
||||||
|
|
||||||
if [[ ${#canonicalization_errors[@]} -ne 0 || ${#type_inference_errors[@]} -ne 0 ]]; then
|
|
||||||
echo "----------------"
|
echo "----------------"
|
||||||
echo "Exiting with status 1 due to at least one tgc error."
|
echo "Exiting with status 1 due to at least one tgc error."
|
||||||
exit 1
|
exit 1
|
||||||
|
Loading…
Reference in New Issue
Block a user