-
-
Save PatrickMassot/567833153f106379b87a20e9d3a712ef to your computer and use it in GitHub Desktop.
Bundles Lean+VScodium+mathlib
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/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') |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment