diff --git a/.appveyor.yml b/.appveyor.yml
deleted file mode 100644
index 7423438e68..0000000000
--- a/.appveyor.yml
+++ /dev/null
@@ -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
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 0000000000..9d05528e87
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -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'
diff --git a/.travis.yml b/.travis.yml
deleted file mode 100644
index 0df10d7cc5..0000000000
--- a/.travis.yml
+++ /dev/null
@@ -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
diff --git a/azure-pipelines.yml b/azure-pipelines.yml
deleted file mode 100644
index 5283318c87..0000000000
--- a/azure-pipelines.yml
+++ /dev/null
@@ -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
diff --git a/doc/make/travis.md b/doc/make/travis.md
deleted file mode 100644
index a91982d584..0000000000
--- a/doc/make/travis.md
+++ /dev/null
@@ -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.
diff --git a/script/ci.sh b/script/ci.sh
index 137abc506e..e754765ab9 100755
--- a/script/ci.sh
+++ b/script/ci.sh
@@ -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
diff --git a/shell.nix b/shell.nix
index 63b0ff7f03..1f1e1ce44b 100644
--- a/shell.nix
+++ b/shell.nix
@@ -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