Skip to content

Bring CONTRIBUTING and the CLI reference in line with main #149

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Deicyde merged 2 commits into from
Oct 6, 2026
Merged

Bring CONTRIBUTING and the CLI reference in line with main #149

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9430ddd
Bring the contributor and CLI docs in line with main
Deicyde Oct 5, 2026
e565b24
Describe the CI jobs, Lean test skips, and line length accurately
Deicyde Oct 5, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 29 additions & 5 deletions CONTRIBUTING.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,27 @@ We want to make contributing to this project as easy and transparent as
possible.

## Our Development Process
... (in particular how this is synced with internal changes to the project)
Development happens in this repository: changes reach `main` through pull
requests. You need Python 3.10 or newer, [`uv`](https://docs.astral.sh/uv/),
Git, and Make. From a clone:

```bash
make setup # uv sync --extra dev --extra repl
make lint # uv run ruff check autoform_cli servers tests
make test # uv run pytest -q
make check-example # validate, render, and build the bundled example site
```

CI (`.github/workflows/tests.yml`) runs the same four steps on Python 3.10 and
3.13 for every push and pull request. A separate job runs
`tests/test_skeleton.py` and one `tests/test_project_inspect.py` test against a
real Lean toolchain; another runs the inspection, bounded-subprocess, and
transactional-output tests on Windows. Locally, tests that need Lean skip when
`lake` is not on `PATH`. The `tests/test_skeleton.py` ones also skip when the
toolchain pinned in `tests/fixtures/skeleton-project/lean-toolchain` is
missing; the others let elan download it. Run `lake build` in
`skills/setup/assets/cabannes-thesis-project` when you change the example's
Lean sources or declarations.

## Pull Requests
We actively welcome your pull requests.
Expand All @@ -30,10 +50,14 @@ disclosure of security bugs. In those cases, please go through the process
outlined on that page and do not file a public issue.

## Coding Style
* 2 spaces for indentation rather than tabs
* 80 character line length
* ...
* Python uses 4-space indentation and a 120-character line length
(`[tool.ruff]` in `pyproject.toml`). Ruff's default rules do not check line
length, and a few existing lines run longer.
* `make lint` runs `ruff check` with ruff's default rules on `autoform_cli`,
`servers`, and `tests`; CI runs the same check.
* CI runs no formatter, so match the surrounding code instead of reformatting
unrelated lines.

## License
By contributing to __________, you agree that your contributions will be licensed
By contributing to autoform-bot, you agree that your contributions will be licensed
under the LICENSE file in the root directory of this source tree.
13 changes: 6 additions & 7 deletions autoform_cli/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -114,9 +114,10 @@ This section is the single source of truth for the command line. Skills
describe what to achieve and link here; they do not restate flags, so a change
to the CLI lands in one place.

The commands below are written as they appear on `PATH`. Inside a consumer
project the plugin is not installed, so resolve `<AUTOFORM_PLUGIN_ROOT>` from
the loaded plugin and prefix each one, running from the project root:
The commands below are written as they appear on `PATH` once this Python
package is installed. Inside a consumer project the package is not installed,
so resolve `<AUTOFORM_PLUGIN_ROOT>` from the loaded plugin and prefix each one,
running from the project root:

```bash
uv run --project "<AUTOFORM_PLUGIN_ROOT>" autoform check blueprint --lean-root .
Expand Down Expand Up @@ -680,9 +681,7 @@ worktree each and serialize `lake build` behind a `lake-build` claim, because
builds share the elan toolchain and the Mathlib cache even when the checkouts
are separate.

Claims are temporary operational state, never article frontmatter. Future
Deicyde workers may share this protocol, but their current continue-uncoordinated
failure behavior must be removed before they use the canonical claim API.
Claims are temporary operational state, never article frontmatter.

## Local runtime doctor

Expand All @@ -706,7 +705,7 @@ This command is strictly read-only and local. It does not invoke Git, GitHub,
subprocesses, network services, claims, queues, reviews, recovery state,
providers, workers, renderers, or dashboards, and it creates no cache, scratch
repository, service, state directory, or `graph.json`. It is a project/runtime
doctor, separate from any future Deicyde fleet or machine-capability preflight.
doctor, separate from any future worker fleet or machine-capability preflight.

## Runtime contract

Expand Down
Loading