Skip to content

Commit

Permalink
fix: make fix-lints.py work on windows (leanprover-community#5055)
Browse files Browse the repository at this point in the history
The `encoding='utf8'` fixes the crashes, the `with` statements are better WRT lifetime management of files.



Co-authored-by: Chris Hughes <[email protected]>
  • Loading branch information
eric-wieser and ChrisHughes24 committed Jun 21, 2023
1 parent c9f26d2 commit aeb2e01
Showing 1 changed file with 6 additions and 4 deletions.
10 changes: 6 additions & 4 deletions scripts/fix-lints.py
Original file line number Diff line number Diff line change
Expand Up @@ -19,16 +19,17 @@ def getpos(line):
# try to build
log = subprocess.run(
['lake', 'build', leanmodule],
capture_output=True)
capture_output=True, encoding='utf8')
if log.returncode == 0:
print("no errors 🎉")
exit(0)

shutil.copyfile(leanfile, leanfile + '.bak')

with open(leanfile + '.bak', encoding='utf8') as fp:
f = list(fp)
count = 0
f = list(open(leanfile + '.bak'))
for l in reversed(log.stderr.decode().splitlines()):
for l in reversed(log.stderr.splitlines()):
if 'linter.unusedVariables' in l:
line, col = getpos(l)
f[line-1] = f[line-1][0:col] + '_' + f[line-1][col:]
Expand All @@ -42,5 +43,6 @@ def getpos(line):

print(f'Fixed {count} warnings', file=sys.stderr)

open(leanfile, 'w').write(''.join(f))
with open(leanfile, 'w', encoding='utf8') as fp:
fp.write(''.join(f))
os.remove(leanfile + '.bak')

0 comments on commit aeb2e01

Please sign in to comment.