INNER CODE UNIT · Python

_command

lean-dojo/TorchLean · torchlean/__init__.py:28

def _command(checker: str | Path | Sequence[str] | None) -> list[str]:
    if isinstance(checker, (str, Path)):
        return [str(checker), "ir"]
    if checker is not None:
        if (not isinstance(checker, Sequence) or not checker
                or not all(isinstance(argument, str) for argument in checker)):
            raise TypeError("checker must be a path or a nonempty sequence of command arguments")
        return list(checker)
    path = os.environ.get("TORCHLEAN_VERIFY")
    if path:
        return [path, "ir"]
    executable = Path(__file__).resolve().parent.parent / ".lake/build/bin/verify"
    if not executable.is_file():
        raise FileNotFoundError(
            "Build the TorchLean `verify` executable first, or supply checker= with "
            "a command ending in `verify ir`. Verification does not start a build implicitly."
        )
    return [str(executable), "ir"]

View source record →