michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(bin/lmake): save .olean file when makefile doesn't exist

Browse source
This commit is contained in:
Soonho Kong 2014-08-17 17:30:43 -07:00
parent 9fae5ae525
commit 72aadd1afa
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
bin/lmake
View file

@ -98,9 +98,11 @@ def find_lean_opt():
def call_lean(leanfile, options):
""" Call lean with options """
from collections import OrderedDict
oleanfile = leanfile[:-5] + ".olean"
lean_exe = find_lean_exe()
lean_opt = list(OrderedDict.fromkeys(find_lean_opt() + options))
subprocess.call([lean_exe] + lean_opt + [leanfile], stderr=subprocess.STDOUT)
cmd = [lean_exe] + lean_opt + [leanfile] + ["-o", oleanfile]
subprocess.call(cmd, stderr=subprocess.STDOUT)
def get_lean(s):
""" Given a string s, return corresponding .lean file if exists """