diff --git a/.github/workflows/test_linux.yml b/.github/workflows/test_linux.yml new file mode 100644 index 00000000..1c0d6cef --- /dev/null +++ b/.github/workflows/test_linux.yml @@ -0,0 +1,32 @@ +name: Test on Linux + +on: [push] + +jobs: + build: + + runs-on: ubuntu-latest + strategy: + matrix: + python-version: [3.5, 3.6, 3.7, 3.8] + + steps: + - uses: actions/checkout@v2 + - name: Set up Python ${{ matrix.python-version }} + uses: actions/setup-python@v1 + with: + python-version: ${{ matrix.python-version }} + - name: Install dependencies + run: | + python -m pip install --upgrade pip + - name: Install elan + run: | + curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain leanprover-community/lean:3.5.1 -y + echo "##[add-path]$HOME/.elan/bin" + shell: bash + - name: Test with pytest + run: | + pip install pytest + pip install . + pytest + diff --git a/.github/workflows/test_macos.yml b/.github/workflows/test_macos.yml new file mode 100644 index 00000000..24034ad3 --- /dev/null +++ b/.github/workflows/test_macos.yml @@ -0,0 +1,33 @@ +name: Test on MacOS + +on: [push] + +jobs: + build: + + runs-on: macos-latest + strategy: + matrix: + python-version: [3.5, 3.6, 3.7, 3.8] + + steps: + - uses: actions/checkout@v2 + - name: Set up Python ${{ matrix.python-version }} + uses: actions/setup-python@v1 + with: + python-version: ${{ matrix.python-version }} + - name: Install dependencies + run: | + python -m pip install --upgrade pip + brew install gmp coreutils + - name: Install elan + run: | + curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain leanprover-community/lean:3.5.1 -y + echo "##[add-path]$HOME/.elan/bin" + shell: bash + - name: Test with pytest + run: | + pip install pytest + pip install . + pytest + diff --git a/.github/workflows/test_win.yml b/.github/workflows/test_win.yml new file mode 100644 index 00000000..42ea4a6f --- /dev/null +++ b/.github/workflows/test_win.yml @@ -0,0 +1,32 @@ +name: Test on Windows + +on: [push] + +jobs: + build: + + runs-on: windows-latest + strategy: + matrix: + python-version: [3.5, 3.6, 3.7, 3.8] + + steps: + - uses: actions/checkout@v2 + - name: Set up Python ${{ matrix.python-version }} + uses: actions/setup-python@v1 + with: + python-version: ${{ matrix.python-version }} + - name: Install dependencies + run: | + python -m pip install --upgrade pip + - name: Install elan + run: | + curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain leanprover-community/lean:3.5.1 -y + echo "##[add-path]C:\Users\runneradmin\.elan\bin" + shell: bash + - name: Test with pytest + run: | + pip install pytest + pip install . + pytest + diff --git a/.gitignore b/.gitignore index 4b75ffb3..82c4b7a2 100644 --- a/.gitignore +++ b/.gitignore @@ -3,4 +3,10 @@ /leanpkg.path _cache __pycache__ -*.pyc \ No newline at end of file +*.pyc +*.mypy_cache +.python-version +.tox +build +dist +*.egg-info diff --git a/.mergify.yml b/.mergify.yml deleted file mode 100644 index 13d0e8e6..00000000 --- a/.mergify.yml +++ /dev/null @@ -1,40 +0,0 @@ -pull_request_rules: - - name: automatic merge on CI success and review - pr - conditions: - - status-success=continuous-integration/travis-ci/pr - - status-success=continuous-integration/appveyor/pr - - "#changes-requested-reviews-by=0" - - base=master - - label=ready-to-merge - - approved-reviews-by=@leanprover-community/mathlib-maintainers - actions: - delete_head_branch: {} - merge: - method: squash - strict: smart - strict_method: merge - # second condition necessary, as mergify was failing if the travis "pr" build - # finished before the travis "push" build due to branch protection setting requiring - # the "push" build to complete before a merge - - name: automatic merge on CI success and review - push - conditions: - - status-success=continuous-integration/travis-ci/push - - status-success=continuous-integration/travis-ci/pr - - status-success=continuous-integration/appveyor/pr - - "#changes-requested-reviews-by=0" - - base=master - - label=ready-to-merge - - approved-reviews-by=@leanprover-community/mathlib-maintainers - actions: - delete_head_branch: {} - merge: - method: squash - strict: smart - strict_method: merge - - - name: remove outdated reviews - conditions: - - base=master - actions: - dismiss_reviews: - approved: True diff --git a/.travis.yml b/.travis.yml deleted file mode 100644 index 5d464b32..00000000 --- a/.travis.yml +++ /dev/null @@ -1,85 +0,0 @@ -language: c -sudo: false -env: - global: - - secure: "HxnRtl6pMc+nbszQgDgvMuroMG5AuviULPb0MxPfEIZqYSwKALgc0ILXc89kJyf9rFfpsUdKGmtrGOytzXIp8Yuxvp+fnk/rtuuRyMLeWA0sJ75/Jn+l0BKVid6LNwl7bA4aMOSkjL85kaxU2e5HtlROUkiAgmdAcV10BoK7Vh7yC/S4Zl3kzyCQd8AGSxk0AbeQrb9vK7T1+gWVkEjUFtUsFJ3q5SGrO/j3825qLoRnYj/bKUgtYExQNKjTnTYMbeok+mKJEO1VbLeTk1ri8bLyO2x25lhGImaJSgdPOzuH905ALrf+EHkKm/FYvy5w+zERiuidwwFK5OqVOVWsD5W0G5rYKmDKpzSd39FNnrvb2Tzl2kCin70j6SDOXyZ+4k/iGJpBnOtx3+Ez4gsBDWLIba1c5EXvzhvPoycddgSLBY2LNz4EJI+YqbBTBxG7dVr4NmKKjPowFerVMLM10SgkH9ZZjbAVMxejUJTzp/4gxTanlWm/xds5uC0E0mraLY1H1yzGtwij/lVJN8RGbuhvW9jluLYQzfN7Hb/MReBXTKwdVo5SnsZzv9GEM56IsQXgIhzRoHAuDHd8rS1rfXGaOVfsbYK7pBjtx9j+Pq3BNSPlIL5u4j2JXH6QVJSNaK1npCq81S21dIBfYTP49ft28bhgVE0czkD7kl3fCCk=" - -cache: - directories: - - $HOME/.elan - -install: - - | - if [ ! -d "$HOME/.elan/toolchains/" ]; then - curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y - fi - - source ~/.elan/env - - mkdir $HOME/scripts || echo "" - - export PATH="$HOME/scripts:$PATH" - - export OLEAN_RS=https://github.com/cipher1024/olean-rs/releases - - export latest=$(curl -sSf "$OLEAN_RS/latest" | cut -d'"' -f2 | awk -F/ '{print $NF}') - - curl -sSfL "$OLEAN_RS/download/$latest/olean-rs-linux" -o "$HOME/scripts/olean-rs" - - chmod +x $HOME/scripts/olean-rs - - cp travis_long.sh $HOME/scripts/travis_long - - chmod +x $HOME/scripts/travis_long - - git clean -d -f -q - - export LEAN_VERSION=lean-`lean --run scripts/lean_version.lean` - -jobs: - include: - - language: python - python: - - "3.6" - install: - - if [ "$GITHUB_CRED" != "" ]; then git config --add github.oauthtoken $GITHUB_CRED; echo setting up GitHub credentials; else echo no GitHub credentials available; fi - os: - - linux - script: - - cp scripts/leanpkg-example.toml leanpkg.toml - - pip3 install . - - update-mathlib - - cache-olean - - yes | setup-lean-git-hooks - - - language: sh - install: - - if [ "$GITHUB_CRED" != "" ]; then git config --add github.oauthtoken $GITHUB_CRED; echo setting up GitHub credentials; else echo no GitHub credentials available; fi - os: - - osx - script: - - cp scripts/leanpkg-example.toml leanpkg.toml - - pip3 install . - - update-mathlib - - cache-olean - - yes | setup-lean-git-hooks - - - sudo: true - language: python - python: - - "3.5" - install: - - if [ "$GITHUB_CRED" != "" ]; then git config --add github.oauthtoken $GITHUB_CRED; echo setting up GitHub credentials; else echo no GitHub credentials available; fi - os: - - linux - script: - - cp scripts/leanpkg-example.toml leanpkg.toml - - pip3 install . - - cd scripts - - update-mathlib - - cache-olean - - cache-olean --fetch - - yes | setup-lean-git-hooks - - - language: sh - install: - - if [ "$GITHUB_CRED" != "" ]; then git config --add github.oauthtoken $GITHUB_CRED; echo setting up GitHub credentials; else echo no GitHub credentials available; fi - os: - - osx - script: - - cp scripts/leanpkg-example.toml leanpkg.toml - - pip3 install . - - cd scripts - - update-mathlib - - cache-olean - - cache-olean --fetch - - yes | setup-lean-git-hooks diff --git a/README.md b/README.md index 413c5db9..f2c08835 100644 --- a/README.md +++ b/README.md @@ -1,13 +1,10 @@ # mathlib-tools -[![Build Status](https://travis-ci.org/leanprover-community/mathlib-tools.svg?branch=master)](https://travis-ci.org/leanprover-community/mathlib-tools) -[![Build status](https://ci.appveyor.com/api/projects/status/t353pkb62tep1rth?svg=true)](https://ci.appveyor.com/project/cipher1024/mathlib-tools) +![Test on Linux](https://github.com/leanprover-community/mathlib-tools/workflows/Test%20on%20Linux/badge.svg) +![Test on MacOS](https://github.com/leanprover-community/mathlib-tools/workflows/Test%20on%20MacOS/badge.svg) +![Test on Windows](https://github.com/leanprover-community/mathlib-tools/workflows/Test%20on%20Windows/badge.svg) -This package contains several supporting tools for [Lean mathlib](https://leanprover-community.github.io/). - - - `update-mathlib` fetches precompiled olean files if you use mathlib as a dependency - - `cache-olean` caches olean files, and if you're working on mathlib it can also fetch precompiled olean files from github - - `setup-lean-git-hooks` automates the usage of `cache-olean` using git hooks +This package contains `leanproject`, a supporting tool for [Lean mathlib](https://leanprover-community.github.io/). See also [the documentation in the mathlib repository](https://github.com/leanprover-community/mathlib/blob/8700aa7d78b10b65cf8db1d9e320872ae313517a/docs/contribute/index.md). diff --git a/appveyor.yml b/appveyor.yml deleted file mode 100644 index 41fec4d0..00000000 --- a/appveyor.yml +++ /dev/null @@ -1,47 +0,0 @@ -version: 1.0.{build} -build: off -# only_commits: -# files: -# - scripts/* -# - appveyor.yml - -environment: - GITHUB_CRED: - secure: RPr/nQN2GbjWFfbUiBzpVeO/ojQYoAeqHjOAUhvzHk3DnrbY72zR6yUQQ8AETGtG - matrix: - - PYTHON: "Python36" - PYTHON_VERSION: "3.6.x" - PYTHON_ARCH: "32" - - PYTHON: "Python36" - PYTHON_VERSION: "3.6.x" - PYTHON_ARCH: "64" - -test_script: - - sh -c "if [ '%GITHUB_CRED%' != '' ]; then git config --add github.oauthtoken %GITHUB_CRED%; echo setting up GitHub credentials; else echo no GitHub credentials available; fi" - - "SET PATH=C:\\Users\\appveyor\\AppData\\Roaming\\Python\\%PYTHON%\\Scripts;C:\\%PYTHON%;C:\\%PYTHON%\\Scripts; %PATH%" - - sh -c "echo export PATH=\\\"/c/Users/appveyor/AppData/Roaming/Python/%PYTHON%/Scripts:/c/%PYTHON%:/c/%PYTHON%/Scripts:\$PATH\\\" >> $HOME/.profile" - - "python --version" - - cp scripts/leanpkg-example.toml leanpkg.toml - - sh -c "ln -s `which python` `which python`3" - - sh -c "pip3 install ." - - sh -c "source $HOME/.profile; update-mathlib" - - sh -c "source $HOME/.profile; yes | setup-lean-git-hooks" - - sh -c "source $HOME/.profile; cache-olean" - - # what if it's already installed? - - sh -c "pip3 install ." - - sh -c "source $HOME/.profile; update-mathlib" - - sh -c "source $HOME/.profile; yes | setup-lean-git-hooks" - - sh -c "source $HOME/.profile; cache-olean" - - - sh -c "pip3 install ." - - sh -c "source $HOME/.profile; update-mathlib" - - sh -c "source $HOME/.profile; cache-olean" - - sh -c "source $HOME/.profile; cache-olean --fetch" - - sh -c "source $HOME/.profile; yes | setup-lean-git-hooks" - # do it again - - sh -c "pip3 install ." - - sh -c "source $HOME/.profile; update-mathlib" - - sh -c "source $HOME/.profile; cache-olean" - - sh -c "source $HOME/.profile; cache-olean --fetch" - - sh -c "source $HOME/.profile; yes | setup-lean-git-hooks" diff --git a/bin/cache-olean b/bin/cache-olean deleted file mode 100755 index 2942db47..00000000 --- a/bin/cache-olean +++ /dev/null @@ -1,107 +0,0 @@ -#!/usr/bin/env python3 -import os.path -import os -import sys -import tarfile -import signal -from git import Repo, InvalidGitRepositoryError - -from mathlibtools.delayed_interrupt import DelayedInterrupt -from mathlibtools.fetching import mathlib_asset, fetch_mathlib - - -def make_cache(fn): - if os.path.exists(fn): - os.remove(fn) - - with DelayedInterrupt([signal.SIGTERM, signal.SIGINT]): - ar = tarfile.open(fn, 'w|bz2') - if os.path.exists('src/'): ar.add('src/') - if os.path.exists('test/'): ar.add('test/') - ar.close() - print('... successfully made olean cache.') - - -def should_proceed_with_dirty_repo(action): - if action == ['--fetch-even-if-dirty']: - return True - if action == ['--fetch']: - print('Your repo is dirty; fetching in this state could cause you to lose data. '\ - 'To proceed regardless, use --fetch-even-if-dirty.') - else: - print('Your repo is dirty; commit or discard your changes to perform this action.') - return False - -if __name__ == "__main__": - try: - repo = Repo('.', search_parent_directories=True) - except InvalidGitRepositoryError: - print('This does not seem to be a git repository.') - sys.exit(-1) - - if repo.bare: - print('Repository not initialized') - sys.exit(-1) - - if repo.is_dirty(): - if not should_proceed_with_dirty_repo(sys.argv[1:]): - sys.exit(-1) - print('Warning: proceeding with dirty repo.') - - root_dir = repo.working_tree_dir - os.chdir(root_dir) - rev = repo.commit().hexsha - - cache_dir = os.path.join(root_dir, "_cache") - if not os.path.exists(cache_dir): - os.makedirs(cache_dir) - fn = os.path.join(cache_dir, 'olean-' + rev + ".bz2") - - if sys.argv[1:] == ['--fetch'] or sys.argv[1:] == ['--fetch-even-if-dirty']: - if os.path.exists(fn): - ar = tarfile.open(fn, 'r') - ar.extractall(root_dir) - ar.close() - print('... successfully fetched local cache.') - else: - asset = mathlib_asset(rev) - if asset: - fetch_mathlib(asset) - else: - print('no cache found') - elif sys.argv[1:] == ['--build']: - os.system('leanpkg build') - make_cache(fn) # we make the cache even if the build failed - elif sys.argv[1:] == ['--build-all']: - for b in repo.branches: - print("Switching to branch " + b.name) - try: - b.checkout() - except Exception as e: - print("Failed to switch branch:") - print(repr(e)) - continue - rev = repo.commit().hexsha - fn = os.path.join(cache_dir, 'olean-' + rev + ".bz2") - os.system('leanpkg build') - make_cache(fn) # we make the cache even if the build failed - elif sys.argv[1:] == ['--build-new']: - for b in repo.branches: - rev = b.commit.hexsha - fn = os.path.join(cache_dir, 'olean-' + rev + ".bz2") - if os.path.exists(fn): - print("Branch already built: " + b.name) - else: - print("Building branch: " + b.name) - try: - b.checkout() - except Exception as e: - print("Failed to switch branch:") - print(repr(e)) - continue - os.system('leanpkg build') - make_cache(fn) # we make the cache even if the build failed - elif sys.argv[1:] == []: - make_cache(fn) - else: - print('usage: cache-olean [--fetch | --fetch-even-if-dirty | --build | --build-all | --build-new]') diff --git a/bin/setup-lean-git-hooks b/bin/setup-lean-git-hooks deleted file mode 100755 index 75b01d6b..00000000 --- a/bin/setup-lean-git-hooks +++ /dev/null @@ -1,25 +0,0 @@ -#!/usr/bin/env python3 - -import sys -import shutil -from pathlib import Path -import mathlibtools -from git import Repo - - -repo = Repo('.', search_parent_directories=True) -hook_dir = Path(repo.git_dir) / 'hooks' -mathlib_dir = Path(mathlibtools.__file__).parent - -if hook_dir.exists(): - print('This script will copy post-commit and post-checkout scripts to ', hook_dir) - rep = input("Do you want to proceed (y/n)? ") - if rep in ['y', 'Y']: - shutil.copy(str(mathlib_dir/'post-commit'), str(hook_dir)) - shutil.copy(str(mathlib_dir/'post-checkout'), str(hook_dir)) - print("Successfully copied scripts") - else: - print("Cancelled...") -else: - print('No git repo found') - sys.exit(-1) diff --git a/bin/update-mathlib b/bin/update-mathlib deleted file mode 100755 index e6a88bf4..00000000 --- a/bin/update-mathlib +++ /dev/null @@ -1,51 +0,0 @@ -#!/usr/bin/env python3 - -import os.path -import os -import sys -import toml - -from mathlibtools.fetching import mathlib_asset, fetch_mathlib - -# find root of project and leanpkg.toml -cwd = os.getcwd() -while not os.path.isfile('leanpkg.toml') and os.getcwd() != '/': - os.chdir(os.path.dirname(os.getcwd())) - -# parse leanpkg.toml -try: - leanpkg = toml.load('leanpkg.toml') -except FileNotFoundError: - print('Error: No leanpkg.toml found') - sys.exit(1) - -try: - lib = leanpkg['dependencies']['mathlib'] -except KeyError: - print('Error: Project does not depend on mathlib') - sys.exit(1) - -try: - git_url = lib['git'] - rev = lib['rev'] -except KeyError: - print('Error: Project seems to refer to a local copy of mathlib ' - 'instead of a GitHub repository') - sys.exit(1) - -# some leanpkg files might contain urls ending in '/' -git_url = git_url.rstrip('/') - -if git_url not in ['https://github.com/leanprover/mathlib', - 'git@github.com:leanprover/mathlib.git', - 'https://github.com/leanprover-community/mathlib', - 'git@github.com:leanprover-community/mathlib.git']: - print('Error: mathlib reference', git_url, 'seems to be a fork') - sys.exit(1) - -asset = mathlib_asset(rev) -# Get archive if needed -if asset: - fetch_mathlib(asset, target='_target/deps/mathlib') -else: - print('no cache found') diff --git a/default.nix b/default.nix index 0bfc3ec0..38cf8b2e 100644 --- a/default.nix +++ b/default.nix @@ -3,10 +3,12 @@ with pkgs.python3Packages; buildPythonApplication { pname = "mathlib-tools"; - version = "0.0.2"; + version = "0.0.3"; src = ./.; + doCheck = false; + propagatedBuildInputs = [ - PyGithub GitPython toml + PyGithub GitPython toml click tqdm ]; } diff --git a/mathlibtools/auth_github.py b/mathlibtools/auth_github.py index ceaeef4a..928d9503 100644 --- a/mathlibtools/auth_github.py +++ b/mathlibtools/auth_github.py @@ -1,5 +1,5 @@ -from git import Repo, InvalidGitRepositoryError -from github import Github +from git import Repo, InvalidGitRepositoryError # type: ignore +from github import Github # type: ignore import configparser def auth_github(): diff --git a/mathlibtools/fetching.py b/mathlibtools/fetching.py deleted file mode 100644 index e2412bc3..00000000 --- a/mathlibtools/fetching.py +++ /dev/null @@ -1,57 +0,0 @@ -import os.path -import os -import tarfile -import urllib3 -import certifi -import signal - -from mathlibtools.auth_github import auth_github -from mathlibtools.delayed_interrupt import DelayedInterrupt - -def mathlib_asset(rev): - g = auth_github() - print("Querying GitHub...") - repo = g.get_repo("leanprover-community/mathlib-nightly") - tags = {tag.name: tag.commit.sha for tag in repo.get_tags()} - try: - release = next(r for r in repo.get_releases() - if r.tag_name.startswith('nightly-') and - tags[r.tag_name] == rev) - except StopIteration: - print('Error: no nightly archive found') - return None - - try: - asset = next(x for x in release.get_assets() - if x.name.startswith('mathlib-olean-nightly-')) - except StopIteration: - print("Error: Release " + release.tag_name + " does not contains a olean " - "archive (this shouldn't happen...)") - return None - return asset - - -def fetch_mathlib(asset, target='.'): - mathlib_dir = os.path.join(os.environ['HOME'], '.mathlib') - if not os.path.isdir(mathlib_dir): - os.mkdir(mathlib_dir) - - if not os.path.isfile(os.path.join(mathlib_dir, asset.name)): - print("Downloading nightly...") - cd = os.getcwd() - os.chdir(mathlib_dir) - http = urllib3.PoolManager( - cert_reqs='CERT_REQUIRED', - ca_certs=certifi.where()) - req = http.request('GET', asset.browser_download_url) - with DelayedInterrupt([signal.SIGTERM, signal.SIGINT]): - with open(asset.name, 'wb') as f: - f.write(req.data) - os.chdir(cd) - else: - print("Reusing cached olean archive") - - with DelayedInterrupt([signal.SIGTERM, signal.SIGINT]): - ar = tarfile.open(os.path.join(mathlib_dir, asset.name)) - ar.extractall(target) - print("... successfully extracted olean archive.") diff --git a/mathlibtools/leanproject.py b/mathlibtools/leanproject.py new file mode 100644 index 00000000..6c87f3ee --- /dev/null +++ b/mathlibtools/leanproject.py @@ -0,0 +1,202 @@ +import sys +import os +from pathlib import Path +from datetime import datetime + +from git.exc import GitCommandError # type: ignore +import click + +from mathlibtools.lib import (LeanProject, log, LeanDirtyRepo, + InvalidLeanProject, LeanDownloadError, set_download_url) + +# Click aliases from Stephen Rauch at +# https://stackoverflow.com/questions/46641928 +class CustomMultiCommand(click.Group): + def command(self, *args, **kwargs): + """Behaves the same as `click.Group.command()` except if passed + a list of names, all after the first will be aliases for the first. + """ + def decorator(f): + if args and isinstance(args[0], list): + _args = [args[0][0]] + list(args[1:]) + for alias in args[0][1:]: + cmd = super(CustomMultiCommand, self).command( + alias, *args[1:], **kwargs)(f) + cmd.short_help = "Alias for '{}'".format(_args[0]) + else: + _args = args + cmd = super(CustomMultiCommand, self).command( + *_args, **kwargs)(f) + return cmd + + return decorator + +def proj(): + return LeanProject.from_path(Path('.'), cache_url, force_download, + lean_upgrade) + +# The following are global state variables. This is a lazy way of propagating +# the global options. +cache_url = '' +force_download = False +lean_upgrade = True + +@click.group(cls=CustomMultiCommand, context_settings={ 'help_option_names':['-h', '--help']}) +@click.option('--from-url', '-u', default='', nargs=1, + help='Override base url for olean cache.') +@click.option('--force-download', '-f', 'force', default=False, is_flag=True, + help='Download olean cache without looking for a local version.') +@click.option('--no-lean-upgrade', 'noleanup', default=False, is_flag=True, + help='Do not upgrade Lean version when upgrading mathlib.') +def cli(from_url, force, noleanup): + """Command line client to manage Lean projects depending on mathlib. + Use leanproject COMMAND --help to get more help on any specific command.""" + global cache_url, force_download, lean_upgrade + cache_url = from_url + force_download = force + lean_upgrade = not noleanup + +@cli.command() +@click.argument('path', default='.') +def new(path: str = '.'): + """Create a new Lean project and prepare mathlib. + + If no directory name is given, the current directory is used. + """ + LeanProject.new(Path(path), cache_url, force_download) + +@cli.command() +def add_mathlib(): + """Add mathlib to the current project.""" + proj().add_mathlib() + +@cli.command(['upgrade-mathlib', 'update-mathlib', 'up']) +def upgrade_mathlib(): + """Upgrade mathlib (as a dependency or as the main project).""" + try: + proj().upgrade_mathlib() + except LeanDownloadError: + log.error('Failed to fetch mathlib oleans') + sys.exit(-1) + except InvalidLeanProject: + project = LeanProject.user_wide(cache_url, force_download) + project.upgrade_mathlib() + except Exception as err: + log.error(err) + sys.exit(-1) + +@cli.command() +def build(): + """Build the current project.""" + proj().build() + +@cli.command(name='get') +@click.argument('name') +@click.argument('dir', default='') +def get_project(name: str, target: str = ''): + """Clone a project from a GitHub name or git url. + + Put it in dir if this argument is given. + A GitHub name without / will be considered as + a leanprover-community project.""" + if not name.startswith(('git@', 'http')): + if '/' not in name: + name = 'leanprover-community/'+name + name = 'https://github.com/'+name+'.git' + try: + LeanProject.from_git_url(name, target, cache_url, force_download) + except GitCommandError: + log.error('Git command failed') + sys.exit(-1) + except Exception as err: + log.error(err) + sys.exit(-1) + +@cli.command() +@click.option('--force', default=False, + help='Make cache even if the repository is dirty.') +def mk_cache(force: bool = False): + """Cache olean files.""" + try: + proj().mk_cache(force) + except LeanDirtyRepo: + log.error('The repository is dirty, please commit changes before ' + 'making cache, or run this command with option --force.') + sys.exit(-1) + except Exception as err: + log.error(err) + sys.exit(-1) + + +@cli.command() +@click.option('--force', default=False, + help='Get cache even if the repository is dirty.') +def get_cache(force: bool = False): + """Restore cached olean files.""" + try: + proj().get_cache(force) + except LeanDirtyRepo: + log.error('The repository is dirty, please commit changes before ' + 'fetching cache, or run this command with option --force.') + sys.exit(-1) + except (LeanDownloadError, FileNotFoundError): + log.error('Failed to fetch mathlib oleans') + sys.exit(-1) + except Exception as err: + log.error(err) + sys.exit(-1) + +@cli.command() +def hooks(): + """Setup git hooks for the current project.""" + try: + proj().setup_git_hooks() + except Exception as err: + log.error(err) + sys.exit(-1) + +@cli.command() +@click.argument('url') +def set_url(url: str): + """Set the default url where oleans should be fetched.""" + set_download_url(url) + +def check_core(): + """Check that oleans are more recent than their source in core lib""" + now = datetime.now().timestamp() + for toolchain_path in (Path.home()/'.elan'/'toolchains').iterdir(): + if any(p.stat().st_mtime > p.with_suffix('.olean').stat().st_mtime + for p in toolchain_path.glob('**/*.lean')): + print('Some core oleans files in toolchain {} seem older than' + 'their source.'.format(str(toolchain_path))) + touch = input('Do you want to set their modification time to now (y/n) ? ') + if touch.lower() in ['y', 'yes']: + for p in toolchain_path.glob('**/*.olean'): + os.utime(str(p), (now, now)) + +@cli.command() +def check(): + """Check mathlib oleans are more recent than their sources""" + try: + project = proj() + check_core() + if project.check_timestamps(): + log.info('Everything looks fine.') + else: + print('Some mathlib oleans files seem older than their source.') + touch = input('Do you want to set their modification time to now (y/n) ? ') + if touch.lower() in ['y', 'yes']: + project.touch_oleans() + except Exception as err: + log.error(err) + sys.exit(-1) + +@cli.command() +def global_install(): + """Install mathlib user-wide.""" + try: + proj = LeanProject.user_wide(cache_url, force_download) + proj.add_mathlib() + except Exception as err: + log.error(err) + sys.exit(-1) diff --git a/mathlibtools/lib.py b/mathlibtools/lib.py new file mode 100644 index 00000000..36f57645 --- /dev/null +++ b/mathlibtools/lib.py @@ -0,0 +1,474 @@ +from pathlib import Path +import logging +import tempfile +import shutil +import tarfile +import signal +import re +import os +import subprocess +from datetime import datetime +from typing import Iterable, Union, List, Tuple +from tempfile import TemporaryDirectory + +import requests +from tqdm import tqdm # type: ignore +import toml +from git import Repo, InvalidGitRepositoryError, GitCommandError # type: ignore + +from mathlibtools.delayed_interrupt import DelayedInterrupt +from mathlibtools.auth_github import auth_github + +log = logging.getLogger("Mathlib tools") +log.setLevel(logging.INFO) +if (log.hasHandlers()): + log.handlers.clear() +log.addHandler(logging.StreamHandler()) + + +class InvalidLeanProject(Exception): + pass + +class InvalidMathlibProject(Exception): + """A mathlib project is a Lean project depending on mathlib""" + pass + +class LeanDownloadError(Exception): + pass + +class LeanDirtyRepo(Exception): + pass + +class InvalidLeanVersion(Exception): + pass + +def nightly_url(rev: str) -> str: + """From a git rev, try to find an asset name and url.""" + g = auth_github() + repo = g.get_repo("leanprover-community/mathlib-nightly") + tags = {tag.name: tag.commit.sha for tag in repo.get_tags()} + try: + release = next(r for r in repo.get_releases() + if r.tag_name.startswith('nightly-') and + tags[r.tag_name] == rev) + except StopIteration: + raise LeanDownloadError('Error: no nightly archive found') + + try: + asset = next(x for x in release.get_assets() + if x.name.startswith('mathlib-olean-nightly-')) + except StopIteration: + raise LeanDownloadError("Error: Release " + release.tag_name + + " does not contains a olean archive (this shouldn't happen...)") + return asset.browser_download_url + + +DOT_MATHLIB = Path.home()/'.mathlib' +AZURE_URL = 'https://oleanstorage.azureedge.net/mathlib/' + +DOT_MATHLIB.mkdir(parents=True, exist_ok=True) +DOWNLOAD_URL_FILE = DOT_MATHLIB/'url' + +MATHLIB_URL = 'https://github.com/leanprover-community/mathlib.git' +LEAN_VERSION_RE = re.compile(r'(.*)\t.*refs/heads/lean-(.*)') + +VersionTuple = Tuple[int, int, int] + +def mathlib_lean_version() -> VersionTuple: + """Return the latest Lean release supported by mathlib""" + out = subprocess.run(['git', 'ls-remote', '--heads', MATHLIB_URL], + stdout=subprocess.PIPE).stdout.decode() + version = (3, 4, 1) + for branch in out.split('\n'): + m = LEAN_VERSION_RE.match(branch) + if m: + version = max(version, parse_version(m.group(2))) + return version + +def set_download_url(url: str = AZURE_URL) -> None: + """Store the download url in .mathlib.""" + DOWNLOAD_URL_FILE.write_text(url) + +def get_download_url() -> str: + """Get the download url from .mathlib.""" + return DOWNLOAD_URL_FILE.read_text().strip('/\n')+'/' + +if not DOWNLOAD_URL_FILE.exists(): + set_download_url() + +def pack(root: Path, srcs: Iterable[Path], target: Path) -> None: + """Creates, as target, a tar.bz2 archive containing all paths from src, + relative to the folder root""" + try: + target.unlink() + except FileNotFoundError: + pass + cur_dir = Path.cwd() + with DelayedInterrupt([signal.SIGTERM, signal.SIGINT]): + os.chdir(str(root)) + ar = tarfile.open(str(target), 'w|bz2') + for src in srcs: + ar.add(str(src.relative_to(root))) + ar.close() + os.chdir(str(cur_dir)) + +def unpack_archive(fname: Union[str, Path], tgt_dir: Union[str, Path]) -> None: + """Unpack archive. This is needed for python < 3.7.""" + shutil.unpack_archive(str(fname), str(tgt_dir)) + + +def download(url: str, target: Path) -> None: + """Download from url into target""" + log.info('Trying to download {} to {}'.format(url, target)) + try: + req = requests.get(url, stream=True) + req.raise_for_status() + except ConnectionError: + raise LeanDownloadError("Can't connect to " + url) + except requests.HTTPError: + raise LeanDownloadError('Failed to download ' + url) + total_size = int(req.headers.get('content-length', 0)) + BLOCK_SIZE = 1024 + progress = tqdm(total=total_size, unit='iB', unit_scale=True) + with target.open('wb') as tgt: + for data in req.iter_content(BLOCK_SIZE): + progress.update(len(data)) + tgt.write(data) + progress.close() + if total_size != 0 and progress.n != total_size: + raise LeanDownloadError('Failed to download ' + url) + + +def get_mathlib_archive(rev: str, url:str = '', force: bool = False) -> Path: + """Download a mathlib archive for revision rev into .mathlib + + Return the archive Path. Will raise LeanDownloadError if nothing works. + """ + + fname = rev + '.tar.gz' + path = DOT_MATHLIB/fname + if not force: + log.info('Looking for local mathlib oleans') + if path.exists(): + log.info('Found local mathlib oleans') + return path + log.info('Looking for remote mathlib oleans') + try: + base_url = url or get_download_url() + download(base_url+fname, path) + log.info('Found mathlib oleans at '+base_url) + return path + except LeanDownloadError: + pass + log.info('Looking for GitHub mathlib oleans') + download(nightly_url(rev), path) + log.info('Found GitHub mathlib oleans') + return path + +def parse_version(version: str) -> VersionTuple: + """Turn a lean version string into a tuple of integers or raise + InvalidLeanVersion""" + #Something that could be in a branch name or modern leanpkg.toml + m = re.match(r'.*lean[-:](.*)\.(.*)\.(.*).*', version) + if m: + return (int(m.group(1)), int(m.group(2)), int(m.group(3))) + + # The output of `lean -- version` + m = re.match(r'.*version (.*)\.(.*)\.(.*),.*', version) + if m: + return (int(m.group(1)), int(m.group(2)), int(m.group(3))) + + # Only a version string + m = re.match(r'(.*)\.(.*)\.(.*)', version) + if m: + return (int(m.group(1)), int(m.group(2)), int(m.group(3))) + raise InvalidLeanVersion(version) + +def lean_version_toml(version: VersionTuple) -> str: + """Turn a Lean version tuple into the string expected in leanpkg.toml.""" + ver_str = '{:d}.{:d}.{:d}'.format(*version) + if version < (3, 5, 0): + return ver_str + else: + return 'leanprover-community/lean:' + ver_str + + +class LeanProject: + def __init__(self, repo: Repo, is_dirty: bool, rev: str, directory: Path, + pkg_config: dict, deps: dict, + cache_url: str = '', force_download: bool = False, + upgrade_lean: bool = True) -> None: + """A Lean project.""" + self.repo = repo + self.is_dirty = is_dirty + self.rev = rev + self.directory = directory + self.pkg_config = pkg_config + self.deps = deps + self.cache_url = cache_url or get_download_url() + self.force_download = force_download + self.upgrade_lean = upgrade_lean + + @classmethod + def from_path(cls, path: Path, cache_url: str = '', + force_download: bool = False, + upgrade_lean: bool = True) -> 'LeanProject': + """Builds a LeanProject from a Path object""" + try: + repo = Repo(path, search_parent_directories=True) + except InvalidGitRepositoryError: + raise InvalidLeanProject('Invalid git repository') + if repo.bare: + raise InvalidLeanProject('Git repository is not initialized') + is_dirty = repo.is_dirty() + try: + rev = repo.commit().hexsha + except ValueError: + rev = '' + directory = Path(repo.working_dir) + try: + config = toml.load(directory/'leanpkg.toml') + except FileNotFoundError: + raise InvalidLeanProject('Missing leanpkg.toml') + + return cls(repo, is_dirty, rev, directory, + config['package'], config['dependencies'], + cache_url, force_download, upgrade_lean) + + @classmethod + def user_wide(cls, cache_url: str = '', + force_download: bool = False) -> 'LeanProject': + """Return the user-wide LeanProject (living in ~/.lean) + + If the project does not exist, it will be created, using the latest + version of Lean supported by mathlib.""" + directory = Path.home()/'.lean' + try: + config = toml.load(directory/'leanpkg.toml') + except FileNotFoundError: + directory.mkdir(exist_ok=True) + version = mathlib_lean_version() + if version <= (3, 4, 2): + version_str = '.'.join(map(str, version)) + else: + version_str = 'leanprover-community/lean:' +\ + '.'.join(map(str, version)) + + pkg = { 'name': '_user_local_packages', + 'version': '1', + 'lean_version': version_str } + with (directory/'leanpkg.toml').open('w') as pkgtoml: + toml.dump({'package': pkg}, pkgtoml) + config = { 'package': pkg, 'dependencies': dict() } + + return cls(None, False, '', directory, + config['package'], config['dependencies'], + cache_url, force_download) + + @property + def name(self) -> str: + return self.pkg_config['name'] + + @property + def lean_version(self) -> VersionTuple: + return parse_version(self.pkg_config['lean_version']) + + @lean_version.setter + def lean_version(self, version: VersionTuple) -> None: + self.pkg_config['lean_version'] = lean_version_toml(version) + + + @property + def is_mathlib(self): + return self.name == 'mathlib' + + @property + def mathlib_rev(self) -> str: + if self.is_mathlib: + return self.rev + if 'mathlib' not in self.deps: + raise InvalidMathlibProject('This project does not depend on mathlib') + try: + rev = self.deps['mathlib']['rev'] + except KeyError: + raise InvalidMathlibProject( + 'Project seems to refer to a local copy of mathlib ' + 'instead of a GitHub repository') + return rev + + @property + def mathlib_folder(self) -> Path: + if self.is_mathlib: + return self.directory + else: + return self.directory/'_target'/'deps'/'mathlib' + + def read_config(self) -> None: + try: + config = toml.load(self.directory/'leanpkg.toml') + except FileNotFoundError: + raise InvalidLeanProject('Missing leanpkg.toml') + + self.deps = config['dependencies'] + self.pkg_config = config['package'] + + def write_config(self) -> None: + """Write leanpkg.toml for this project.""" + # Fix leanpkg lean_version bug if needed (the lean_version property + # setter is working here, hence the weird line). + self.lean_version = self.lean_version + + # Note we can't blindly use toml.dump because we need dict as values + # for dependencies. + with (self.directory/'leanpkg.toml').open('w') as cfg: + cfg.write('[package]\n') + cfg.write(toml.dumps(self.pkg_config)) + cfg.write('\n[dependencies]\n') + for dep, val in self.deps.items(): + nval = str(val).replace("'git':", 'git =').replace( + "'rev':", 'rev =').replace("'", '"') + cfg.write('{} = {}\n'.format(dep, nval)) + + def get_mathlib_olean(self) -> None: + """Get precompiled mathlib oleans for this project.""" + self.mathlib_folder.mkdir(parents=True, exist_ok=True) + unpack_archive(get_mathlib_archive(self.mathlib_rev, self.cache_url, + self.force_download), + self.mathlib_folder) + # Let's now touch oleans, just in case + self.touch_oleans() + + def mk_cache(self, force: bool = False) -> None: + """Cache oleans for this project.""" + if self.is_dirty and not force: + raise LeanDirtyRepo + if not self.rev: + raise ValueError('This project has no git commit.') + tgt_folder = DOT_MATHLIB if self.is_mathlib else self.directory/'_cache' + tgt_folder.mkdir(exist_ok=True) + archive = tgt_folder/(str(self.rev) + '.tar.bz2') + if archive.exists(): + log.info('Cache for revision {} already exists'.format(self.rev)) + return + pack(self.directory, filter(Path.exists, [self.directory/'src', self.directory/'test']), + archive) + + def get_cache(self, force: bool = False, url:str = '') -> None: + """Tries to get olean cache. + + Will raise LeanDownloadError or FileNotFoundError if no archive exists. + """ + if self.is_dirty and not force: + raise LeanDirtyRepo + if self.is_mathlib: + self.get_mathlib_olean() + else: + unpack_archive(self.directory/'_cache'/(str(self.rev)+'.tar.bz2'), + self.directory) + + @classmethod + def from_git_url(cls, url: str, target: str = '', cache_url: str = '', + force_download: bool = False) -> 'LeanProject': + """Download a Lean project using git and prepare mathlib if needed.""" + target = target or url.split('/')[-1].split('.')[0] + repo = Repo.clone_from(url, target) + proj = cls.from_path(Path(repo.working_dir), cache_url, force_download) + proj.run(['leanpkg', 'configure']) + if 'mathlib' in proj.deps: + proj.get_mathlib_olean() + return proj + + @classmethod + def new(cls, path: Path = Path('.'), cache_url: str = '', + force_download: bool = False) -> 'LeanProject': + """Create a new Lean project and prepare mathlib.""" + if path == Path('.'): + subprocess.run(['leanpkg', 'init', path.absolute().name]) + else: + subprocess.run(['leanpkg', 'new', str(path)]) + + proj = cls.from_path(path, cache_url, force_download) + proj.write_config() + proj.add_mathlib() + return proj + + def run(self, args: List[str]) -> None: + """Run a command in the project directory. + + args is a list as in subprocess.run""" + subprocess.run(args, cwd=str(self.directory)) + + def build(self) -> None: + log.info('Building project '+self.name) + self.run(['leanpkg', 'build']) + + def upgrade_mathlib(self) -> None: + """Upgrade mathlib in the project. + + In case this project is mathlib, we assume we are already on the branch + we want. + """ + if self.is_mathlib: + try: + rem = next(remote for remote in self.repo.remotes + if any('leanprover' in url + for url in remote.urls)) + rem.pull(self.repo.active_branch) + except (StopIteration, GitCommandError): + log.info("Couldn't pull from a relevant git remote. " + "You may try to git pull manually and then " + "run `leanproject get-cache`") + return + self.rev = self.repo.commit().hexsha + else: + try: + shutil.rmtree(str(self.mathlib_folder)) + except FileNotFoundError: + pass + if self.upgrade_lean: + mathlib_lean = mathlib_lean_version() + + if mathlib_lean > self.lean_version: + self.lean_version = mathlib_lean + self.write_config() + self.run(['leanpkg', 'upgrade']) + self.read_config() + self.get_mathlib_olean() + + def add_mathlib(self) -> None: + """Add mathlib to the project.""" + if 'mathlib' in self.deps: + log.info('This project already depends on mathlib') + return + log.info('Adding mathlib') + self.run(['leanpkg', 'add', 'leanprover-community/mathlib']) + log.debug('Configuring') + self.run(['leanpkg', 'configure']) + self.read_config() + self.get_mathlib_olean() + + def setup_git_hooks(self) -> None: + hook_dir = Path(self.repo.git_dir)/'hooks' + src = Path(__file__).parent + print('This script will copy post-commit and post-checkout scripts to ', hook_dir) + rep = input("Do you want to proceed (y/n)? ") + if rep in ['y', 'Y']: + shutil.copy(str(src/'post-commit'), str(hook_dir)) + shutil.copy(str(src/'post-checkout'), str(hook_dir)) + print("Successfully copied scripts") + else: + print("Cancelled...") + + def touch_oleans(self) -> None: + """Set modification time for mathlib oleans to now""" + now = datetime.now().timestamp() + for p in (self.mathlib_folder/'src').glob('**/*.olean'): + os.utime(str(p), (now, now)) + + def check_timestamps(self) -> bool: + """Check that mathlib oleans are more recent than their sources""" + try: + return all(p.stat().st_mtime < p.with_suffix('.olean').stat().st_mtime + for p in (self.mathlib_folder/'src').glob('**/*.lean')) + except FileNotFoundError: + return False diff --git a/mathlibtools/post-checkout b/mathlibtools/post-checkout index 91013c6c..553d3fd0 100755 --- a/mathlibtools/post-checkout +++ b/mathlibtools/post-checkout @@ -1,5 +1,5 @@ #!/bin/sh -# SourceTree on OS X provides a defective path that doesn't contain pythong +# SourceTree on OS X provides a defective path that doesn't contain python # https://jira.atlassian.com/browse/SRCTREE-6540 export PATH=$PATH:/usr/local/bin @@ -10,7 +10,7 @@ CHANGED_BRANCH=$3 if [ "$CHANGED_BRANCH" -eq "1" ]; then if /usr/bin/env python3 -c ""; then echo "Trying to fetch cached olean" - cache-olean --fetch + leanproject get-cache else echo "'env python3' failed; not running post-checkout hook" fi diff --git a/mathlibtools/post-commit b/mathlibtools/post-commit index ac61046c..d25949e0 100755 --- a/mathlibtools/post-commit +++ b/mathlibtools/post-commit @@ -1,5 +1,5 @@ #!/bin/sh -# SourceTree on OS X provides a defective path that doesn't contain pythong +# SourceTree on OS X provides a defective path that doesn't contain python # https://jira.atlassian.com/browse/SRCTREE-6540 export PATH=$PATH:/usr/local/bin @@ -7,7 +7,7 @@ export PATH=$PATH:/usr/local/bin # if python3 isn't available, we don't generate an error; just a message if /usr/bin/env python3 -c ""; then echo "Caching olean..." - cache-olean + leanproject mk-cache else echo "'env python3' failed; not running post-checkout hook" fi diff --git a/setup.py b/setup.py index c7c35fc9..dbe0be92 100644 --- a/setup.py +++ b/setup.py @@ -5,22 +5,23 @@ setuptools.setup( name="mathlibtools", - version="0.0.2", + version="0.0.3", author="The mathlib community", description="Lean prover mathlib supporting tools.", long_description=long_description, long_description_content_type="text/markdown", url="https://github.com/leanprover-community/mathlib-tools", packages=setuptools.find_packages(), - scripts=[ - 'bin/cache-olean', - 'bin/update-mathlib', - 'bin/setup-lean-git-hooks'], + entry_points={ + "console_scripts": [ + "leanproject = mathlibtools.leanproject:cli", + ]}, package_data = { 'mathlibtools': ['post-commit', 'post-checkout'] }, classifiers=[ "Programming Language :: Python :: 3", "License :: OSI Approved :: Apache Software License", "Operating System :: OS Independent" ], python_requires='>=3.5', - install_requires=['toml', 'PyGithub', 'certifi', 'gitpython', 'requests'] + install_requires=['toml', 'PyGithub', 'certifi', 'gitpython', 'requests', + 'Click', 'tqdm'] ) diff --git a/tests/test_functional.py b/tests/test_functional.py new file mode 100644 index 00000000..d80034b4 --- /dev/null +++ b/tests/test_functional.py @@ -0,0 +1,67 @@ +import os +import re +import subprocess +from pathlib import Path + +def chdir(path): + # Fighting old pythons... + os.chdir(str(path)) + +LEAN_VERSION_RE = re.compile(r'.*lean_version = "(3.[5-9][^"]*).*"', re.DOTALL) + +MATHLIB_REV_RE = re.compile(r".*mathlib.* = 'rev': '([^']*)'.*", re.DOTALL) + +def fix_leanpkg_bug(): + """Fix the leanpkg toolchain bug in current folder.""" + leanpkg = Path('leanpkg.toml') + conf = leanpkg.read_text() + m = LEAN_VERSION_RE.match(conf) + if m: + ver = m.group(1) + leanpkg.write_text(conf.replace(ver, 'leanprover-community/lean:'+ver)) + +# The next helper is currently unused, but could be used in later tests. +def change_mathlib_rev(rev): + """Change the mathlib SHA in current folder.""" + leanpkg = Path('leanpkg.toml') + conf = leanpkg.read_text() + m = MATHLIB_REV_RE.match(conf) + if m: + old_rev = m.group(1) + leanpkg.write_text(conf.replace(old_rev, rev)) + +def test_new(tmpdir): + """Create a new package and check mathlib oleans are there.""" + chdir(tmpdir) + subprocess.run(['leanproject', 'new']) + assert (tmpdir/'leanpkg.path').exists() + assert (tmpdir/'_target'/'deps'/'mathlib'/'src'/'algebra'/'default.olean').exists() + +def test_add(tmpdir): + """Add mathlib to a project and check mathlib oleans are there.""" + chdir(tmpdir) + subprocess.run(['leanpkg', 'init', 'project']) + fix_leanpkg_bug() + subprocess.run(['leanproject', 'add-mathlib']) + assert (tmpdir/'_target'/'deps'/'mathlib'/'src'/'algebra'/'default.olean').exists() + +def test_upgrade_project(tmpdir): + chdir(tmpdir) + subprocess.run(['leanpkg', 'init', 'project']) + fix_leanpkg_bug() + leanpkg = Path('leanpkg.toml') + leanpkg.write_text(leanpkg.read_text() + + 'mathlib = {git = "https://github.com/leanprover-community/mathlib",' + 'rev = "a9ed54ca0329771deab21d7574d7d19b417bf4a3"}') + subprocess.run(['leanproject', 'upgrade-mathlib']) + assert (tmpdir/'_target'/'deps'/'mathlib'/'src'/'algebra'/'default.olean').exists() + +def test_upgrade_mathlib(tmpdir): + chdir(tmpdir) + subprocess.run(['git', 'clone', 'https://github.com/leanprover-community/mathlib']) + chdir(tmpdir/'mathlib') + subprocess.run(['git', 'checkout', 'lean-3.5.1']) + subprocess.run(['git', 'reset', '--hard', 'a9ed54ca0329771deab21d7574d7d19b417bf4a3']) + subprocess.run(['leanproject', 'upgrade-mathlib']) + assert (tmpdir/'mathlib'/'src'/'algebra'/'default.olean').exists() + diff --git a/tox.ini b/tox.ini new file mode 100644 index 00000000..10f00b25 --- /dev/null +++ b/tox.ini @@ -0,0 +1,13 @@ +[tox] +envlist = py35, py36, py37, py38, mypy + +[testenv] +commands= + pip install pytest + pytest + +[testenv:mypy] +basepython = python3.5 +deps = mypy +setenv = MYPYPATH={toxinidir} +commands = mypy mathlibtools diff --git a/travis_long.sh b/travis_long.sh deleted file mode 100644 index 380e316a..00000000 --- a/travis_long.sh +++ /dev/null @@ -1,26 +0,0 @@ -#!/bin/bash - - -# -# This script is taken from: -# -# https://docs.haskellstack.org/en/stable/travis_ci/ -# https://github.com/futurice/fum2github/blob/master/travis_long - -# The following explains the 50min hard timeout on macs -# https://github.com/travis-ci/travis-ci/issues/3810 - -$* & -pidA=$! -minutes=0 - -while true; do sleep 60; ((minutes++)); echo -e "\033[0;32m$minutes minute(s) elapsed.\033[0m" >&2; done & - pidB=$! - - wait $pidA - exitCode=$? - - echo -e "\033[0;32m$* finished.\033[0m" >&2 - - kill -9 $pidB - exit $exitCode