mirror of
https://github.com/Smaug123/agdaproofs
synced 2025-10-09 05:48:41 +00:00
Travis fix (#77)
This commit is contained in:
@@ -11,4 +11,8 @@ git:
|
||||
|
||||
script:
|
||||
- export BRANCH=$(if [ "$TRAVIS_PULL_REQUEST" == "false" ]; then echo $TRAVIS_BRANCH; else echo $TRAVIS_PULL_REQUEST_BRANCH; fi)
|
||||
- docker run smaug451/agda:basic /bin/sh -c "cd ~/; git clone https://github.com/Smaug123/agdaproofs.git; cd agdaproofs; git fetch; git checkout $BRANCH; agda Everything/Safe.agda && agda Everything/WithK.agda; find . -type f -name '*.agda' | sort > /tmp/agdas.txt; find . -type f -name '*.agdai' | sort | rev | cut -c 2- | rev > /tmp/compiled.txt; diff /tmp/agdas.txt /tmp/compiled.txt | grep '<' || true"
|
||||
- docker run -i --detach --name agda smaug451/agda:basic
|
||||
- docker exec agda bash -c "cd ~/; git clone https://github.com/Smaug123/agdaproofs.git; cd agdaproofs; git fetch; git checkout $BRANCH"
|
||||
- docker exec agda bash -c "cd ~/agdaproofs; agda Everything/Safe.agda && agda Everything/WithK.agda"
|
||||
- docker exec agda bash -c "cd ~/agdaproofs; find . -type f -name '*.agda' | sort > /tmp/agdas.txt; find . -type f -name '*.agdai' | sort | rev | cut -c 2- | rev > /tmp/compiled.txt; diff /tmp/agdas.txt /tmp/compiled.txt | grep '<' || true"
|
||||
- docker stop agda
|
||||
|
Reference in New Issue
Block a user