Skip to content

Commit

Permalink
chore(script/test_registry): Replace with leanpkg. Execute in every a…
Browse files Browse the repository at this point in the history
…rtifact-producing build configuration.
  • Loading branch information
Kha authored and leodemoura committed Dec 20, 2017
1 parent ddf014c commit 7e4f348
Show file tree
Hide file tree
Showing 6 changed files with 24 additions and 71 deletions.
3 changes: 3 additions & 0 deletions .appveyor.yml
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,9 @@ build_script:

test_script:
- C:\msys64\usr\bin\bash -lc "exec 0</dev/null && cd $APPVEYOR_BUILD_FOLDER/build && ctest -j4 --output-on-failure"
- C:\msys64\usr\bin\bash -lc "exec 0</dev/null && cd $APPVEYOR_BUILD_FOLDER/packages &&
../bin/leanpkg configure &&
for d in _target/deps/*; do (cd $d; ../../../../bin/leanpkg test || exit 1); done"

artifacts:
- path: build\lean-*-windows.zip
Expand Down
13 changes: 10 additions & 3 deletions .travis.yml
Original file line number Diff line number Diff line change
Expand Up @@ -92,6 +92,7 @@ matrix:
CMAKE_CXX_COMPILER=clang++
CMAKE_BUILD_TYPE=Release
UPLOAD=ON
TEST_LEANPKG_REGISTRY=ON

- os: osx
env:
Expand All @@ -106,6 +107,7 @@ before_install:
fi

script:
- set -e
- mkdir -p build
- cd build
- if [[ $TESTCOV != ON ]]; then TESTCOV=OFF; fi
Expand All @@ -122,12 +124,17 @@ script:
-DSTATIC=$STATIC
-DLEAN_EXTRA_MAKE_OPTS=$LEAN_EXTRA_MAKE_OPTS
$OPTIONS
../src || exit
- make -j2 || exit
../src
- make -j2
- if [[ $TEST != OFF ]]; then yes "A" | ctest -j2 --output-on-failure; fi
- if [[ $TEST_LEANPKG_REGISTRY == ON ]]; then
cd ../packages;
if [[ $TRAVIS_OS_NAME == linux ]]; then ../bin/leanpkg add "https://github.com/leanprover/smt2_interface"; fi;
../bin/leanpkg configure;
for d in _target/deps/*; do (cd $d; ../../../../bin/leanpkg test); done;
fi
- if [[ $UPLOAD == ON ]]; then cpack; fi
- if [[ $UPLOAD == ON && $GH_TOKEN && $TRAVIS_PULL_REQUEST == false && $TRAVIS_BRANCH == master ]]; then (cd ..; bash script/deploy_gh_pages.sh); fi
- if [[ $TEST_LEANPKG_REGISTRY == ON ]]; then ../script/test_registry.py; fi
- cd ..

after_script:
Expand Down
3 changes: 3 additions & 0 deletions packages/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
*.olean
/_target
/leanpkg.path
8 changes: 8 additions & 0 deletions packages/leanpkg.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
[package]
name = "test_registry"
version = "0.1"
lean_version = "master"

[dependencies]
super = { git = "https://github.com/leanprover/super", rev = "master" }
mini_crush = { git = "https://github.com/leanprover/mini_crush", rev = "master" }
7 changes: 0 additions & 7 deletions script/package_registry.json

This file was deleted.

61 changes: 0 additions & 61 deletions script/test_registry.py

This file was deleted.

0 comments on commit 7e4f348

Please sign in to comment.