What is cmd = 'find ./data -type f -exec sed -i \'\' \'s/TAPAS_ROOT_ABSOLUTE_PATH/%s/g\' {} +' % cwd.replace(os.path.sep, '\/') for?

[brando90]

I want to help improve the CoqGym library (to help centralize the efforts to make ML for Coq) and I was trying to install (and slightly modify) the unzip_data.py but at the end I came across this command that looked rather cryptic:

print('setting the absolute paths..')
cwd = os.getcwd()
if platform.system() == 'Darwin':
    cmd = 'find ./data -type f -exec sed -i \'\' \'s/TAPAS_ROOT_ABSOLUTE_PATH/%s/g\' {} +' % cwd.replace(os.path.sep, '\/')
else:
    cmd = 'find ./data -type f -exec sed -i \'s/TAPAS_ROOT_ABSOLUTE_PATH/%s/g\' {} +' % cwd.replace(os.path.sep, '\/')
execute(cmd)
print('The CoqGym dataset is ready!')

what is it suppose to be doing? I know the print statement says setting absolute paths but what does that mean? Paths are set automatically wherever one places a file/folder. Can this perhaps be replaced by a os.walk? (Also, running unix commands in python is very uncommon, especially since they pose security threats for example).

Anyway, let me know how I can help to make this better! :) Making this easier can make a wider adoption of the CoqGym data set as the standard (since its easy to use!)

I can paste my current attempt to make that file more flexible so people can place the data wherever they want (especially outside the repo where git might try to track it accidentally):

"""
create coqgym data set.

Would be nice to make all the code in either python or bash but not mix it like it's done here.
Also using pathlib as much as possible.
"""
import os
import platform
import sys
from hashlib import md5
import pdb

from pathlib import Path


def execute(cmd):
    print(cmd)
    assert os.system(cmd) == 0


def check_md5(filename, gt_hashcode):
    print('checking %s..' % filename)
    if not os.path.exists(filename):
        print(filename, 'not exists')
        print('aborting..')
        sys.exit(-1)
    hashcode = md5(open(filename, 'rb').read()).hexdigest() 
    if hashcode != gt_hashcode:
        print(filename, 'has the wrong MD5 hashcode')
        print('expect %s but found %s' % (gt_hashcode, hashcode))
        print('aborting..')
        sys.exit(-1)
    return


def unzip(filename):
    filename = str(filename)
    if os.path.exists(filename[:-7]):
        remove = input(filename[:-7] + ' already exists. Do you want to remove it? (y/N)').lower()
        if remove == 'y':
            execute('rm -r ' + filename[:-7])
        else:
            print('aborting..')
            sys.exit(-1)
 
    execute('tar -xvzf ' + str(filename))


def do_mdb_load(original_code=False):
    """

    command:
        mdb_load [-V] [-f file] [-n] [-s subdb] [-N] [-T]  envpath
    description:
        The mdb_load utility reads from the standard input and loads it into the LMDB environment envpath.
    Kaiyu's example:
        execute('mdb_load -f sexp_cache.lmdb sexp_cache')
    """
    if original_code:
        execute('mdb_load -f sexp_cache.lmdb sexp_cache')
        os.remove('sexp_cache.lmdb')
    else:
        sexp_cache_lmdb = Path('~/data/coqgym/sexp_cache.lmdb').expanduser()
        sexp_cache = Path('~/data/coqgym/sexp_cache').expanduser()
        execute(f'mdb_load -f {sexp_cache_lmdb} {sexp_cache}')
        os.remove(sexp_cache_lmdb)

def main():
    projs_split = Path('~/data/coqgym/projs_split.json').expanduser()
    data = Path('~/data/coqgym/data.tar.gz').expanduser()
    sexp_cache = Path('~/data/coqgym/sexp_cache.tar.gz').expanduser()

    # check data integrity
    # check_md5(projs_split, '39eac2315532040f370ca4996862ef75')
    # check_md5(data, '922937155a199605eb8067ccfbbdb81a')
    # check_md5(sexp_cache, '2e8ff40a7dd0b6d0efc74480dd3dfc8d')

    # unzip
    print('unziping...')
    unzip(data)
    unzip(sexp_cache)
    print('done unziping')

    # create sexp
    print('doing the sexp...')
    sexp_cache_dir = Path('~/data/coqgym/sexp_cache').expanduser()
    sexp_cache_dir.mkdir(parents=True, exist_ok=True)
    do_mdb_load()
    print('done doing the sexps...')

    print('setting the absolute paths...')
    cwd = os.getcwd()
    if platform.system() == 'Darwin':
        cmd = 'find ./data -type f -exec sed -i \'\' \'s/TAPAS_ROOT_ABSOLUTE_PATH/%s/g\' {} +' % cwd.replace(os.path.sep, '\/')
    else:
        cmd = 'find ./data -type f -exec sed -i \'s/TAPAS_ROOT_ABSOLUTE_PATH/%s/g\' {} +' % cwd.replace(os.path.sep, '\/')
    execute(cmd)


if __name__ == '__main__':
    main()
    print('The CoqGym dataset is ready!')

[yangky11]

The proofs extracted from Coq projects contain hard-coded paths to the current directory. In the pre-extracted proofs, I replaced the path with TAPAS_ROOT_ABSOLUTE_PATH. So unzip_data.py restores it using the user's current path.

Indeed, the current codebase for CoqGym still has a lot of room to improve its accessibility. But unfortunately, I don't have enough bandwidth to do a major overhaul. You're welcome to submit pull requests though. Also feel free to post in Discussions so that I may take a look whenever I get a chance. I just reformatted all Python code using black and added a comment about contributing in the README file.