diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml index 4c72ac1..88b6c44 100644 --- a/.github/workflows/lean.yml +++ b/.github/workflows/lean.yml @@ -16,9 +16,5 @@ jobs: check-reservoir-eligibility: false run_executable: steps: - - pwd - - tree - - echo "8875913 1124087 165048 20902 185856 26055 3456 484\n1776924" | .lake/build/bin/formalqkd > output.txt - - if cat output.txt | grep -q 'SKL = 1464719'; then - echo "matched" - fi + - test/run_executable_example.sh + diff --git a/test/run_executable_example.sh b/test/run_executable_example.sh new file mode 100755 index 0000000..711e2f5 --- /dev/null +++ b/test/run_executable_example.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +printf "8875913 1124087 165048 20902 185856 26055 3456 484\n1776924" | .lake/build/bin/formalqkd > output.txt + +if cat output.txt | grep -q 'SKL = 1464719'; then + echo "Expected result." +else + echo "Unexpected result" + exit -1 +fi