#!/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')
