the signals and their derived score are provisional and subject to change.
validate manually before sharing.
16089e43221032b88b1c6ecbd0c1b23bb78e2257c326a85cddfb1 month agoCo-Authored-By: Claude Opus 5 <noreply@anthropic.com>---
name: validate-explain-codes
description: >
Validates the bad and good Ada/SPARK code examples in one or more explain
code markdown files (E00NN.md) by running gnatprove --mode=stone against
each snippet in the ec-test project. Can be invoked standalone or called
as a step from the explain-code skill.
license: Apache-2.0
metadata:
version: "0.1.0"
---
# validate-explain-codes
This skill validates the Ada/SPARK code examples embedded in explain code
markdown files (`share/spark/explain_codes/---
name: explain-code
description: >
Use this skill when the user wants to add a new GNATprove explain code for a
SPARK violation. Covers validation, research, drafting the markdown explanation,
user confirmation, and all four code changes needed to wire the new code up.
license: Apache-2.0
metadata:
version: "0.1.0"
---
# Explain Code Skill
This skill adds a new explain code (E00NN) for a `Violation_Kind` in the
spark2014 repository. Explain codes appear in GNATprove error messages as
`[E00NN]` ---
name: test-creator
description: Use this skill when creating new automated tests in this repository. It contains details about test selection, test structure, required setup, and validation steps.
---
# Test Creator
## Purpose
The purpose of this skill is to add a new test in the testsuite/gnatprove/tests subfolder.
## Inputs
The expected test behavior, or tool behavior under test, or code to be covered should be available.
## Workflow
1. Create the test folder under testsuite/gnatprove/tests, se# AGENTS.md
Repository guidance for coding agents working on SPARK 2014.
## Project
- GitLab project: `eng/spark/spark2014`
## Build And Test
Assume the environment is already set up.
- Build and install with `make` and `make install-all`.
- The gnatprove testsuite does not rebuild tools automatically. Re-run `make`
and `make install-all` before testing source changes.
- Format Ada code with `make format`; verify formatting with `make check-format`.
- Run tests from `testsuite/gnatprove/` with `./runone