crawl.py

from leancrawler import LeanLibModel, create_db, Path
import os

pkgname = 'mathlib'
pkgpath = '/Users/chb/Documents/lean/'+pkgname

# uncomment this and edit for a package with dependencies
# os.environ['LEAN_PATH']="/Users/chb/Documents/lean/leancrawler/src/leancrawler/:"+pkgpath+"/src:"+pkgpath+"/_target/deps/mathlib:/Users/chb/.elan/toolchains/3.4.2/lib/lean/library/"
# use this for a package with no dependencies
os.environ['LEAN_PATH']="/Users/chb/Documents/lean/leancrawler/src/leancrawler/:"+pkgpath+"/src:/Users/chb/.elan/toolchains/3.4.2/lib/lean/library/"

# print(os.environ['LEAN_PATH'])

create_db(pkgname+'.db')
LeanLibModel.from_path(pkgname, Path(pkgpath+'/src'))