Skip to content

Commit

Permalink
Run the shell script in an entirely separate directory tree.
Browse files Browse the repository at this point in the history
  • Loading branch information
Julian committed Feb 7, 2021
1 parent 5379c1f commit fcc3591
Showing 1 changed file with 27 additions and 11 deletions.
38 changes: 27 additions & 11 deletions scripts/lint_style_sanity_test.py
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
#!/usr/bin/env python3
from pathlib import Path
from tempfile import NamedTemporaryFile
from shutil import copy
from tempfile import NamedTemporaryFile, TemporaryDirectory
from textwrap import dedent
import subprocess
import unittest

Expand Down Expand Up @@ -148,19 +150,33 @@ def test_running_the_shell_script_does_not_error(self):
Running it exits with successful return code.
This test will not run if there are current style warnings.
This test will execute in a separate directory tree to make sure
it doesn't fail if there are current style warnings.
"""

src = list(ROOT_DIR.glob("src/**/*.lean"))
archive = list(ROOT_DIR.glob("archive/**/*.lean"))
if subprocess.run(
["./scripts/lint-style.py"] + src + archive,
stdout=subprocess.DEVNULL,
cwd=ROOT_DIR,
).returncode:
self.skipTest("Skipping... there are unfixed style warnings.")
with TemporaryDirectory() as tmpdir:
root = Path(tmpdir)
for each in "scripts", "src", "archive":
root.joinpath(each).mkdir()

copy(SCRIPTS_DIR / "lint-style.sh", root / "scripts")
copy(SCRIPTS_DIR / "lint-style.py", root / "scripts")

# Give us at least one file to check
root.joinpath("src", "unittesting123.lean").write_text(
dedent(
"""\
/-
Copyright (c) 2021 Someone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Someone
-/
example : 37 = 37 := rfl
""",
)
)

subprocess.run(["./scripts/lint-style.sh"], check=True, cwd=ROOT_DIR)
subprocess.run(["./scripts/lint-style.sh"], check=True, cwd=root)


if __name__ == "__main__":
Expand Down

0 comments on commit fcc3591

Please sign in to comment.