Metadata-Version: 2.4
Name: metamath-prelude
Version: 0.0.2
Summary: Prelude definitions for Metamath projects
Author-email: Mingli Yuan <mingli.yuan@gmail.com>
Maintainer-email: Mingli Yuan <mingli.yuan@gmail.com>
License-Expression: GPL-2.0-or-later
Project-URL: Homepage, https://github.com/epistemic-frontier/metamath-prelude
Project-URL: Repository, https://github.com/epistemic-frontier/metamath-prelude
Project-URL: Issues, https://github.com/epistemic-frontier/metamath-prelude/issues
Keywords: metamath,proof,proof-scaffold
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: Programming Language :: Python
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3 :: Only
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Programming Language :: Python :: 3.14
Classifier: Topic :: Software Development :: Build Tools
Requires-Python: >=3.10
Description-Content-Type: text/markdown
Requires-Dist: proof-scaffold==0.0.5

# metamath-prelude

`metamath-prelude` is a small Python package that exports the “prelude” layer used by ProofScaffold-based Metamath projects.
It provides the core constants, variables, and a minimal set of foundational statements that downstream packages can depend on and link against.

## Versioning

- Package version: `0.0.2`
- ProofScaffold dependency: `proof-scaffold==0.0.5`

## Installation

This package is published on PyPI: https://pypi.org/project/metamath-prelude/

With `uv`:

```bash
uv add metamath-prelude
```

## What this package contains

- A ProofScaffold `build.py` entrypoint that emits the prelude statements as a linkable unit.
- Authoring helpers for the Hilbert-style propositional fragment (rule bundle used by downstream proof scripts).
- A documented alignment with the early part of `set.mm`.

## Verification

This repository uses `uv` for reproducible installs and runs `skfd verify --level 1` as the primary correctness gate.

From the `metamath-prelude/` directory:

```bash
uv sync --locked --dev
uv run --frozen ruff check .
uv run --frozen mypy .
uv run --frozen python -m pytest
uv run --frozen skfd verify --level 1 metamath-prelude
```

`skfd verify` builds the package into a verification monolith (under `target/`) and checks it with the configured verifiers.

## set.mm alignment

- Milestone boundary (within the first ~700 lines): prelude = `set.mm` lines 1–648; propositional logic starts at line 649 (the `ax-mp` block).
- Mapping notes and migrated comments: [`docs/SETMM_PRELUDE_1_648.md`](docs/SETMM_PRELUDE_1_648.md)
