Core

Provide the shared leaves of veriphy: its named exceptions, the protocol's type vocabulary, the project layout.

CertificateError

Bases: VeriphyError

Signal that no certificate exists or that a supplied certificate is malformed.

EncodingError

Bases: VeriphyError

Signal a method result that has no exact JSON encoding.

MethodError

Bases: VeriphyError

Signal a failed daemon method, with a message of the form <method>: <reason>.

ParamError(param, reason)

Bases: VeriphyError

Signal a request parameter that failed validation.

Parameters:

Name	Type	Description	Default
param	str	The name of the parameter.	required
reason	str	What is wrong with the parameter.	required

Source code in src/veriphy/core/_errors.py

def __init__(self, param: str, reason: str) -> None:
    message = f"parameter '{param}': {reason}"
    super().__init__(message)
    self.param = param
    self.reason = reason

ScriptError(reason, stdout)

Bases: VeriphyError

Signal a Sage script that failed, carrying the output it printed before failing.

Parameters:

Name	Type	Description	Default
reason	str	Why the script failed.	required
stdout	str	The output the script printed, possibly empty.	required

Source code in src/veriphy/core/_errors.py

def __init__(self, reason: str, stdout: str) -> None:
    message = reason + (f'\n--- script stdout ---\n{stdout}' if stdout else '')
    super().__init__(message)
    self.reason = reason
    self.stdout = stdout

TableError(source, field, reason)

Bases: VeriphyError

Signal a translation-table file that does not follow the schema.

Parameters:

Name	Type	Description	Default
source	str	The file the table came from.	required
field	str	The field at fault.	required
reason	str	What is wrong with it.	required

Source code in src/veriphy/core/_errors.py

def __init__(self, source: str, field: str, reason: str) -> None:
    message = (
        f"{source}: {reason} '{field}'" if reason == 'missing field' else f"{source}: field '{field}' {reason}"
    )
    super().__init__(message)
    self.source = source
    self.field = field
    self.reason = reason

VeriphyError

Bases: Exception

Signal a failure inside veriphy.

find_workspace_root(start=None)

Return the Lean workspace root: the nearest directory, from start upwards, that holds a lakefile.

Parameters:

Name	Type	Description	Default
start	Path | None	The directory to search from, the working directory when None.	None

Returns:

Type	Description
Path	The workspace root, or start itself when no ancestor holds a lakefile.

Examples:

>>> import tempfile
>>> with tempfile.TemporaryDirectory() as tmp:
...     root = Path(tmp).resolve()
...     _ = (root / 'lakefile.toml').write_text('')
...     (root / 'Sub' / 'Dir').mkdir(parents=True)
...     find_workspace_root(root / 'Sub' / 'Dir') == root
True

Source code in src/veriphy/core/_project.py

def find_workspace_root(start: Path | None = None) -> Path:
    """Return the Lean workspace root: the nearest directory, from `start` upwards, that holds a lakefile.

    Args:
        start: The directory to search from, the working directory when `None`.

    Returns:
        The workspace root, or `start` itself when no ancestor holds a lakefile.

    Examples:
        >>> import tempfile
        >>> with tempfile.TemporaryDirectory() as tmp:
        ...     root = Path(tmp).resolve()
        ...     _ = (root / 'lakefile.toml').write_text('')
        ...     (root / 'Sub' / 'Dir').mkdir(parents=True)
        ...     find_workspace_root(root / 'Sub' / 'Dir') == root
        True
    """
    origin = (start or Path.cwd()).resolve()
    for directory in (origin, *origin.parents):
        if any((directory / name).is_file() for name in LAKEFILES):
            return directory
    return origin

project_dir(root=None)

Return the project's .veriphy/ directory, without creating it.

Parameters:

Name	Type	Description	Default
root	Path | None	The workspace root, found from the working directory when None.	None

Returns:

Type	Description
Path	The path of .veriphy/ under the workspace root.

Examples:

>>> project_dir(Path('/work/project')).as_posix()
'/work/project/.veriphy'

Source code in src/veriphy/core/_project.py

def project_dir(root: Path | None = None) -> Path:
    """Return the project's `.veriphy/` directory, without creating it.

    Args:
        root: The workspace root, found from the working directory when `None`.

    Returns:
        The path of `.veriphy/` under the workspace root.

    Examples:
        >>> project_dir(Path('/work/project')).as_posix()
        '/work/project/.veriphy'
    """
    return (root if root is not None else find_workspace_root()) / PROJECT_DIR_NAME