Debian package builder for Lean

tasks.py

import tempfile
from pathlib import Path
from invoke import task

LEAN_CONTROL="""Package: lean
Version: {}
Section: math
Priority: optional
Architecture: amd64
Depends: git (>= 1.2)
Maintainer: Patrick Massot <patrick.massot@u-psud.fr>
Description: Lean theorem prover
 The Lean theorem prover.
"""

MATHLIB_CONTROL="""Package: lean-mathlib
Version: {}
Section: math
Priority: optional
Architecture: amd64
Depends: git (>= 1.2)
Maintainer: Patrick Massot <patrick.massot@u-psud.fr>
Description: Mathlib
 The standard mathematics library for the Lean theorem prover.
 commit {}
"""

@task
def lean(c, lean_version='3.4.2', package_version='1'):
    package_version = lean_version + '-' + package_version
    with tempfile.TemporaryDirectory() as tmpdirname:
        with c.cd(tmpdirname):
            c.run('wget https://github.com/leanprover/lean/releases/download/v'+lean_version+'/lean-'+lean_version+'-linux.tar.gz')
            c.run('tar xf lean-'+lean_version+'-linux.tar.gz')
            base_path = Path(tmpdirname)
            src_path = base_path / ('lean-'+lean_version+'-linux')
            pkg_path = base_path / ('lean_'+package_version)
            deb_path = pkg_path / 'DEBIAN'
            deb_path.mkdir(parents=True)
            
            with (deb_path / 'control').open('w') as control:
                control.write(LEAN_CONTROL.format(package_version))
            
            (pkg_path / 'usr' / 'bin').mkdir(parents=True)
            c.run('mv '+ str(src_path / 'bin')+'/* ' + str(pkg_path / 'usr' / 'bin'))
            
            (pkg_path / 'usr' / 'lib').mkdir(parents=True)
            c.run('mv '+ str(src_path / 'lib')+'/* ' + str(pkg_path / 'usr' / 'lib'))

            c.run('fakeroot dpkg-deb --build lean_'+package_version)
        (base_path / ('lean_'+package_version + '.deb')).rename('lean_'+package_version + '.deb')


@task
def mathlib(c, lean_version='3.4.2', package_version='1'):
    package_version = lean_version + '-' + package_version
    with tempfile.TemporaryDirectory() as tmpdirname:
        with c.cd(tmpdirname):
            c.run('wget https://github.com/leanprover/lean/releases/download/v'+lean_version+'/lean-'+lean_version+'-linux.tar.gz')
            c.run('tar xf lean-'+lean_version+'-linux.tar.gz')
            base_path = Path(tmpdirname)
            leanpkg_path = base_path / ('lean-'+lean_version+'-linux/bin/leanpkg')
            src_path = base_path / 'mathlib'
            pkg_path = base_path / ('lean-mathlib_'+package_version)
            deb_path = pkg_path / 'DEBIAN'
            deb_path.mkdir(parents=True)
            
            c.run('git clone https://github.com/leanprover/mathlib.git')
            with (src_path / '.git/refs/heads/master').open('r') as f:
                commit = f.read()

            with (deb_path / 'control').open('w') as control:
                control.write(MATHLIB_CONTROL.format(package_version, commit))
            
            with c.cd(str(src_path)):
                c.run(str(leanpkg_path) + ' build')

            (pkg_path / 'usr/lib/lean-mathlib').mkdir(parents=True)
            c.run('mv '+ str(src_path)+'/leanpkg.* ' + str(pkg_path / 'usr/lib/lean-mathlib'))
            c.run('mv '+ str(src_path / 'src')+'* ' + str(pkg_path / 'usr/lib/lean-mathlib'))
            
            c.run('fakeroot dpkg-deb --build lean-mathlib_'+package_version)
        (base_path / ('lean-mathlib_'+package_version + '.deb')).rename('lean-mathlib_'+package_version + '.deb')