eventb-rossi/rossi-action
GitHub: eventb-rossi/rossi-action
在 GitHub Actions CI 中对 Event-B 形式化模型执行验证、格式检查与静态构建，并以行内注释和 SARIF 报告形式呈现发现结果的 GitHub Action。
Stars: 0 | Forks: 0
# Rossi Event-B Validator — GitHub Action
在 CI 中使用 [rossi](https://github.com/eventb-rossi/rossi) 检查 Event-B 模型：
安装经过验证的二进制文件，在你的模型上运行 `validate` / `fmt --check` / `build`，
将每一项发现内联标注出来，并可选择将一次 SARIF 运行上传至
code scanning。
```
- uses: eventb-rossi/rossi-action@v1
with:
path: models/
```
这会安装最新的 rossi 发行版，验证 `models/`，将每一项
发现标注在相应的出错的行上，并在出现任何错误时使步骤失败。
## 用法
### 同时对建议性 lint 进行拦截
建议性 lint（`EB011` 死变量，`EB012` 未修改的变量，
`EB014` 未完成初始化，`EB023` 被遮蔽的名称）是警告，默认情况下
不会导致运行失败：
```
- uses: eventb-rossi/rossi-action@v1
with:
path: models/
deny-warnings: "true"
```
### 将发现结果上传至 code scanning
```
permissions:
contents: read
security-events: write
steps:
- uses: actions/checkout@v7
- uses: eventb-rossi/rossi-action@v1
with:
path: models/
sarif: "true"
upload-sarif: "true"
category: rossi
```
无论接收到多少文件、目录和压缩包，rossi 都会生成**完全一致的一次 SARIF 运行**，这正是
[code scanning 所要求的][sarif-runs] —— 运行共享同一类别的上传会被
拒绝。如果你从同一个代码库上传了不止一份分析报告，请为
每一份指定独立的 `category`。
`sarif` 是由 validate 验证过程生成的，因此 `commands` 必须包含 `validate`。
在未包含此项的情况下请求报告会导致错误，而不是在 Security 标签页中留下
一个静默的空状态。
对于来自（**from**）fork 的拉取请求，上传操作会被跳过，因为它们无法被授予
`security-events: write` 权限；但在这种情况下，发现结果仍会以注释的形式显示。
### 同时检查格式化与静态构建
```
- uses: eventb-rossi/rossi-action@v1
with:
path: models/
commands: validate,fmt-check,build
```
`build` 的执行单元是一个**项目 (project)**：将其指向某个项目目录或 `.zip` 文件，
而不是一组散碎的组件，否则每一个跨组件的引用都会失效。该
action 会拒绝这种拆分方式，而不会将原本正确的模型报告为损坏。
对于项目目录或 `.zip` 文件，`validate` 已经运行了与
`build` 相同的语义检查，并会附带规则 ID 和位置进行报告，而 `build` 仅输出纯文本——因此在那里添加 `build` 多半只是在对相同的
模型进行第二次检查。`build` 的真正价值在于处理**松散的** `.eventb` 文件：`validate`
没有可以用来解析它的项目，因此会跳过这些检查，所以未解析的
`SEES` 仅会由 `build` 报告。
### 收集发现结果而不使任务失败
```
- uses: eventb-rossi/rossi-action@v1
id: rossi
with:
path: models/
fail-on-error: "false"
- run: echo "${{ steps.rossi.outputs.error-count }} errors"
```
## 输入
| 输入 | 默认值 | 描述 |
|---|---|---|
| `path` | `.` | 要检查的模型：文件、解压后的项目目录，或 Rodin `.zip` 压缩包。以空格分隔；支持扩展 glob。 |
| `version` | latest | 要安装的 rossi 版本，不包含前缀 `v`。 |
| `rossi-path` | – | 使用现有的二进制文件，而不是下载。相对路径会基于工作区根目录进行解析，因此搭配 `working-directory` 使用时也能正常工作。 |
| `commands` | `validate` | 以逗号分隔：`validate`、`fmt-check`、`build`。`build` 需要指向项目根目录。 |
| `deny-warnings` | `false` | 遇到建议性 lint 和错误时均判定为失败。 |
| `annotations` | `true` | 输出内联的 `::error` / `::warning` 注释。 |
| `sarif` | `false` | 生成 SARIF 报告。要求 `commands` 中包含 `validate`。 |
| `sarif-file` | `rossi.sarif` | 报告的写入位置。 |
| `category` | `rossi` | SARIF 运行的分析类别。 |
| `upload-sarif` | `false` | 将报告上传至 code scanning。 |
| `working-directory` | `.` | 运行 rossi 的目录；`path` 相对于此目录。 |
| `fail-on-error` | `true` | 发现问题时使步骤失败，包括“在 `path` 下未找到 Event-B 组件”。 |
## 输出
| 输出 | 描述 |
|---|---|
| `valid` | 当 rossi 未报告任何失败时为 `"true"`。 |
| `error-count` | 错误严重级别的发现数量。 |
| `warning-count` | 建议性发现结果的数量。 |
| `sarif-file` | SARIF 报告的路径，当 `sarif` 关闭时为空。 |
| `rossi-version` | 实际运行的 rossi 版本。 |
## 版本的选择方式
该 action 会安装最新的 rossi 发行版，并会根据该发行版的
`SHA256SUMS` 进行校验；如果某个发行版没有校验清单，将会被拒绝安装，
而不是在未经验证的情况下安装。设置 `version:` 则可以安装指定的具体版本。
## 环境要求
`bash`、`curl` 和 `jq` —— 在 Linux、macOS 和 Windows 的 GitHub 托管的
runner 上均已预装。在这三种操作系统上均提供了适用于 x86-64 和 arm64 架构的预编译二进制文件。
## 许可证
采用 [Apache 2.0](LICENSE-APACHE) 和 [MIT](LICENSE-MIT) 双重许可，与
rossi 相同。
标签：Event-B, GitHub Action, 应用安全, 形式化验证, 静态检查