Bundles Lean+VScodium+mathlib

mk_bundle.py

#!/usr/bin/env python3

from pathlib import Path
import os
import shutil
import stat
import tempfile
import re
import logging
from datetime import datetime

import urllib3
import certifi
from github import Github
from git import Repo

DIST_LIN = Path('linux')/'trylean'
DIST_WIN = Path('windows')/'trylean'
DIST_MAC = Path('macos')/'trylean'
DISTS = [DIST_LIN, DIST_WIN, DIST_MAC]
DIST_ALL = Path('all')
DATA_LIN = DIST_LIN/'vscodium'/'data'
DATA_WIN = DIST_WIN/'vscodium'/'data'
DATA_MAC = DIST_MAC/'vscodium'/'codium-portable-data'

log = logging.getLogger("Make Lean bundle")
log.setLevel(logging.INFO)
if (log.hasHandlers()):
    log.handlers.clear()
log.addHandler(logging.StreamHandler())

# We need to tell python that .vsix files are secretely zip files
shutil.register_unpack_format('VScode extension', ['.vsix'], 
        shutil._unpack_zipfile)

g = Github()
http = urllib3.PoolManager(cert_reqs='CERT_REQUIRED', ca_certs=certifi.where())

def get_asset(project: str, name: str, name_re: str, target: Path):
    """
    Download and unpack asset from a GitHub release.
    project: the GitHub project id, e.g. leanprover-community/lean
    name: Human readable name of the asset, for logging purposes
    name_re: a regex matched against the asset name
    target: a folder Path where the asset will be extracted. It will be
            created if needed.
    """
    log.info(f'Searching for {name}')
    release = g.get_repo(project).get_latest_release()
    asset = next(x for x in release.get_assets() if re.match(name_re, x.name))
    target.mkdir(parents=True, exist_ok=True)
    log.info(f'Downloading {asset.name}')
    with tempfile.TemporaryDirectory() as tmpdirname:
        archive_path = Path(tmpdirname)/asset.name
        with archive_path.open('wb') as f:
            f.write(http.request('GET', asset.browser_download_url).data)
        log.info('Unpacking')
        shutil.unpack_archive(archive_path, target)

def touch_olean(dest: Path):
    """Set access and modification time to now for all olean below dest."""
    now = datetime.now().timestamp()
    for p in dest.glob('**/*.olean'):
        os.utime(str(p), (now, now))

# Get Lean, and rename it to get rid of the version number
#get_asset('leanprover-community/lean', 'Lean for linux', r'lean.*linux.tar.gz', DIST_LIN)
#next(DIST_LIN.glob('lean-*')).replace(DIST_LIN/'lean')
#get_asset('leanprover-community/lean', 'Lean for Windows', r'lean.*windows.zip', DIST_WIN)
#next(DIST_WIN.glob('lean-*')).replace(DIST_WIN/'lean')
#get_asset('leanprover-community/lean', 'Lean for MacOS', r'lean.*darwin.zip', DIST_MAC)
#next(DIST_MAC.glob('lean-*')).replace(DIST_MAC/'lean')

for dest in DISTS:
    touch_olean(dest/'lean'/'lib'/'lean'/'library')

# Get VScodium, the open source version of VScode *binaries*
get_asset('VSCodium/vscodium', 'VScodium for Linux', r'VSCodium-linux-x64.*.tar.gz', 
          DIST_LIN/'vscodium')
get_asset('VSCodium/vscodium', 'VScodium for Windows', r'VSCodium-win32-x64.*.zip', 
          DIST_WIN/'vscodium')
get_asset('VSCodium/vscodium', 'VScodium for MacOS', r'VSCodium-darwin.*.zip', 
          DIST_MAC/'vscodium')

# Get the Lean extension, and move it to the right place
lean_extension_path = DIST_ALL/'extension'
get_asset('leanprover/vscode-lean', 'Lean extension', r'.*.vsix', 
          lean_extension_path)
for dest in [DATA_LIN, DATA_WIN, DATA_MAC]:
    shutil.copytree(lean_extension_path/'extension', dest/'extensions'/'lean')


# Write relevant VScode settings
SETTINGS = """{
    "files.exclude": {
        "**/.git": true,
        "**/.svn": true,
        "**/.hg": true,
        "**/CVS": true,
        "**/.DS_Store": true,
        "**/*.olean": true
    },
    "lean.executablePath": "%extensionPath%/../../../../lean/bin/lean"
    "editor.minimap.enabled": false,
    "window.titleBarStyle": "custom",
}
"""
for dest in [DATA_LIN, DATA_WIN, DATA_MAC]:
    user = dest/'user-data'/'User'
    user.mkdir(parents=True, exist_ok=True)
    with (user/'settings.json').open('w') as settings:
        settings.write(SETTINGS)

# Get mathlib
(DIST_ALL/'mathlib').mkdir(exist_ok=True)
get_asset('leanprover-community/mathlib-nightly', 'Mathlib', r'mathlib-olean-nightly-.*.tar.gz',
        DIST_ALL/'mathlib')
for dest in DISTS:
    shutil.copytree(DIST_ALL/'mathlib', dest/'mathlib')
    touch_olean(dest/'mathlib')

# Get some file to play with
log.info('Getting tutorial files')
with tempfile.TemporaryDirectory() as tmpdirname:
    Repo.clone_from('https://github.com/leanprover-community/tutorials.git', tmpdirname)
    for dest in DISTS:
        (dest/'src').mkdir(exist_ok=True)
        for f in (Path(tmpdirname)/'src').glob('*.lean'):
                shutil.copy(f, dest/'src'/f.name)

# Setup leanpk.path
log.info('Setting up leanpkg.path')
LEANPKG_PATH = """builtin_path
path ../mathlib/src/
"""
for dest in DISTS:
    with (dest/'src'/'leanpkg.path').open('w') as path:
        path.write(LEANPKG_PATH)

# Create Launcher
BASH_SCRIPT = """#!/bin/bash
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
cd $DIR
./vscodium/codium $DIR/src
"""
with (DIST_LIN/'trylean').open('w') as path:
    path.write(BASH_SCRIPT)
(DIST_LIN/'trylean').chmod(stat.S_IXUSR | stat.S_IRUSR | stat.S_IWUSR)
MAC_BASH_SCRIPT = """#!/bin/bash
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
cd $DIR
open ./vscodium/VSCodium.app --args $DIR/src
"""
with (DIST_MAC/'trylean').open('w') as path:
    path.write(MAC_BASH_SCRIPT)
(DIST_MAC/'trylean').chmod(stat.S_IXUSR | stat.S_IRUSR | stat.S_IWUSR)

BAT_SCRIPT = r""".\vscodium\VSCodium src
"""
with (DIST_WIN/'trylean.bat').open('w') as path:
    path.write(BAT_SCRIPT)

# Zip all
log.info('Making Linux archive')
shutil.make_archive('trylean_linux', 'gztar', root_dir='linux', base_dir='trylean')
log.info('Making Windows archive')
shutil.make_archive('trylean_windows', 'zip', root_dir='windows', base_dir='trylean')
log.info('Making MacOS archive')
shutil.make_archive('trylean_darwin', 'zip', root_dir='macos', base_dir='trylean')