max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: switch to Github Actions

Browse source
This commit is contained in:
Sebastian Ullrich 2019-11-19 12:41:24 +01:00 • committed by Leonardo de Moura
parent e426e5dd28
commit 82a0991df6
7 changed files with 96 additions and 332 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

62
.appveyor.yml
View file

@ -1,62 +0,0 @@
image: Visual Studio 2017
environment:
MSYSTEM: MINGW64 # use MSYS2 shell
matrix:
- CFG: MINGW64
UPLOAD: ON
- CFG: MSVC
cache: c:\tools\vcpkg\installed\
install:
# upgrade git for vcpkg: https://github.com/appveyor/ci/issues/2097
- if %CFG% == MSVC (choco upgrade git -y & vcpkg install mpir:x64-windows)
build_script:
- call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Community\VC\Auxiliary\Build\vcvars64.bat"
- cd %APPVEYOR_BUILD_FOLDER% && mkdir build && cd build
# disable slow LTO
- if %CFG% == MSVC (cmake ../src
-DCMAKE_BUILD_TYPE=Release
-DCMAKE_TOOLCHAIN_FILE=c:/tools/vcpkg/scripts/buildsystems/vcpkg.cmake
-DLEAN_EXTRA_CXX_FLAGS=/GL-
-DLEAN_EXTRA_LINKER_FLAGS_MSVC=/LTCG:OFF
-G "NMake Makefiles" &&
cmake --build .)
- if %CFG% == MINGW64 (C:\msys64\usr\bin\bash -lc "exec 0</dev/null && cd $APPVEYOR_BUILD_FOLDER/build &&
OPTIONS='';
if [[ $APPVEYOR_SCHEDULED_BUILD == True ]]; then . ../script/setup_nightly.sh; fi &&
cmake ../src -DINCLUDE_MSYS2_DLLS=ON -DCMAKE_BUILD_TYPE=Release $OPTIONS -G 'Unix Makefiles' &&
cmake --build . &&
cpack")
test_script:
- C:\msys64\usr\bin\bash -lc "exec 0</dev/null && cd $APPVEYOR_BUILD_FOLDER/build && ctest -j4 --output-on-failure"
# # don't test packages when building nightly
# - C:\msys64\usr\bin\bash -lc "exec 0</dev/null && cd $APPVEYOR_BUILD_FOLDER/packages &&
# if [[ ! -f ../build/nightly.sh ]]; then
# ../bin/leanpkg configure &&
# for d in _target/deps/*; do (cd $d; ../../../../bin/leanpkg test || exit 1); done;
# fi"
# - C:\msys64\usr\bin\bash -lc "exec 0</dev/null && cd $APPVEYOR_BUILD_FOLDER &&
# if [[ $UPLOAD == ON && $GH_TOKEN && $APPVEYOR_BRANCH == master ]]; then
# . build/nightly.sh &&
# bash script/deploy_nightly.sh build/lean-*-windows.zip;
# fi"
artifacts:
- path: build\lean-*-windows.zip
name: binary
deploy:
description: 'Lean release'
provider: GitHub
auth_token:
secure: d+yPrDEAbiNrcf3a0PDNYEn/ieOOP6M7cP9zje+QkJEjHFdjBjWMe8b3qrC1hrus
artifact: binary
draft: false
prerelease: false
on:
appveyor_repo_tag: true
UPLOAD: ON

92
.github/workflows/ci.yml vendored Normal file
View file

@ -0,0 +1,92 @@
name: CI
on:
push:
branches:
- master
tags:
- '*'
pull_request:
branches:
- master
jobs:
Build:
runs-on: ${{ matrix.os }}
strategy:
matrix:
# NOTE: must list all targets in `include` here to activate them
name: [Linux, "Linux Debug", "Linux fsanitize", "Linux LLVM=ON", macOS, Windows]
include:
- name: Linux
os: ubuntu-latest
- name: Linux Debug
os: ubuntu-latest
CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Debug
- name: Linux fsanitize
os: ubuntu-latest
CMAKE_OPTIONS: -DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS=-fsanitize=address,undefined
- name: Linux LLVM=ON
os: ubuntu-latest
CMAKE_OPTIONS: -DLLVM=ON
- name: macOS
os: macos-latest
- name: Windows
os: windows-latest
CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Release -G "Unix Makefiles" -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++
# complete all jobs
fail-fast: false
env:
# must be inside workspace
CCACHE_DIR: ${{ github.workspace }}/.ccache
CCACHE_COMPRESS: true
# current cache limit
CCACHE_MAXSIZE: 200M
CMAKE_OPTIONS: ${{ matrix.CMAKE_OPTIONS }}
steps:
- name: Checkout
uses: actions/checkout@v1
- name: Install Nix
uses: cachix/install-nix-action@v5
if: matrix.os != 'windows-latest'
- name: Install MSYS2
uses: numworks/setup-msys2@v1
if: matrix.os == 'windows-latest'
# binaries segfault without this step (?!), must be separate step because it might update the MSYS2 runtime
- name: Update MSYS2
run: msys2do pacman -Syu --noconfirm
if: matrix.os == 'windows-latest'
- name: Cache
uses: actions/cache@v1
with:
path: .ccache
key: ${{ matrix.name }}-build-${{ github.sha }}
# fall back to (latest) previous cache
restore-keys: |
${{ matrix.name }}-build
- name: Setup
run: |
# open shell once for initial setup
nix-shell --run true
if: matrix.os != 'windows-latest'
- name: Setup
run: msys2do pacman --noconfirm -S make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x86_64-ccache git diffutils
if: matrix.os == 'windows-latest'
- name: Build
run: nix-shell --run ./script/ci.sh
if: matrix.os != 'windows-latest'
- name: Build
run: msys2do ./script/ci.sh
if: matrix.os == 'windows-latest'
- name: Test
run: nix-shell --run "cd build; ctest -j --output-on-failure < /dev/null"
if: matrix.os != 'windows-latest'
- name: Test
run: msys2do cd build; ctest -j --output-on-failure ^< /dev/null
shell: cmd
if: matrix.os == 'windows-latest'
- name: CCache stats
run: nix-shell --run "ccache -s"
if: matrix.os != 'windows-latest'
- name: CCache stats
run: msys2do ccache -s
if: matrix.os == 'windows-latest'

174
.travis.yml
View file

@ -1,174 +0,0 @@
language: cpp
sudo: true
cache: apt
dist: trusty
group: deprecated-2017Q3
addons:
apt:
sources: &apt_sources
- ubuntu-toolchain-r-test
- sourceline: 'ppa:kalakris/cmake' # cmake 2.8 for precise
- sourceline: 'ppa:adrozdoff/cmake' # cmake 3 for trusty
- sourceline: 'ppa:h-rayflood/llvm'
- sourceline: ppa:hvr/z3 # z3 for the smt interface package
packages: &default_packages
- cmake
- libgmp-dev
- libgoogle-perftools-dev
- g++-4.9
- clang-3.4
matrix:
include:
- os: linux
dist: precise
env:
CMAKE_CXX_COMPILER=g++-4.9
CMAKE_BUILD_TYPE=Release
UPLOAD=ON
STATIC=ON
FIRST=1
- os: linux
env:
CMAKE_CXX_COMPILER=clang++-3.4
CMAKE_BUILD_TYPE=Release
LEAN_EXTRA_MAKE_OPTS=-t0
TCMALLOC=ON
- os: linux
addons: &gcc6_addons
apt:
sources: *apt_sources
packages:
- *default_packages
- g++-6
- gcc-6
env:
CMAKE_CXX_COMPILER=g++-6
CMAKE_BUILD_TYPE=Release
TCMALLOC=ON
- os: linux
addons: *gcc6_addons
env:
CMAKE_CXX_COMPILER=g++-6
CMAKE_BUILD_TYPE=Release
TESTCOV=ON
- os: linux
addons: *gcc6_addons
env:
CMAKE_CXX_COMPILER=g++-6
CMAKE_BUILD_TYPE=Release
MULTI_THREAD=OFF
- os: linux
addons:
apt:
sources: *apt_sources
packages:
- *default_packages
- z3
env:
CMAKE_CXX_COMPILER=g++-4.9
CMAKE_BUILD_TYPE=Release
TEST=OFF
TEST_LEANPKG_REGISTRY=ON
- os: linux
env:
CMAKE_CXX_COMPILER=clang++-3.4
CMAKE_BUILD_TYPE=Debug
TCMALLOC=ON
- os: linux
dist: precise
env:
CMAKE_CXX_COMPILER=g++-4.9
CMAKE_BUILD_TYPE=Debug
- os: osx
env:
CMAKE_CXX_COMPILER=clang++
CMAKE_BUILD_TYPE=Release
UPLOAD=ON
TEST_LEANPKG_REGISTRY=ON
- os: osx
env:
CMAKE_CXX_COMPILER=g++
CMAKE_BUILD_TYPE=Debug
before_install:
- |
if [[ $TRAVIS_OS_NAME == osx ]]; then
brew update &&
(brew install gcc || brew link --overwrite gcc) &&
brew install gmp &&
# workaround for https://github.com/travis-ci/travis-ci/issues/6307
command curl -sSL https://rvm.io/mpapis.asc | gpg --import -
rvm get head || true
fi
script:
- set -e
- mkdir -p build
- cd build
- if [[ $TESTCOV != ON ]]; then TESTCOV=OFF; fi
- if [[ $TCMALLOC != ON ]]; then TCMALLOC=OFF; fi
- if [[ $STATIC != ON ]]; then STATIC=OFF; fi
- if [[ $MULTI_THREAD != OFF ]]; then MULTI_THREAD=ON; fi
- OPTIONS=""
- |
if [[ $TRAVIS_EVENT_TYPE == cron ]]
then
# trigger AppVeyor build from first Travis job because they can't be bothered to let us set up a cron build
[[ -n $FIRST ]] && curl -H "Authorization: Bearer $APPVEYOR_TOKEN" -H "Content-Type: application/json" https://ci.appveyor.com/api/builds -d '{"accountName": "leodemoura", "projectSlug": "lean", "branch": "master", "environmentVariables": {"APPVEYOR_SCHEDULED_BUILD": "True"}}'
git fetch --unshallow --tags origin
. ../script/setup_nightly.sh
fi
- cmake -DCMAKE_BUILD_TYPE=$CMAKE_BUILD_TYPE
-DCMAKE_CXX_COMPILER=$CMAKE_CXX_COMPILER
-DTESTCOV=$TESTCOV
-DTCMALLOC=$TCMALLOC
-DMULTI_THREAD=$MULTI_THREAD
-DSTATIC=$STATIC
-DLEAN_EXTRA_MAKE_OPTS=$LEAN_EXTRA_MAKE_OPTS
$OPTIONS
../src
- make -j2
- if [[ $TEST != OFF ]]; then yes "A" | travis_wait 60 ctest -j2 --output-on-failure; fi
# - |
# # don't test packages when building nightly
# if [[ $TEST_LEANPKG_REGISTRY == ON && -z $LEAN_VERSION_STRING ]]; 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_nightly.sh build/lean-*); fi
- cd ..
after_script:
- if [[ $TESTCOV == ON ]]; then bash <(curl -s https://codecov.io/bash) -x gcov-6; fi
notifications:
email:
recipients:
- lean-build@googlegroups.com
on_success: change
on_failure: always
deploy:
provider: releases
api_key: $GH_TOKEN
file_glob: true
file: build/lean-*
skip_cleanup: true
overwrite: true
on:
condition: $UPLOAD = ON && $GH_TOKEN
repo: leanprover/lean
tags: true

72
azure-pipelines.yml
View file

@ -1,72 +0,0 @@
trigger:
branches:
include:
- master
tags:
include:
- '*'
jobs:
- job: Nix
strategy:
matrix:
Linux:
imageName: ubuntu-latest
Linux Debug:
imageName: ubuntu-latest
CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Debug
Linux -fsanitize=address,undefined:
imageName: ubuntu-latest
CMAKE_OPTIONS: -DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS=-fsanitize=address,undefined
Linux LLVM=ON:
imageName: ubuntu-latest
CMAKE_OPTIONS: -DLLVM=ON
macOS:
imageName: macos-latest
pool:
vmImage: $(imageName)
steps:
- script: |
# https://github.com/commercialhaskell/stack/commit/b2e2f3d0568e6d73fc0477dee8ca7c04466ec1f6
(for i in {1..5}; do bash <(curl https://nixos.org/nix/install) && exit 0; done; exit 1)
. ~/.nix-profile/etc/profile.d/nix.sh
# open shell once for initial setup
eval nix-shell $NIX_SHELL_OPTIONS --run true
displayName: Setup
- script: |
. ~/.nix-profile/etc/profile.d/nix.sh
export CMAKE_OPTIONS="-DCMAKE_BUILD_TYPE=Release $CMAKE_OPTIONS"
eval nix-shell $NIX_SHELL_OPTIONS --run ./script/ci.sh
displayName: Build
- task: PublishTestResults@2
inputs:
testResultsFormat: cTest
testResultsFiles: build/Testing/*/Test.xml
testRunTitle: $(Agent.JobName)
condition: succeededOrFailed()
displayName: Publish test results
- job: Windows
pool:
vmImage: windows-latest
steps:
- script: |
choco install -y msys2
C:\tools\msys64\usr\bin\bash -lc "pacman --noconfirm -S make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang git diffutils"
displayName: Setup
- script: |
C:\tools\msys64\usr\bin\bash -l ./script/ci.sh
env:
CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Release -G "Unix Makefiles" -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++
# use mingw64 shell
MSYSTEM: MINGW64
# don't let bash reset cwd
CHERE_INVOKING: 1
displayName: Build
- task: PublishTestResults@2
inputs:
testResultsFormat: cTest
testResultsFiles: build/Testing/*/Test.xml
testRunTitle: $(Agent.JobName)
condition: succeededOrFailed()
displayName: Publish test results

19
doc/make/travis.md
View file

@ -1,19 +0,0 @@
Automatic Builds at [Travis](https://travis-ci.org/)
----------------------------------------------------
When a commit is submitted to the the main repository,
a service hook at github will automatically build Lean using
[Travis](https://travis-ci.org/).
There is a way to prevent a push from being built.
Pushes that have either ```[ci skip]``` or ```[skip ci]``` *anywhere* in one of the
commit messages will be ignored.
Automatic builds can be enabled for any *fork* of the Lean repository.
We just have to go to our fork page at github; select `settings` (it is an icon on the right hand side of the page);
select `Service Hooks`; select `Travis`; and provide the required information.
We must have an account at Travis.
By default, build reports are sent to the [lean-build](https://groups.google.com/forum/#!forum/lean-build) Google group.
You can change that by modifying the file [.travis.yml](../../.travis.yml) in the Lean root directory. The file contains a
`recipients:` entry.

3
script/ci.sh
View file

@ -4,7 +4,4 @@ mkdir build
cd build
eval cmake ../src $CMAKE_OPTIONS
cmake --build .
# -T to create .xml file for CI display
# `<&-` to close stdin so that assertion dialog doesn't wait for input
ctest -j8 --output-on-failure --no-compress-output -T Test <&-
cpack

6
shell.nix
View file

@ -2,10 +2,12 @@
let
lean = import ./default.nix args;
temci = import (builtins.fetchGit { url = http://github.com/parttimenerd/temci.git; rev = "4cae802606b871021394e250a280a2154b92f44b"; }) { inherit pkgs; };
temci = (import (builtins.fetchGit { url = http://github.com/parttimenerd/temci.git; rev = "4cae802606b871021394e250a280a2154b92f44b"; }) { inherit pkgs; }).override {
doCheck = false;
};
in pkgs.mkShell.override { stdenv = lean.stdenv; } rec {
inputsFrom = [ lean ];
buildInputs = with pkgs; [ temci ];
buildInputs = with pkgs; [ temci ccache ];
# https://github.com/NixOS/nixpkgs/issues/60919
hardeningDisable = [ "all" ];
# more convenient `ctest` output