公开记录中等
软件健康报告模式 0.27.0 · 指标 2.3.1 · 2026-07-27 23:55 UTC
rocq-community / fourcolor
Formal proof of the Four Color Theorem [maintainer=@ybertot]
rocq-community/fourcolor 的健康指数为 100 分中的 53 分，处于「中等」区间。 其得分最高的类别是Sustainability & Governance（76/100），最低的是AI Readiness（22/100）。 最近一次更新在 10 天前。 近期的大部分工作由 3 位贡献者完成。
53
总分 / 100软件健康指数
指标归入加权类别，统一采用 1–100 量表。总体分先取类别加权平均，再依据公开记录的分布进行校准，使各等级具有百分位含义；当公开证据触发高风险司法辖区政策时，评级会按政策调整，并设置 34（存在风险）的上限。
53
卓越93-100公开记录中的最高层级（约前 5%）；基本满足所有检验标准
优秀80-92各方面均表现强劲；仅有少量不足
良好65-79健康；不足之处有限且可控
中等50-64可接受，但存在明显不足；建议进行审查
薄弱35-49多个领域存在实质性薄弱环节
存在风险20-34存在重大薄弱环节；采用时应保持审慎
危急1-19问题严重（项目被弃置、仅有单一维护者、缺乏基本工程规范）
评分画像
每条轴代表一个类别。形状比平均值更重要——健康的对象会填满整个图形，而“一峰一谷”式画像意味着某一维度的优势正掩盖另一维度的风险。
加权总体分 52 经校准后在公布的指数量表上为 53（记录校准 2026-08-02）。
所有权
按类别列示的指标
活力
项目是否仍有生命——是否仍在编写代码，是否仍在发布版本？
56
开发活跃度
37薄弱
评分方式
| 28.8/36 | 推送新近度 — 最近一次推送于 10 天前 |
| 2.1/36 | 提交节奏 — 52 周中有 3 周有提交 |
| 6.3/18 | 提交量 — 最近一年 4 次提交 |
| 0/10 | OpenSSF Scorecard：Maintained — 0 commit(s) and 0 issue activity found in the last 90 days -- score normalized to 0 |
所用输入
| commits_last_year | 4 |
| human_commit_share | 1 |
| days_since_last_push | 10 |
| active_weeks_last_year | 3 |
发布纪律
84优秀
评分方式
| 27/27 | 有发布版本 — 已发布 12 个发布版本 |
| 36/36 | 发布时效 — 最近一次发布版本于 10 天前 |
| 12.6/27 | 发布节奏 — 约每 246.1 天发布一次 |
| 0/10 | OpenSSF Scorecard：Signed-Releases — 无数据 |
所用输入
| releases_count | 12 |
| latest_release_tag | v1.4.3 |
| releases_from_tags | 否 |
| days_since_latest_release | 10 |
| mean_days_between_releases | 246.1 |
已排除计分（无数据或不适用）：OpenSSF Scorecard：Signed-Releases。 其余权重已重新归一化。
社区与采用
项目是否拥有用户、下载量与关注度，并具备欢迎贡献者参与的配置？
50
流行度与采用
56中等
评分方式
| 38.7/60 | 星标 — 245 个星标 |
| 11.7/25 | 复刻 — 26 个复刻 |
| 5.8/15 | 关注者 — 12 位关注者 |
所用输入
| forks | 26 |
| stars | 245 |
| watchers | 12 |
| growth_state | unverified |
| growth_factor_pct | 100 |
| growth_unverified_reason | no_history |
社区健康
44薄弱
评分方式
| 22.5/22.5 | README |
| 16.9/22.5 | 许可证 — 存在许可证文件，但不是可识别的许可证 |
| 0/18 | CONTRIBUTING 指南 |
| 0/13.5 | 行为准则 |
| 0/7.2 | 议题模板 |
| 0/6.3 | PR 模板 |
所用输入
| has_readme | 是 |
| has_license | 是 |
| readme_badges | — |
| has_contributing | 否 |
| has_issue_template | 否 |
| has_code_of_conduct | 否 |
| readme_badge_services | — |
| has_pull_request_template | 否 |
可持续性与治理
项目能否在其成员之外延续——巴士系数、响应能力、由谁支持，以及软件包的维护状况？
76
维护者韧性（巴士系数）
77良好
评分方式
| 36/54 | 巴士系数 — 3 位贡献者贡献了半数提交 |
| 17.4/22.5 | 提交分布 — 头号贡献者编写了 23% 的提交 |
| 13.5/13.5 | 贡献者广度 — 15 位贡献者 |
| 10/10 | OpenSSF Scorecard：Contributors — project has 9 contributing companies or organizations |
所用输入
| bus_factor | 3 |
| contributors_sampled | 15 |
| top_contributor_share | 0.228 |
议题与 PR 响应能力
81优秀
评分方式
| 42/42 | 议题解决 — 100% 的议题已关闭 |
| 26.6/30 | PR 接受 — 已裁定的 PR 中 62/70 已合并 |
| 0/13 | Newcomer PR acceptance — 30 天内没有首次贡献者的 PR 得到裁决 |
| 1.5/15 | OpenSSF Scorecard：Code-Review — Found 2/13 approved changesets -- score normalized to 1 |
所用输入
| merged_prs | 62 |
| open_issues | 0 |
| closed_issues | 6 |
| prs_merged_7d | — |
| prs_decided_7d | — |
| prs_merged_30d | — |
| prs_decided_30d | — |
| issue_closed_ratio | 1 |
| closed_unmerged_prs | 8 |
| first_time_authors_30d | — |
| first_time_prs_merged_30d | — |
| first_time_prs_decided_30d | — |
已排除计分（无数据或不适用）：newcomer_pr_acceptance。 其余权重已重新归一化。
所有权与托管责任
71良好
评分方式
| 30/30 | 所有权背书 — 组织持有 |
| 0/20 | 已验证域名 |
| 16.1/25 | 所有者影响力 — rocq-community 有 170 位关注者 |
| 25/25 | 既往记录 — 76 个公开仓库，账户约 8 年 |
所用输入
| followers | 170 |
| owner_type | Organization |
| is_verified | — |
| owner_login | rocq-community |
| public_repos | 76 |
| account_age_days | 3,150 |
工程质量
基础的工程与文档实践是否到位？
41
工程实践
28存在风险
评分方式
| 24/24 | CI 工作流 — 4 个工作流 |
| 0/24 | 存在测试 |
| 0/16 | Linter 配置 |
| 0/9.6 | Pre-commit 钩子 |
| 0/6.4 | .editorconfig |
| 4/20 | OpenSSF Scorecard：CI-Tests — 3 out of 13 merged PRs checked by a CI test -- score normalized to 2 |
所用输入
| has_ci | 是 |
| has_tests | 否 |
| has_editorconfig | 否 |
| has_linter_config | 否 |
| has_precommit_config | 否 |
文档
60中等
评分方式
| 30/30 | README |
| 0/25 | 文档目录 |
| 0/15 | 文档 / 主页站点 |
| 10/10 | 仓库描述 |
| 10/10 | 主题标签 — 5 个主题标签 |
| 10/10 | Wiki |
所用输入
| topics | coq, ssreflect, mathcomp, four-color-theorem, coq-ci |
| has_wiki | 是 |
| homepage | — |
| has_readme | 是 |
| has_docs_dir | 否 |
| has_description | 是 |
安全
可见的安全与供应链实践是否稳固，且不存在未解决的高风险司法辖区暴露？
36
安全态势
36薄弱
评分方式
| 7.5/7.5 | Binary-Artifacts — no binaries found in the repo |
| 0/7.5 | Branch-Protection — 无数据 |
| 0.5/2.5 | CI-Tests — 3 out of 13 merged PRs checked by a CI test -- score normalized to 2 |
| 0/2.5 | CII-Best-Practices — no effort to earn an OpenSSF best practices badge detected |
| 0.8/7.5 | Code-Review — Found 2/13 approved changesets -- score normalized to 1 |
| 2.5/2.5 | Contributors — project has 9 contributing companies or organizations |
| 10/10 | Dangerous-Workflow — no dangerous workflow patterns detected |
| 0/7.5 | Dependency-Update-Tool — no update tool detected |
| 0/5 | Fuzzing — project is not fuzzed |
| 2.2/2.5 | 许可证 — license file detected |
| 0/7.5 | Maintained — 0 commit(s) and 0 issue activity found in the last 90 days -- score normalized to 0 |
| 0/5 | Packaging — 无数据 |
| 0/5 | Pinned-Dependencies — dependency not pinned by hash detected -- score normalized to 0 |
| 0/5 | SAST — SAST tool is not run on all commits -- score normalized to 0 |
| 0/5 | Security-Policy — security policy file not detected |
| 0/7.5 | Signed-Releases — 无数据 |
| 0/7.5 | Token-Permissions — detected GitHub workflow tokens with excessive permissions |
| 7.5/7.5 | Vulnerabilities — 0 existing vulnerabilities detected |
所用输入
| source | openssf_scorecard |
| checks_evaluated | 15 |
| scorecard_version | v5.5.0 |
| checks_inconclusive | 3 |
| scorecard_aggregate | 3.6 |
已排除计分（无数据或不适用）：branch_protection, packaging, signed_releases。 其余权重已重新归一化。
AI 就绪度
该仓库在多大程度上具备与 AI 编码代理协同开发与维护的条件？权重刻意设小（4%）：代理工具链是一项真实的维护信号，但完全不具备的仓库仍可达到 100/100。
22
AI 代理上下文与指引
25存在风险
评分方式
| 0/45 | 代理指令 — 没有 CLAUDE.md / AGENTS.md / 编辑器规则 |
| 0/15 | 机器可读文档（llms.txt） |
| 25.1/40 | 可读的提交历史 — 100 次人类提交中有 47 次说明了意图（结构化标题或解释性正文） |
所用输入
| has_llms_txt | 否 |
| legible_history_share | 0.47 |
| agent_instruction_files | — |
| agent_instruction_max_bytes | — |
验证循环（构建 / 测试 / 类型检查）
28存在风险
评分方式
| 18/18 | 一条命令的引导启动 — Makefile, theories/proof/Makefile, theories/reals/Makefile |
| 0/22 | 自动化测试 |
| 0/11 | Lint / 格式化配置 |
| 0/11 | 静态类型检查 |
| 10/10 | 可复现环境 — Nix |
| 0/10 | 已体现的代理实践 — 最近 100 次提交中没有代理编写的提交 |
| 0/8 | 自动化维护 — 未观察到自动依赖更新 |
| 0/10 | OpenSSF Scorecard：Pinned-Dependencies — dependency not pinned by hash detected -- score normalized to 0 |
所用输入
| has_nix | 是 |
| has_tests | 否 |
| lockfiles | — |
| has_dockerfile | 否 |
| typed_language | 否 |
| bootstrap_files | Makefile, theories/proof/Makefile, theories/reals/Makefile |
| has_devcontainer | 否 |
| has_linter_config | 否 |
| typecheck_configs | — |
| agent_commit_share | 0 |
| toolchain_manifests | — |
| dependency_bot_commit_share | 0 |
面向模型的代码可读性
1危急
评分方式
| 0/45 | 可类型检查的代码 — Rocq Prover，未配置类型检查 |
| 0/55 | 可控的文件大小 — 未检测到源文件 |
所用输入
| primary_language | Rocq Prover |
| largest_source_bytes | — |
| source_files_sampled | 0 |
| oversized_source_files | 0 |
已排除计分（无数据或不适用）：可控的文件大小。 其余权重已重新归一化。
关键数据
245GitHub 星标
15贡献者
4最近 12 个月提交数
10距最近推送天数
12发布版本数
3巴士系数（bus factor）
0开放议题
—软件包生态系统数
数据采集警告
- Star history unavailable: GitHub GraphQL error: Resource not accessible by personal access token
更多细节
Star 与 Fork 历史 0 ★ / 26 ⇿
0Star
26Fork
11发布
每颗 star 和每个 fork 的添加时间，来自 GitHub 并按天汇总。累计增长位于其构成来源——每日新增——的正上方，二者可相互对照：稳定的自然增长与短暂的突增形态截然不同。当这一差别可被衡量时，它会作为增长真实性予以报告。
主版本 0次版本 2修订 8
每个点涵盖 7 天。
OpenSSF Scorecard 3.6 / 10
3.6综合
来自开源项目 OpenSSF Scorecard 的独立、工具无关的安全评估。每项检查奖励的是安全实践本身，而非特定供应商的工具。Scorecard 无法判定的检查项标记为 不适用，并从安全评分中剔除（绝不按零分计）。
| 10 | Binary-Artifacts | no binaries found in the repo |
| 不适用 | Branch-Protection | internal error: error during branchesHandler.setup: internal error: some github tokens can't read classic branch protection rules: https://github.com/ossf/scorecard-action/blob/main/docs/authentication/fine-grained-auth-token.md |
| 2 | CI-Tests | 3 out of 13 merged PRs checked by a CI test -- score normalized to 2 |
| 0 | CII-Best-Practices | no effort to earn an OpenSSF best practices badge detected |
| 1 | Code-Review | Found 2/13 approved changesets -- score normalized to 1 |
| 10 | Contributors | project has 9 contributing companies or organizations |
| 10 | Dangerous-Workflow | no dangerous workflow patterns detected |
| 0 | Dependency-Update-Tool | no update tool detected |
| 0 | Fuzzing | project is not fuzzed |
| 9 | License | license file detected |
| 0 | Maintained | 0 commit(s) and 0 issue activity found in the last 90 days -- score normalized to 0 |
| 不适用 | Packaging | packaging workflow not detected |
| 0 | Pinned-Dependencies | dependency not pinned by hash detected -- score normalized to 0 |
| 0 | SAST | SAST tool is not run on all commits -- score normalized to 0 |
| 0 | Security-Policy | security policy file not detected |
| 不适用 | Signed-Releases | no releases found |
| 0 | Token-Permissions | detected GitHub workflow tokens with excessive permissions |
| 10 | Vulnerabilities | 0 existing vulnerabilities detected |
全部依赖 0
来自 GitHub 依赖图的完整解析依赖集合：0 个直接依赖与 0 个间接（传递）软件包。仓库提交锁文件时，传递闭包才是完整的。
| 注册表 | 软件包 | 版本 | 关系 |
|---|
依赖安全公告 未评估
本报告未能完成公告比对：No resolved dependencies to assess
原始 JSON 报告 机器可读
{
"data": {
"repo": {
"topics": [
"coq",
"ssreflect",
"mathcomp",
"four-color-theorem",
"coq-ci"
],
"is_fork": false,
"size_kb": 890,
"has_wiki": true,
"homepage": null,
"languages": {
"Nix": 4385,
"Makefile": 3270,
"Rocq Prover": 2020753
},
"pushed_at": "2026-07-17T13:33:53Z",
"created_at": "2018-11-06T17:43:35Z",
"owner_type": "Organization",
"updated_at": "2026-06-30T11:19:42Z",
"description": "Formal proof of the Four Color Theorem [maintainer=@ybertot]",
"is_archived": false,
"is_disabled": false,
"license_spdx": null,
"default_branch": "master",
"license_spdx_raw": "NOASSERTION",
"primary_language": "Rocq Prover",
"significant_languages": [
"Rocq Prover"
]
},
"owner": {
"blog": "https://rocq-community.org",
"name": "Rocq-community",
"type": "Organization",
"login": "rocq-community",
"company": null,
"location": null,
"followers": 170,
"avatar_url": "https://avatars.githubusercontent.com/u/34452610?v=4",
"created_at": "2017-12-11T16:11:12Z",
"is_verified": null,
"public_repos": 76,
"account_age_days": 3150
},
"license": {
"state": "custom",
"spdx_id": null,
"raw_spdx": "NOASSERTION",
"file_present": true,
"scorecard_found": true,
"profile_has_license": true
},
"activity": {
"releases": [
{
"tag": "v1.4.3",
"kind": "patch",
"published_at": "2026-07-17T13:33:53Z"
},
{
"tag": "v1.4.2",
"kind": "patch",
"published_at": "2025-10-14T07:16:36Z"
},
{
"tag": "v1.4.1",
"kind": "patch",
"published_at": "2025-04-16T06:55:15Z"
},
{
"tag": "v1.4.0",
"kind": "minor",
"published_at": "2024-11-15T07:18:04Z"
},
{
"tag": "v1.3.1",
"kind": "patch",
"published_at": "2023-10-26T13:45:33Z"
},
{
"tag": "v1.3.0",
"kind": "minor",
"published_at": "2023-05-26T07:30:58Z"
},
{
"tag": "v1.2.5",
"kind": "patch",
"published_at": "2022-07-13T12:59:49Z"
},
{
"tag": "v1.2.4",
"kind": "patch",
"published_at": "2022-01-26T14:13:38Z"
},
{
"tag": "v1.2.3",
"kind": "patch",
"published_at": "2020-12-16T15:13:47Z"
},
{
"tag": "v1.2.2",
"kind": "patch",
"published_at": "2020-06-23T10:54:01Z"
},
{
"tag": "v1.2.1",
"kind": "patch",
"published_at": "2020-02-27T15:02:00Z"
},
{
"tag": "v1.2",
"kind": "other",
"published_at": "2019-04-25T13:01:29Z"
}
],
"recent_commits": [
{
"oid": "f2fcc837b817632f334f9c7d7fbb0195ad4ba4e2",
"body": "Adapt to https://github.com/rocq-prover/rocq/pull/21849",
"is_bot": false,
"headline": "Merge pull request #77 from rocq-community/rocq21849",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2026-04-01T13:55:05Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "7fd114d8159b8a4c26605ea607e54664a7a7a233",
"body": null,
"is_bot": false,
"headline": "Adapt to https://github.com/rocq-prover/rocq/pull/21849",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2026-04-01T13:24:01Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "43a1b511e44c2be655bd5b1b663ec683b94f5915",
"body": "Adapt to https://github.com/math-comp/math-comp/pull/1545",
"is_bot": false,
"headline": "Merge pull request #76 from rocq-community/mc1545",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2026-03-03T14:43:41Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "3d0fb645cd8c94e7c4559297be614a774c6c95e5",
"body": null,
"is_bot": false,
"headline": "Adapt to https://github.com/math-comp/math-comp/pull/1545",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2026-02-26T11:01:22Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "9990abd7a15f80916c14367ac6dec947a836e60e",
"body": "Address notation warnings",
"is_bot": false,
"headline": "Merge pull request #74 from rocq-community/mc1110",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2025-06-18T07:18:49Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "e4395482c6669eb23eba6966accf56ebd628e704",
"body": null,
"is_bot": false,
"headline": "Address notation warnings",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2025-06-17T15:13:25Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "9e52fe907a057021db44612659d9255c88235805",
"body": null,
"is_bot": false,
"headline": "[CI] Update Nix toolbox",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2025-06-17T15:13:25Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "a722b67d60d7e12a41aef7ec3154c829918e529c",
"body": null,
"is_bot": false,
"headline": "Drop support for Coq 8.18 and 8.19 and MC <= 2.4",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2025-06-17T14:02:43Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "dff565790a6aad4d64373046e723c4163c85b5f9",
"body": "Adapt to https://github.com/math-comp/math-comp/pull/1354",
"is_bot": false,
"headline": "Merge pull request #72 from rocq-community/mc1354",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2025-04-25T06:53:56Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "18f0f29954f10c1245035844ecc6732dd8c6a8ad",
"body": null,
"is_bot": false,
"headline": "80 char lines",
"author_name": "Quentin Vermande",
"author_login": "Tragicus",
"committed_at": "2025-03-25T12:45:06Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "5696469244c4610de00db7f971b62793e5ff9249",
"body": null,
"is_bot": false,
"headline": "lock gedge, gnode and gface",
"author_name": "Quentin Vermande",
"author_login": "Tragicus",
"committed_at": "2025-03-25T12:45:06Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "7cea617766581c01fcd1c2decc64231bb6e9f9cc",
"body": null,
"is_bot": false,
"headline": "Adapt to https://github.com/math-comp/math-comp/pull/1354",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2025-02-28T12:13:21Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "de7e174a7327c0e228bc3ad28ea13c38e37e9166",
"body": "Update opam files following removal of Stdlib dep",
"is_bot": false,
"headline": "Merge pull request #71 from coq-community/opam",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2025-02-25T10:02:19Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "add58b42e3ec4b934ce2369fab533a5cac40e506",
"body": null,
"is_bot": false,
"headline": "Update opam files following removal of Stdlib dep",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2025-02-25T08:55:30Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "b23e3a827a832a5927c442084af7569d45930d22",
"body": "Fix sed commands for MacOS",
"is_bot": false,
"headline": "Merge pull request #70 from coq-community/fix-macos",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2025-02-24T14:08:22Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "0398d489b923cd1ecc5dab0e839b86a84596b863",
"body": null,
"is_bot": false,
"headline": "Fix sed commands for MacOS",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2025-02-24T14:07:29Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "ed53286e1f81146a17234bd446fd15d773d5cb8e",
"body": "Remove Stdlib dependency",
"is_bot": false,
"headline": "Merge pull request #68 from coq-community/no-stdlib",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2025-02-22T10:34:39Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "16621330f2a8021c78ddd0c35978ff2a2e9776f2",
"body": null,
"is_bot": false,
"headline": "Remove Stdlib dependency",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2025-02-21T19:20:48Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "1781e69252cd1b18253f59467f63159d4a3d73ec",
"body": null,
"is_bot": false,
"headline": "[CI] Remove 8.16 and 8.17",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2025-02-21T19:20:48Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "05aba1518f888fdf9de8ef6997682832a87c505d",
"body": "|CI] Update Nix toolbox",
"is_bot": false,
"headline": "Merge pull request #69 from coq-community/ci-update",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2025-02-20T16:36:51Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "2950f959bd6eaa0b5a647ebcbf001ce2677318bc",
"body": null,
"is_bot": false,
"headline": "[CI] Update Nix toolbox",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2025-02-19T08:48:16Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "1e94ffa35df8581fc90dbddd586cdec69a20eaa2",
"body": "adjust CI to Rocq changes",
"is_bot": false,
"headline": "Merge pull request #67 from coq-community/ci-fix-8.20",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2025-02-09T16:43:21Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "f48e9ea4b00c49eb7c0e6329ff963fa12ecfeebb",
"body": null,
"is_bot": false,
"headline": "adjust CI to Rocq changes",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2025-02-09T16:00:28Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "2cd48e2db50edff6a65b4f91eb29dd88d1242d15",
"body": "Another way to adapt to math-comp#1300",
"is_bot": false,
"headline": "Merge pull request #66 from CohenCyril/mc1300",
"author_name": "Cyril Cohen",
"author_login": "CohenCyril",
"committed_at": "2025-01-23T13:40:45Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "595c6248074000a16c22f9e25555529cd4966abc",
"body": null,
"is_bot": false,
"headline": "update wrt math-comp#1300",
"author_name": "Cyril Cohen",
"author_login": "CohenCyril",
"committed_at": "2024-12-09T15:43:16Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "1739214a760d7844e971cb8170707b0395f55c6d",
"body": null,
"is_bot": false,
"headline": "modify meta.yml and generate README.md for new building instructions",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2024-11-14T15:28:16Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "b1a9bfab5f84b1d6245403bb725c76d49416786d",
"body": null,
"is_bot": false,
"headline": "introduce makefiles in subdirectories, modify opam packages to use them",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2024-11-14T15:28:16Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "0b91f2244a9ac1e437e87e0a5d60ac084efa705f",
"body": null,
"is_bot": false,
"headline": "introduce reals and proof subdirectories for theories",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2024-11-14T15:28:16Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "c028f9bbed175407c23ee86ef2c70592c1caeaf5",
"body": "adapt to MC#1256",
"is_bot": false,
"headline": "Merge pull request #62 from Tragicus/pr1256",
"author_name": "Quentin VERMANDE",
"author_login": "Tragicus",
"committed_at": "2024-08-06T08:14:35Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "a361c3bca6a73f83127b502c128d44617d340279",
"body": null,
"is_bot": false,
"headline": "adapt to MC#1256",
"author_name": "Quentin Vermande",
"author_login": "Tragicus",
"committed_at": "2024-08-05T11:48:03Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "1efde3a89655849947a94a2ec5412397c0e8e47e",
"body": "switch Docker CI cron to weekly, explicit dependency on HB",
"is_bot": false,
"headline": "Merge pull request #61 from coq-community/ci-weekly",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2024-07-24T12:13:49Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "832787e00857627a5c49e03fb9d6b19d722f0dd1",
"body": null,
"is_bot": false,
"headline": "switch Docker CI cron to weekly, explicit dependency on HB",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2024-07-24T11:39:48Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "c9429eb0ec0f1f4dcc89afa3d3ad8ff1b6deebdb",
"body": "add HAL paper in meta.yml and README.md",
"is_bot": false,
"headline": "Merge pull request #60 from coq-community/add-hal-paper",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2024-07-02T22:26:17Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "efbff79362e1480ad097652d3860ffd7adc13e73",
"body": null,
"is_bot": false,
"headline": "add HAL paper in meta.yml and README.md",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2024-07-02T21:39:37Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "250cd386790cadf8d83a2bae6bc58448278578f1",
"body": "Treat a deprecation warning about Qint",
"is_bot": false,
"headline": "Merge pull request #59 from coq-community/deprecation-Qint",
"author_name": "Kazuhiko Sakaguchi",
"author_login": "pi8027",
"committed_at": "2024-07-02T14:06:05Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "b8a5126f3932b3cac740a83eb590531abd1df3f0",
"body": null,
"is_bot": false,
"headline": "Treat a deprecation warning about Qint",
"author_name": "Kazuhiko Sakaguchi",
"author_login": "pi8027",
"committed_at": "2024-07-02T12:48:16Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "027788b559b56218fbe8b28a0723d556b0c5b27d",
"body": "Adapt to https://github.com/math-comp/math-comp/pull/1223",
"is_bot": false,
"headline": "Merge pull request #58 from coq-community/mc_1223",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2024-06-29T10:55:23Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "5be6c5a1c57486de03cd9a6823196ed4b04fab4c",
"body": null,
"is_bot": false,
"headline": "Adapt to https://github.com/math-comp/math-comp/pull/1223",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2024-06-28T07:29:04Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "91ff6b8b846c8ad683260a5e6ce400e186f43c6e",
"body": "…cker\n\nremove mathcomp-dev-coq-8.17 Docker job",
"is_bot": false,
"headline": "Merge pull request #56 from coq-community/remove-mathcomp-dev-8.17-do…",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2024-04-29T07:58:06Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "6b278e4fd9851a2570a03e4696054a59836dbcaf",
"body": null,
"is_bot": false,
"headline": "remove mathcomp-dev-coq-8.17 Docker job",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2024-04-29T07:33:07Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "0ee53c3aa85621aeba6e73a9f1acafa37574b623",
"body": "Adapt to math-comp/math-comp#1190",
"is_bot": false,
"headline": "Merge pull request #55 from coq-community/mc_1190",
"author_name": "Kazuhiko Sakaguchi",
"author_login": "pi8027",
"committed_at": "2024-03-28T16:35:53Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "57b46dca7d3503e4615b6164a2f5e1245414d55f",
"body": null,
"is_bot": false,
"headline": "Update CI",
"author_name": "Kazuhiko Sakaguchi",
"author_login": "pi8027",
"committed_at": "2024-03-28T15:14:31Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "99a29672f5c79fcc3a502a25a720f1f9dcf6fcee",
"body": null,
"is_bot": false,
"headline": "Adapt to math-comp/math-comp#1190",
"author_name": "Kazuhiko Sakaguchi",
"author_login": "pi8027",
"committed_at": "2024-03-28T15:04:46Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "43719c0fb5fb6cb0c8fc1c2db09efc632c23df90",
"body": "[CI] Add MC 2.1.0",
"is_bot": false,
"headline": "Merge pull request #54 from coq-community/ci_mc_2_1_0",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2023-10-26T13:43:57Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "3eff46b1411227c36e9281dab558f3963696c689",
"body": null,
"is_bot": false,
"headline": "[CI] Update Nix CI",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2023-10-26T12:36:39Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "72ec2270fcde967aef04ce0ebd7c0196ed8ba5c7",
"body": null,
"is_bot": false,
"headline": "[CI] Add MC 2.1",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2023-10-26T10:11:38Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "f127f32e644eded02312077f02ffbcc0c3254b75",
"body": "Fix w.r.t. math-comp/math-comp#682",
"is_bot": false,
"headline": "Merge pull request #27 from pi8027/fix-mathcomp-682",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2023-06-04T09:16:18Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "ef7070be2b523d9f93c1a294133a33d020c0c90f",
"body": null,
"is_bot": false,
"headline": "Fix w.r.t. math-comp/math-comp#682",
"author_name": "Kazuhiko Sakaguchi",
"author_login": "pi8027",
"committed_at": "2023-06-03T22:36:31Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "3e39e52e0a05e5819922f2d5d755fab114fe5870",
"body": null,
"is_bot": false,
"headline": "Update meta.yml",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2023-05-26T07:29:56Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "d62fa8f3f32469d913fcbe7918a22f816463a1e0",
"body": "Port to Hierarchy Builder",
"is_bot": false,
"headline": "Merge pull request #44 from coq-community/hierarchy-builder",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2023-05-11T12:31:30Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "dce84bff083f8dec8a7d360c8a2edf27b74761d6",
"body": null,
"is_bot": false,
"headline": "[CI] Update Docker",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2023-05-11T11:51:28Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "2a83a7b2fa75355af7f259dbe43fc1ac8bfbc3a1",
"body": null,
"is_bot": false,
"headline": "[CI] Update Nix",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2023-05-11T11:50:45Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "b39e7fedc7783b39f359a3d71a0eccb79f4b59f1",
"body": null,
"is_bot": false,
"headline": "Port to Hierarchy Builder",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2023-05-11T11:50:45Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "e831b0b00e264285f91938917a0a5ef64ec1a829",
"body": "boilerplate and ci for Coq 8.17 and MathComp 1.16.0",
"is_bot": false,
"headline": "Merge pull request #52 from coq-community/ci-8.17-mc-1.16.0",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2023-02-07T07:27:28Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "a1469a4238accade0c5c2c12de830aeeff73874d",
"body": null,
"is_bot": false,
"headline": "boilerplate and ci for Coq 8.17 and MathComp 1.16.0",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2023-02-06T22:47:48Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "d6127d4e02fdb141131f3aa07fa4d3d4baf71529",
"body": "use MathComp dev Docker image again",
"is_bot": false,
"headline": "Merge pull request #51 from coq-community/docker-dev-fix",
"author_name": "Yves Bertot",
"author_login": "ybertot",
"committed_at": "2022-11-16T12:27:11Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "9cae59e91619529cf809d4f080331e5e2eaefb1e",
"body": null,
"is_bot": false,
"headline": "use MathComp dev Docker image again",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2022-11-15T19:27:34Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "e6b86c5bdbcf169b09740da82ac4dc1c934c6f3b",
"body": "avoid using disabled mathcomp docker images in CI",
"is_bot": false,
"headline": "Merge pull request #50 from coq-community/remove-mathcomp-dev-docker",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2022-10-08T21:37:40Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "c32b2306fc2dcca7153b5af9e90c2497855af96d",
"body": null,
"is_bot": false,
"headline": "avoid using disable mathcomp docker images in CI",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2022-10-08T19:06:05Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "37639531f948eece6ba9662b28710327af2d9b32",
"body": "switch to using regular coq dev Docker image",
"is_bot": false,
"headline": "Merge pull request #49 from coq-community/switch-coq-dev-docker",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2022-10-05T22:57:08Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "3dcb7857a6eba0b0b9b9c340f0334c940edf232b",
"body": null,
"is_bot": false,
"headline": "switch to using regular coq dev Docker image",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2022-10-05T21:50:19Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "851949d1e226b68da1a867b6f30b33d99b9ed15e",
"body": "Add CI for coq 8.16",
"is_bot": false,
"headline": "Merge pull request #48 from coq-community/coq816",
"author_name": "Cyril Cohen",
"author_login": "CohenCyril",
"committed_at": "2022-07-13T12:58:20Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "a6471d37fd6387daf03e3abbf8aae47b0a2f6a6d",
"body": null,
"is_bot": false,
"headline": "Add CI for coq 8.16",
"author_name": "Cyril Cohen",
"author_login": "CohenCyril",
"committed_at": "2022-07-12T17:23:22Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "2eded10cab131e1d61fbc9d9f5f2ea68a24c241b",
"body": "testing mathcomp 1.15",
"is_bot": false,
"headline": "Merge pull request #47 from coq-community/mathcomp-1.15",
"author_name": "Cyril Cohen",
"author_login": "CohenCyril",
"committed_at": "2022-07-12T13:41:30Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "1d83166b5866f4981043b79eabc1ecbd437b0d40",
"body": null,
"is_bot": false,
"headline": "testing mathcomp 1.15 in CI",
"author_name": "Cyril Cohen",
"author_login": "CohenCyril",
"committed_at": "2022-07-11T11:05:23Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "d002a174eff3e180987de4df3df515d195ebb337",
"body": "Remove 1.12 deprecations",
"is_bot": false,
"headline": "Merge pull request #46 from coq-community/mc_898",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2022-06-25T13:29:15Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "274ec15b71b3c504b4d45cba5f86f3f19a930396",
"body": "To adapt to https://github.com/math-comp/math-comp/pull/898",
"is_bot": false,
"headline": "Remove 1.12 deprecations",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2022-06-25T12:35:13Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "c65c6a6151ae6f414d6f2b2e46ced6cc458b331f",
"body": "`inE` robustness wrt math-comp/math-comp#863",
"is_bot": false,
"headline": "Merge pull request #42 from ggonthier/inE-robustness",
"author_name": "Yves Bertot",
"author_login": "ybertot",
"committed_at": "2022-06-05T14:32:12Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "4486796de0df716779caf4e1ba0741cb642dd28c",
"body": "Rm warnings 8.11",
"is_bot": false,
"headline": "Merge pull request #43 from ybertot/rm-warnings-8.11",
"author_name": "Yves Bertot",
"author_login": "ybertot",
"committed_at": "2022-03-29T10:42:27Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "224fde601dce61889deac8879a11ae75c52b7d25",
"body": null,
"is_bot": false,
"headline": "fix order of directives",
"author_name": "Yves Bertot",
"author_login": "ybertot",
"committed_at": "2022-03-29T08:00:04Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "e8dc6293e15d64e4b1832f4d8f7455a15e451a10",
"body": null,
"is_bot": false,
"headline": "2 remaining duplicate clear, and silence other warnings in _CoqProject",
"author_name": "Yves Bertot",
"author_login": "ybertot",
"committed_at": "2022-03-28T15:41:41Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "65ea0f2005c88aa2acddce0088a4ff6fabe737b1",
"body": null,
"is_bot": false,
"headline": "remove unidiomatic empty clears between curly brackets",
"author_name": "Yves Bertot",
"author_login": "ybertot",
"committed_at": "2022-03-28T15:40:11Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "05250dda607b35a4e834935e5a3d95002bfa3482",
"body": "…etains\n\ncompatibility with coq-8.11 and math-comp 1.11",
"is_bot": false,
"headline": "removes some deprecation warnings and duplicate-clear warnings, but r…",
"author_name": "Yves Bertot",
"author_login": "ybertot",
"committed_at": "2022-03-28T15:40:11Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "990b2e9a81b97c261461c1da98f6890ee20c053c",
"body": null,
"is_bot": false,
"headline": "removed deprecation warnings and most duplicate clear warnings",
"author_name": "Yves Bertot",
"author_login": "ybertot",
"committed_at": "2022-03-28T15:40:11Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "8fe5f1a4517d74b5f238d4c288ff1bbba77dc25b",
"body": "Improve proof script robustness whereby selective rewriting depended on that `inE` expands `x \\in A, when `A` is one of the collective `pred`combinators (e.g., `[predU _ & _ ]`), into an expression involving `pred_of_simpl (mem ..) x` subexpression, which need to be further simplified using `/=` or \n[…]\ncit `3!inE` repeat counts.\n As part of this we inlined the `[predU _]` notation in the statement of the `diskN_E` lemma, since expanding it after using the lemma was awkward without the above hacks.",
"is_bot": false,
"headline": "`inE` robustness",
"author_name": "Georges Gonthier",
"author_login": "ggonthier",
"committed_at": "2022-03-18T15:36:43Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "944732e8b47b77e704b344315a14eec9cbfd9c26",
"body": "make Require Imports idiomatic",
"is_bot": false,
"headline": "Merge pull request #40 from coq-community/require-import",
"author_name": "Yves Bertot",
"author_login": "ybertot",
"committed_at": "2022-03-14T10:17:13Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "128a3baedfd65c3c6861057452a35db6487a8052",
"body": null,
"is_bot": false,
"headline": "make Require Imports idiomatic",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2022-03-11T19:58:54Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "8e808ceec873cf170676c5b7ab4fbad1c78d225d",
"body": "add meta.yml and generate coq-community boilerplate",
"is_bot": false,
"headline": "Merge pull request #38 from coq-community/meta",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2022-03-10T16:47:30Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "d2639bea9f8aba32569c3ddaa2f93e806a172199",
"body": null,
"is_bot": false,
"headline": "adjust Docker-Coq CI",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2022-03-10T15:43:32Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "5452d1e41032c757a54e9dcb0c0e5d407eb08ce7",
"body": null,
"is_bot": false,
"headline": "add meta.yml and generate coq-community boilerplate",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2022-03-10T15:43:32Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "b011f5659382fc1854ab8b81f34a44fbf2f1f439",
"body": "Fix Cachix.",
"is_bot": false,
"headline": "Merge pull request #39 from coq-community/fix-cachix",
"author_name": "Karl Palmskog",
"author_login": "palmskog",
"committed_at": "2022-03-10T15:42:13Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "618a8f9d8bbaf002f755a36a8e7df106bc8096ac",
"body": null,
"is_bot": false,
"headline": "Update Coq Nix Toolbox.",
"author_name": "Théo Zimmermann",
"author_login": "Zimmi48",
"committed_at": "2022-03-10T14:39:10Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "42e9a164d8f2222db811ef27cb500072bb12dfcb",
"body": "Fixup after the transfer to coq-community.",
"is_bot": false,
"headline": "Change to which Cachix CI can push.",
"author_name": "Théo Zimmermann",
"author_login": "Zimmi48",
"committed_at": "2022-03-10T14:37:55Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "497b7a36d17eea968ced4e65829c22474af5656b",
"body": "Add %N for nat constants",
"is_bot": false,
"headline": "Merge pull request #36 from proux01/nat-scope-constants",
"author_name": "Cyril Cohen",
"author_login": "CohenCyril",
"committed_at": "2022-02-14T16:43:34Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "ebc367a7822521a1543c8f06d9049b77aeffe7a9",
"body": null,
"is_bot": false,
"headline": "[CI] Add Coq 8.15 to Nix CI",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2022-02-14T12:18:22Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "a1d9ca29366d39b15f9021444e76573f2c33e187",
"body": "This is in preparation of\nhttps://github.com/math-comp/math-comp/pull/841\n\nThis is backward compatible (it only ensures that natural number\nconstants will kee being interpreted in nat_scope when a number\nnotation will be added in ring_scope). Add %N for nat constants",
"is_bot": false,
"headline": "Add %N for nat constants",
"author_name": "Pierre Roux",
"author_login": "proux01",
"committed_at": "2022-02-14T12:12:23Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "47698645f5b2c7bfbc6d634018a9ab6c666bf9cf",
"body": "update CI for mc 1.13 and 1.14",
"is_bot": false,
"headline": "Merge pull request #37 from math-comp/CI-mc.1.14",
"author_name": "Cyril Cohen",
"author_login": "CohenCyril",
"committed_at": "2022-01-26T12:24:45Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "54c610ae17e48254c36172a3e37cd6c3132f1ffd",
"body": null,
"is_bot": false,
"headline": "update CI for mathcomp 1.13 and 1.14",
"author_name": "Cyril Cohen",
"author_login": "CohenCyril",
"committed_at": "2022-01-26T11:21:40Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "4581901330cce906c3c58ce5c24e5d061ea3ab39",
"body": "force use of mc 1.12.0",
"is_bot": false,
"headline": "Merge pull request #34 from math-comp/nix-tooblox",
"author_name": "Cyril Cohen",
"author_login": "CohenCyril",
"committed_at": "2021-06-08T01:03:50Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "d1978ed4abeaa56fa16b8c43b3e768729d4312c3",
"body": null,
"is_bot": false,
"headline": "force use of mc 1.12.0",
"author_name": "Cyril Cohen",
"author_login": "CohenCyril",
"committed_at": "2021-06-07T21:35:59Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "ba42d6d5df293defbd7f00630cf5e0e8c2f25c90",
"body": "adding nix toolbox",
"is_bot": false,
"headline": "Merge pull request #33 from math-comp/nix-tooblox",
"author_name": "Cyril Cohen",
"author_login": "CohenCyril",
"committed_at": "2021-06-07T16:02:44Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "766e1e8231d77e78bc37f5231353abcbf1329a44",
"body": null,
"is_bot": false,
"headline": "adding nix toolbox",
"author_name": "Cyril Cohen",
"author_login": "CohenCyril",
"committed_at": "2021-06-07T15:21:56Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "cdcff4c4bae20482ecc2d0220fc39c064a9580a0",
"body": "Remove the reliance on Coq \"IF then else\" Prop notation.",
"is_bot": false,
"headline": "Merge pull request #32 from ppedrot/remove-if-then-else",
"author_name": "Yves Bertot",
"author_login": "ybertot",
"committed_at": "2021-04-29T07:04:14Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "0d1541d4956eccb7772422e843f2bb6e69d19e54",
"body": "Apart from being quite weird, it is a antiquated notation that is only used\nby this development.",
"is_bot": false,
"headline": "Remove the reliance on Coq \"IF then else\" Prop notation.",
"author_name": "Pierre-Marie Pédrot",
"author_login": "ppedrot",
"committed_at": "2021-04-26T16:18:03Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "e1cbfaaee469ed6a4f7fefc08a379f7e9fe55858",
"body": "realplane.v: fix typo in comment \"type\"",
"is_bot": false,
"headline": "Merge pull request #31 from Blaisorblade/patch-1",
"author_name": "Yves Bertot",
"author_login": "ybertot",
"committed_at": "2021-02-09T11:38:48Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "b752a1a2b2e4706fc397f0a9de1154751cc473f2",
"body": null,
"is_bot": false,
"headline": "realplane.v: add missing \"type\"",
"author_name": "Paolo G. Giarrusso",
"author_login": "Blaisorblade",
"committed_at": "2021-02-09T09:52:41Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "8cb0327098cde06a8e49be084df7a8bb6ee9bf07",
"body": "Rename coq-mathcomp-fourcolor.opam to coq-fourcolor.opam",
"is_bot": false,
"headline": "Merge pull request #29 from math-comp/fix-28",
"author_name": "Cyril Cohen",
"author_login": "CohenCyril",
"committed_at": "2021-02-04T12:34:21Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "d92ec989da11dfc19a78aca0c47a88163fba8a30",
"body": null,
"is_bot": false,
"headline": "Update coq-action.yml",
"author_name": "Cyril Cohen",
"author_login": "CohenCyril",
"committed_at": "2020-12-17T01:21:33Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "c7f267688d778289e9f3a4b5038ac458696218ad",
"body": "This should fix #28",
"is_bot": false,
"headline": "Rename coq-mathcomp-fourcolor.opam to coq-fourcolor.opam",
"author_name": "Cyril Cohen",
"author_login": "CohenCyril",
"committed_at": "2020-12-15T14:50:58Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "a72978a10c1eace75c2d7bb37b87f6cf7a7a4d69",
"body": "Selecting a precise occurence to rewrite",
"is_bot": false,
"headline": "Merge pull request #24 from math-comp/tune_simplification",
"author_name": "Cyril Cohen",
"author_login": "CohenCyril",
"committed_at": "2020-11-20T17:29:55Z",
"body_truncated": false,
"is_coding_agent": false
}
],
"releases_count": 12,
"commits_last_year": 4,
"latest_release_at": "2026-07-17T13:33:53Z",
"latest_release_tag": "v1.4.3",
"releases_from_tags": false,
"days_since_last_push": 10,
"active_weeks_last_year": 3,
"days_since_latest_release": 10,
"mean_days_between_releases": 246.1
},
"community": {
"has_readme": true,
"has_license": true,
"has_description": true,
"has_contributing": false,
"health_percentage": 37,
"has_issue_template": false,
"has_code_of_conduct": false,
"has_pull_request_template": false
},
"ecosystem": {
"packages": []
},
"popularity": {
"forks": 26,
"stars": 245,
"watchers": 12,
"fork_history": {
"days": [
{
"date": "2018-12-05",
"count": 1
},
{
"date": "2019-01-17",
"count": 1
},
{
"date": "2019-04-16",
"count": 1
},
{
"date": "2019-05-06",
"count": 1
},
{
"date": "2019-08-20",
"count": 1
},
{
"date": "2020-04-07",
"count": 1
},
{
"date": "2020-06-22",
"count": 1
},
{
"date": "2020-10-06",
"count": 1
},
{
"date": "2020-11-20",
"count": 1
},
{
"date": "2020-12-20",
"count": 1
},
{
"date": "2021-02-09",
"count": 1
},
{
"date": "2021-04-20",
"count": 1
},
{
"date": "2021-04-26",
"count": 1
},
{
"date": "2021-07-16",
"count": 1
},
{
"date": "2021-09-01",
"count": 1
},
{
"date": "2022-01-22",
"count": 1
},
{
"date": "2022-12-24",
"count": 1
},
{
"date": "2023-11-18",
"count": 1
},
{
"date": "2024-08-05",
"count": 1
},
{
"date": "2024-11-30",
"count": 1
},
{
"date": "2024-12-09",
"count": 1
},
{
"date": "2025-05-07",
"count": 1
},
{
"date": "2026-03-09",
"count": 1
},
{
"date": "2026-06-20",
"count": 1
},
{
"date": "2026-07-10",
"count": 1
}
],
"complete": true,
"collected": 25,
"total_forks": 26
},
"star_history": null,
"open_issues_and_prs": 2
},
"ai_readiness": {
"has_nix": true,
"example_dirs": [],
"has_llms_txt": false,
"has_dockerfile": false,
"has_mcp_signal": false,
"bootstrap_files": [
"Makefile",
"theories/proof/Makefile",
"theories/reals/Makefile"
],
"api_schema_files": [],
"has_devcontainer": false,
"typecheck_configs": [],
"toolchain_manifests": [],
"largest_source_bytes": null,
"source_files_sampled": 0,
"oversized_source_files": 0,
"agent_instruction_files": [],
"agent_instruction_max_bytes": null
},
"dependencies": {
"manifests": [],
"advisories": {
"error": "No resolved dependencies to assess",
"scope": "repository_graph",
"source": null,
"findings": [],
"collected": false,
"malicious": [],
"truncated": false,
"by_severity": {},
"advisory_count": 0,
"affected_count": 0,
"assessed_count": 0,
"malicious_count": 0,
"assessed_package": null,
"unassessed_count": 0,
"direct_affected_count": 0
},
"ecosystems": [],
"dependencies": [],
"all_dependencies": {
"error": null,
"source": "github-sbom",
"packages": [],
"collected": true,
"truncated": false,
"total_count": 0,
"direct_count": 0,
"indirect_count": 0
}
},
"maintainership": {
"issues": {
"open_prs": 2,
"merged_prs": 62,
"open_issues": 0,
"closed_ratio": 1,
"closed_issues": 6,
"closed_unmerged_prs": 8
},
"bus_factor": 3,
"bot_contributors": 0,
"top_contributors": [
{
"type": "User",
"login": "proux01",
"commits": 34,
"avatar_url": "https://avatars.githubusercontent.com/u/15833376?v=4"
},
{
"type": "User",
"login": "CohenCyril",
"commits": 28,
"avatar_url": "https://avatars.githubusercontent.com/u/298705?v=4"
},
{
"type": "User",
"login": "ggonthier",
"commits": 23,
"avatar_url": "https://avatars.githubusercontent.com/u/15231773?v=4"
},
{
"type": "User",
"login": "palmskog",
"commits": 23,
"avatar_url": "https://avatars.githubusercontent.com/u/397424?v=4"
},
{
"type": "User",
"login": "ybertot",
"commits": 13,
"avatar_url": "https://avatars.githubusercontent.com/u/3407333?v=4"
},
{
"type": "User",
"login": "pi8027",
"commits": 9,
"avatar_url": "https://avatars.githubusercontent.com/u/111003?v=4"
},
{
"type": "User",
"login": "ejgallego",
"commits": 4,
"avatar_url": "https://avatars.githubusercontent.com/u/7192257?v=4"
},
{
"type": "User",
"login": "Tragicus",
"commits": 4,
"avatar_url": "https://avatars.githubusercontent.com/u/96025499?v=4"
},
{
"type": "User",
"login": "gares",
"commits": 3,
"avatar_url": "https://avatars.githubusercontent.com/u/1013846?v=4"
},
{
"type": "User",
"login": "erikmd",
"commits": 2,
"avatar_url": "https://avatars.githubusercontent.com/u/10367254?v=4"
}
],
"contributors_sampled": 15,
"top_contributor_share": 0.228
},
"quality_signals": {
"has_ci": true,
"has_tests": false,
"ci_workflows": [
"docker-action.yml",
"nix-action-8.20.yml",
"nix-action-9.0.yml",
"nix-action-master.yml"
],
"has_docs_dir": false,
"linter_configs": [],
"has_editorconfig": false,
"has_linter_config": false,
"has_precommit_config": false
},
"security_signals": {
"lockfiles": [],
"scorecard": {
"checks": [
{
"name": "Binary-Artifacts",
"score": 10,
"reason": "no binaries found in the repo",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#binary-artifacts"
},
{
"name": "Branch-Protection",
"score": null,
"reason": "internal error: error during branchesHandler.setup: internal error: some github tokens can't read classic branch protection rules: https://github.com/ossf/scorecard-action/blob/main/docs/authentication/fine-grained-auth-token.md",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#branch-protection"
},
{
"name": "CI-Tests",
"score": 2,
"reason": "3 out of 13 merged PRs checked by a CI test -- score normalized to 2",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#ci-tests"
},
{
"name": "CII-Best-Practices",
"score": 0,
"reason": "no effort to earn an OpenSSF best practices badge detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#cii-best-practices"
},
{
"name": "Code-Review",
"score": 1,
"reason": "Found 2/13 approved changesets -- score normalized to 1",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#code-review"
},
{
"name": "Contributors",
"score": 10,
"reason": "project has 9 contributing companies or organizations",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#contributors"
},
{
"name": "Dangerous-Workflow",
"score": 10,
"reason": "no dangerous workflow patterns detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#dangerous-workflow"
},
{
"name": "Dependency-Update-Tool",
"score": 0,
"reason": "no update tool detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#dependency-update-tool"
},
{
"name": "Fuzzing",
"score": 0,
"reason": "project is not fuzzed",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#fuzzing"
},
{
"name": "License",
"score": 9,
"reason": "license file detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#license"
},
{
"name": "Maintained",
"score": 0,
"reason": "0 commit(s) and 0 issue activity found in the last 90 days -- score normalized to 0",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#maintained"
},
{
"name": "Packaging",
"score": null,
"reason": "packaging workflow not detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#packaging"
},
{
"name": "Pinned-Dependencies",
"score": 0,
"reason": "dependency not pinned by hash detected -- score normalized to 0",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#pinned-dependencies"
},
{
"name": "SAST",
"score": 0,
"reason": "SAST tool is not run on all commits -- score normalized to 0",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#sast"
},
{
"name": "Security-Policy",
"score": 0,
"reason": "security policy file not detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#security-policy"
},
{
"name": "Signed-Releases",
"score": null,
"reason": "no releases found",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#signed-releases"
},
{
"name": "Token-Permissions",
"score": 0,
"reason": "detected GitHub workflow tokens with excessive permissions",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#token-permissions"
},
{
"name": "Vulnerabilities",
"score": 10,
"reason": "0 existing vulnerabilities detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#vulnerabilities"
}
],
"commit": "f2fcc837b817632f334f9c7d7fbb0195ad4ba4e2",
"ran_at": "2026-07-27T23:55:13Z",
"aggregate_score": 3.6,
"scorecard_version": "v5.5.0"
},
"has_codeql_workflow": false,
"has_security_policy": false,
"has_dependabot_config": false
},
"contribution_flow": {
"collected": true,
"ci_last_run_at": "2026-07-26T07:49:59Z",
"oldest_open_prs": [
{
"number": 41,
"created_at": "2022-03-13T20:26:23Z",
"last_comment_at": "2022-03-23T10:28:29Z",
"last_comment_author": "ybertot"
},
{
"number": 78,
"created_at": "2026-07-19T09:40:21Z",
"last_comment_at": null,
"last_comment_author": null
}
],
"last_merged_pr_at": "2026-04-01T13:55:06Z",
"ci_last_conclusion": "SUCCESS",
"oldest_open_issues": []
}
},
"config": {
"disabled_metrics": [],
"disabled_categories": [],
"disabled_components": {}
},
"source": {
"url": "https://github.com/rocq-community/fourcolor",
"host": "github.com",
"name": "fourcolor",
"owner": "rocq-community"
},
"metrics": {
"overall": {
"key": "overall",
"band": "moderate",
"name": "Overall health",
"note": "The weighted overall 52 is calibrated to 53 on the published index scale (record calibration 2026-08-02).",
"notes": [
{
"code": "overall_calibration",
"params": {
"raw": 52,
"calibrated": 53,
"calibration": "2026-08-02"
}
}
],
"value": 53,
"inputs": {
"security": 36,
"vitality": 56,
"community": 50,
"governance": 76,
"calibration": "2026-08-02",
"engineering": 41,
"ai_readiness": 22,
"weighted_overall_raw": 52
},
"components": []
},
"categories": [
{
"key": "vitality",
"band": "moderate",
"name": "Vitality",
"value": 56,
"weight": 0.21,
"metrics": [
{
"key": "development_activity",
"band": "weak",
"name": "Development activity",
"note": null,
"notes": [],
"value": 37,
"inputs": {
"commits_last_year": 4,
"human_commit_share": 1,
"days_since_last_push": 10,
"active_weeks_last_year": 3
},
"components": [
{
"key": "push_recency",
"name": "Push recency",
"detail": "last push 10 days ago",
"points": 28.8,
"status": "partial",
"details": [
{
"code": "push_recency",
"params": {
"days": 10
}
}
],
"max_points": 36
},
{
"key": "commit_cadence",
"name": "Commit cadence",
"detail": "3/52 weeks with commits",
"points": 2.1,
"status": "partial",
"details": [
{
"code": "commit_cadence_weeks",
"params": {
"weeks": 3
}
}
],
"max_points": 36
},
{
"key": "commit_volume",
"name": "Commit volume",
"detail": "4 commits in the last year",
"points": 6.3,
"status": "partial",
"details": [
{
"code": "commits_last_year",
"params": {
"count": 4
}
}
],
"max_points": 18
},
{
"key": "openssf_scorecard_maintained",
"name": "OpenSSF Scorecard: Maintained",
"detail": "0 commit(s) and 0 issue activity found in the last 90 days -- score normalized to 0",
"points": 0,
"status": "missed",
"details": [],
"max_points": 10
}
]
},
{
"key": "release_discipline",
"band": "excellent",
"name": "Release discipline",
"note": "Excluded from scoring (no data or not applicable): OpenSSF Scorecard: Signed-Releases. Remaining weights renormalized.",
"notes": [
{
"code": "excluded_no_data",
"params": {
"components": [
"openssf_scorecard_signed_releases"
]
}
},
{
"code": "weights_renormalized",
"params": {}
}
],
"value": 84,
"inputs": {
"releases_count": 12,
"latest_release_tag": "v1.4.3",
"releases_from_tags": false,
"days_since_latest_release": 10,
"mean_days_between_releases": 246.1
},
"components": [
{
"key": "ships_releases",
"name": "Ships releases",
"detail": "12 releases published",
"points": 27,
"status": "met",
"details": [
{
"code": "releases_published",
"params": {
"count": 12
}
}
],
"max_points": 27
},
{
"key": "release_recency",
"name": "Release recency",
"detail": "latest release 10 days ago",
"points": 36,
"status": "met",
"details": [
{
"code": "release_recency",
"params": {
"days": 10
}
}
],
"max_points": 36
},
{
"key": "release_cadence",
"name": "Release cadence",
"detail": "a release every ~246.1 days",
"points": 12.6,
"status": "partial",
"details": [
{
"code": "release_cadence",
"params": {
"gap": 246.1
}
}
],
"max_points": 27
},
{
"key": "openssf_scorecard_signed_releases",
"name": "OpenSSF Scorecard: Signed-Releases",
"detail": "no releases found",
"points": 0,
"status": "excluded",
"details": [
{
"code": "no_data",
"params": {}
}
],
"max_points": 10
}
]
},
{
"key": "abandonment",
"band": "exceptional",
"name": "Abandonment",
"note": null,
"notes": [],
"value": 100,
"inputs": {
"cap": null,
"state": "maintained",
"guards": [],
"signals": [],
"red_flag": false,
"multiplier_pct": 100,
"declared_reason": null,
"unverified_reason": null,
"unanswered_open_prs": null,
"unanswered_open_issues": null,
"days_since_last_merged_pr": null,
"days_since_last_human_commit": 123,
"days_since_last_human_commit_is_floor": false
},
"components": [
{
"key": "project_is_still_maintained",
"name": "Project is still maintained",
"detail": "last human commit 123 days ago",
"points": 100,
"status": "met",
"details": [
{
"code": "abandonment_maintained",
"params": {
"days": 123
}
}
],
"max_points": 100
}
]
}
],
"description": "Is the project alive — is code being written and are releases shipping?"
},
{
"key": "community",
"band": "moderate",
"name": "Community & Adoption",
"value": 50,
"weight": 0.17,
"metrics": [
{
"key": "popularity",
"band": "moderate",
"name": "Popularity & adoption",
"note": null,
"notes": [],
"value": 56,
"inputs": {
"forks": 26,
"stars": 245,
"watchers": 12,
"growth_state": "unverified",
"growth_factor_pct": 100,
"growth_unverified_reason": "no_history"
},
"components": [
{
"key": "stars",
"name": "Stars",
"detail": "245 stars",
"points": 38.7,
"status": "partial",
"details": [
{
"code": "stars",
"params": {
"count": 245
}
}
],
"max_points": 60
},
{
"key": "forks",
"name": "Forks",
"detail": "26 forks",
"points": 11.7,
"status": "partial",
"details": [
{
"code": "forks",
"params": {
"count": 26
}
}
],
"max_points": 25
},
{
"key": "watchers",
"name": "Watchers",
"detail": "12 watchers",
"points": 5.8,
"status": "partial",
"details": [
{
"code": "watchers",
"params": {
"count": 12
}
}
],
"max_points": 15
}
]
},
{
"key": "community_health",
"band": "weak",
"name": "Community health",
"note": null,
"notes": [],
"value": 44,
"inputs": {
"has_readme": true,
"has_license": true,
"readme_badges": null,
"has_contributing": false,
"has_issue_template": false,
"has_code_of_conduct": false,
"readme_badge_services": [],
"has_pull_request_template": false
},
"components": [
{
"key": "readme",
"name": "README",
"detail": null,
"points": 22.5,
"status": "met",
"details": [],
"max_points": 22.5
},
{
"key": "license",
"name": "License",
"detail": "license file present, not a recognized license",
"points": 16.9,
"status": "partial",
"details": [
{
"code": "license_custom",
"params": {}
}
],
"max_points": 22.5
},
{
"key": "contributing_guide",
"name": "CONTRIBUTING guide",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 18
},
{
"key": "code_of_conduct",
"name": "Code of conduct",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 13.5
},
{
"key": "issue_template",
"name": "Issue template",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 7.2
},
{
"key": "pr_template",
"name": "PR template",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 6.3
}
]
}
],
"description": "Does the project have users, downloads, attention, and a welcoming setup for contributors?"
},
{
"key": "governance",
"band": "good",
"name": "Sustainability & Governance",
"value": 76,
"weight": 0.23,
"metrics": [
{
"key": "maintainer_resilience",
"band": "good",
"name": "Maintainer resilience (bus factor)",
"note": null,
"notes": [],
"value": 77,
"inputs": {
"bus_factor": 3,
"contributors_sampled": 15,
"top_contributor_share": 0.228
},
"components": [
{
"key": "bus_factor",
"name": "Bus factor",
"detail": "3 contributor(s) cover half of all commits",
"points": 36,
"status": "partial",
"details": [
{
"code": "bus_factor",
"params": {
"count": 3
}
}
],
"max_points": 54
},
{
"key": "commit_distribution",
"name": "Commit distribution",
"detail": "top contributor authored 23% of commits",
"points": 17.4,
"status": "partial",
"details": [
{
"code": "top_contributor_share",
"params": {
"share": 23
}
}
],
"max_points": 22.5
},
{
"key": "contributor_breadth",
"name": "Contributor breadth",
"detail": "15 contributors",
"points": 13.5,
"status": "met",
"details": [
{
"code": "contributors_sampled",
"params": {
"count": 15
}
}
],
"max_points": 13.5
},
{
"key": "openssf_scorecard_contributors",
"name": "OpenSSF Scorecard: Contributors",
"detail": "project has 9 contributing companies or organizations",
"points": 10,
"status": "met",
"details": [],
"max_points": 10
}
]
},
{
"key": "responsiveness",
"band": "excellent",
"name": "Issue & PR responsiveness",
"note": "Excluded from scoring (no data or not applicable): Newcomer PR acceptance. Remaining weights renormalized.",
"notes": [
{
"code": "excluded_no_data",
"params": {
"components": [
"newcomer_pr_acceptance"
]
}
},
{
"code": "weights_renormalized",
"params": {}
}
],
"value": 81,
"inputs": {
"merged_prs": 62,
"open_issues": 0,
"closed_issues": 6,
"prs_merged_7d": null,
"prs_decided_7d": null,
"prs_merged_30d": null,
"prs_decided_30d": null,
"issue_closed_ratio": 1,
"closed_unmerged_prs": 8,
"first_time_authors_30d": null,
"first_time_prs_merged_30d": null,
"first_time_prs_decided_30d": null
},
"components": [
{
"key": "issue_resolution",
"name": "Issue resolution",
"detail": "100% of issues closed",
"points": 42,
"status": "met",
"details": [
{
"code": "issues_closed_share",
"params": {
"share": 100
}
}
],
"max_points": 42
},
{
"key": "pr_acceptance",
"name": "PR acceptance",
"detail": "62/70 decided PRs merged",
"points": 26.6,
"status": "partial",
"details": [
{
"code": "decided_prs_merged",
"params": {
"merged": 62,
"decided": 70
}
}
],
"max_points": 30
},
{
"key": "newcomer_pr_acceptance",
"name": "Newcomer PR acceptance",
"detail": "no first-time contributor's PR decided in 30d",
"points": 0,
"status": "excluded",
"details": [
{
"code": "no_newcomer_prs",
"params": {
"days": 30
}
}
],
"max_points": 13
},
{
"key": "openssf_scorecard_code_review",
"name": "OpenSSF Scorecard: Code-Review",
"detail": "Found 2/13 approved changesets -- score normalized to 1",
"points": 1.5,
"status": "partial",
"details": [],
"max_points": 15
}
]
},
{
"key": "stewardship",
"band": "good",
"name": "Ownership & stewardship",
"note": null,
"notes": [],
"value": 71,
"inputs": {
"followers": 170,
"owner_type": "Organization",
"is_verified": null,
"owner_login": "rocq-community",
"public_repos": 76,
"account_age_days": 3150
},
"components": [
{
"key": "ownership_backing",
"name": "Ownership backing",
"detail": "organization-owned",
"points": 30,
"status": "met",
"details": [
{
"code": "owner_organization",
"params": {}
}
],
"max_points": 30
},
{
"key": "verified_domain",
"name": "Verified domain",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 20
},
{
"key": "owner_reach",
"name": "Owner reach",
"detail": "170 followers of rocq-community",
"points": 16.1,
"status": "partial",
"details": [
{
"code": "owner_followers",
"params": {
"count": 170,
"login": "rocq-community"
}
}
],
"max_points": 25
},
{
"key": "track_record",
"name": "Track record",
"detail": "76 public repos, account ~8 yr old",
"points": 25,
"status": "met",
"details": [
{
"code": "public_repos",
"params": {
"count": 76
}
},
{
"code": "account_age_years",
"params": {
"years": 8
}
}
],
"max_points": 25
}
]
}
],
"description": "Will the project survive its people — bus factor, responsiveness, who backs it, and package upkeep?"
},
{
"key": "engineering",
"band": "weak",
"name": "Engineering Quality",
"value": 41,
"weight": 0.19,
"metrics": [
{
"key": "engineering_practices",
"band": "at_risk",
"name": "Engineering practices",
"note": null,
"notes": [],
"value": 28,
"inputs": {
"has_ci": true,
"has_tests": false,
"has_editorconfig": false,
"has_linter_config": false,
"has_precommit_config": false
},
"components": [
{
"key": "ci_workflows",
"name": "CI workflows",
"detail": "4 workflow(s)",
"points": 24,
"status": "met",
"details": [
{
"code": "ci_workflows",
"params": {
"count": 4
}
}
],
"max_points": 24
},
{
"key": "tests_present",
"name": "Tests present",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 24
},
{
"key": "linter_config",
"name": "Linter config",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 16
},
{
"key": "pre_commit_hooks",
"name": "Pre-commit hooks",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 9.6
},
{
"key": "editorconfig",
"name": ".editorconfig",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 6.4
},
{
"key": "openssf_scorecard_ci_tests",
"name": "OpenSSF Scorecard: CI-Tests",
"detail": "3 out of 13 merged PRs checked by a CI test -- score normalized to 2",
"points": 4,
"status": "partial",
"details": [],
"max_points": 20
}
]
},
{
"key": "documentation",
"band": "moderate",
"name": "Documentation",
"note": null,
"notes": [],
"value": 60,
"inputs": {
"topics": [
"coq",
"ssreflect",
"mathcomp",
"four-color-theorem",
"coq-ci"
],
"has_wiki": true,
"homepage": null,
"has_readme": true,
"has_docs_dir": false,
"has_description": true
},
"components": [
{
"key": "readme",
"name": "README",
"detail": null,
"points": 30,
"status": "met",
"details": [],
"max_points": 30
},
{
"key": "documentation_directory",
"name": "Documentation directory",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 25
},
{
"key": "documentation_homepage_site",
"name": "Documentation / homepage site",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 15
},
{
"key": "repository_description",
"name": "Repository description",
"detail": null,
"points": 10,
"status": "met",
"details": [],
"max_points": 10
},
{
"key": "topics",
"name": "Topics",
"detail": "5 topics",
"points": 10,
"status": "met",
"details": [
{
"code": "topics_count",
"params": {
"count": 5
}
}
],
"max_points": 10
},
{
"key": "wiki",
"name": "Wiki",
"detail": null,
"points": 10,
"status": "met",
"details": [],
"max_points": 10
}
]
}
],
"description": "Are baseline engineering and documentation practices in place?"
},
{
"key": "security",
"band": "weak",
"name": "Security",
"value": 36,
"weight": 0.16,
"metrics": [
{
"key": "security_posture",
"band": "weak",
"name": "Security posture",
"note": "Excluded from scoring (no data or not applicable): Branch-Protection, Packaging, Signed-Releases. Remaining weights renormalized.",
"notes": [
{
"code": "excluded_no_data",
"params": {
"components": [
"branch_protection",
"packaging",
"signed_releases"
]
}
},
{
"code": "weights_renormalized",
"params": {}
}
],
"value": 36,
"inputs": {
"source": "openssf_scorecard",
"checks_evaluated": 15,
"scorecard_version": "v5.5.0",
"checks_inconclusive": 3,
"scorecard_aggregate": 3.6
},
"components": [
{
"key": "binary_artifacts",
"name": "Binary-Artifacts",
"detail": "no binaries found in the repo",
"points": 7.5,
"status": "met",
"details": [],
"max_points": 7.5
},
{
"key": "branch_protection",
"name": "Branch-Protection",
"detail": "internal error: error during branchesHandler.setup: internal error: some github tokens can't read classic branch protection rules: https://github.com/ossf/scorecard-action/blob/main/docs/authentication/fine-grained-auth-token.md",
"points": 0,
"status": "excluded",
"details": [
{
"code": "no_data",
"params": {}
}
],
"max_points": 7.5
},
{
"key": "ci_tests",
"name": "CI-Tests",
"detail": "3 out of 13 merged PRs checked by a CI test -- score normalized to 2",
"points": 0.5,
"status": "partial",
"details": [],
"max_points": 2.5
},
{
"key": "cii_best_practices",
"name": "CII-Best-Practices",
"detail": "no effort to earn an OpenSSF best practices badge detected",
"points": 0,
"status": "missed",
"details": [],
"max_points": 2.5
},
{
"key": "code_review",
"name": "Code-Review",
"detail": "Found 2/13 approved changesets -- score normalized to 1",
"points": 0.8,
"status": "partial",
"details": [],
"max_points": 7.5
},
{
"key": "contributors",
"name": "Contributors",
"detail": "project has 9 contributing companies or organizations",
"points": 2.5,
"status": "met",
"details": [],
"max_points": 2.5
},
{
"key": "dangerous_workflow",
"name": "Dangerous-Workflow",
"detail": "no dangerous workflow patterns detected",
"points": 10,
"status": "met",
"details": [],
"max_points": 10
},
{
"key": "dependency_update_tool",
"name": "Dependency-Update-Tool",
"detail": "no update tool detected",
"points": 0,
"status": "missed",
"details": [],
"max_points": 7.5
},
{
"key": "fuzzing",
"name": "Fuzzing",
"detail": "project is not fuzzed",
"points": 0,
"status": "missed",
"details": [],
"max_points": 5
},
{
"key": "license",
"name": "License",
"detail": "license file detected",
"points": 2.2,
"status": "partial",
"details": [],
"max_points": 2.5
},
{
"key": "maintained",
"name": "Maintained",
"detail": "0 commit(s) and 0 issue activity found in the last 90 days -- score normalized to 0",
"points": 0,
"status": "missed",
"details": [],
"max_points": 7.5
},
{
"key": "packaging",
"name": "Packaging",
"detail": "packaging workflow not detected",
"points": 0,
"status": "excluded",
"details": [
{
"code": "no_data",
"params": {}
}
],
"max_points": 5
},
{
"key": "pinned_dependencies",
"name": "Pinned-Dependencies",
"detail": "dependency not pinned by hash detected -- score normalized to 0",
"points": 0,
"status": "missed",
"details": [],
"max_points": 5
},
{
"key": "sast",
"name": "SAST",
"detail": "SAST tool is not run on all commits -- score normalized to 0",
"points": 0,
"status": "missed",
"details": [],
"max_points": 5
},
{
"key": "security_policy",
"name": "Security-Policy",
"detail": "security policy file not detected",
"points": 0,
"status": "missed",
"details": [],
"max_points": 5
},
{
"key": "signed_releases",
"name": "Signed-Releases",
"detail": "no releases found",
"points": 0,
"status": "excluded",
"details": [
{
"code": "no_data",
"params": {}
}
],
"max_points": 7.5
},
{
"key": "token_permissions",
"name": "Token-Permissions",
"detail": "detected GitHub workflow tokens with excessive permissions",
"points": 0,
"status": "missed",
"details": [],
"max_points": 7.5
},
{
"key": "vulnerabilities",
"name": "Vulnerabilities",
"detail": "0 existing vulnerabilities detected",
"points": 7.5,
"status": "met",
"details": [],
"max_points": 7.5
}
]
},
{
"key": "high_risk_jurisdiction_exposure",
"band": "exceptional",
"name": "High-Risk Jurisdiction Exposure",
"note": "Only high-confidence self-published location evidence affects this multiplier. Ambiguous matches are review-only; country evidence is not proof of nationality, citizenship, legal registration, malicious intent, or sanctions status.",
"notes": [
{
"code": "jurisdiction_evidence_limits",
"params": {}
}
],
"value": 100,
"inputs": {
"meaning": "self-published location evidence; not nationality or citizenship",
"red_flag": false,
"exposures": [],
"policy_countries": [
"Russia",
"Iran",
"North Korea"
],
"commit_weight_rule": {
"min_commits": 50,
"min_commit_share": 0.1
},
"review_only_matches": 0,
"below_threshold_exposures": [],
"assessed_self_published_locations": 8
},
"components": [
{
"key": "policy_exposure_multiplier",
"name": "Policy exposure multiplier",
"detail": "no confirmed policy-scope location match",
"points": 100,
"status": "met",
"details": [
{
"code": "jurisdiction_no_match",
"params": {}
}
],
"max_points": 100
}
]
}
],
"description": "Are visible security and supply-chain practices strong, with no malicious dependency and no unresolved high-risk jurisdiction exposure?"
},
{
"key": "ai_readiness",
"band": "at_risk",
"name": "AI Readiness",
"value": 22,
"weight": 0.04,
"metrics": [
{
"key": "ai_agent_context",
"band": "at_risk",
"name": "Agent context & guidance",
"note": null,
"notes": [],
"value": 25,
"inputs": {
"has_llms_txt": false,
"legible_history_share": 0.47,
"agent_instruction_files": [],
"agent_instruction_max_bytes": null
},
"components": [
{
"key": "agent_instructions",
"name": "Agent instructions",
"detail": "no CLAUDE.md / AGENTS.md / editor rules",
"points": 0,
"status": "missed",
"details": [
{
"code": "no_agent_instructions",
"params": {}
}
],
"max_points": 45
},
{
"key": "machine_readable_docs_llms_txt",
"name": "Machine-readable docs (llms.txt)",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 15
},
{
"key": "legible_commit_history",
"name": "Legible commit history",
"detail": "47 of 100 human commits state their intent (structured subject or explanatory body)",
"points": 25.1,
"status": "partial",
"details": [
{
"code": "legible_history",
"params": {
"legible": 47,
"sampled": 100
}
}
],
"max_points": 40
}
]
},
{
"key": "ai_verify_loop",
"band": "at_risk",
"name": "Verify loop (build / test / typecheck)",
"note": null,
"notes": [],
"value": 28,
"inputs": {
"has_nix": true,
"has_tests": false,
"lockfiles": [],
"has_dockerfile": false,
"typed_language": false,
"bootstrap_files": [
"Makefile",
"theories/proof/Makefile",
"theories/reals/Makefile"
],
"has_devcontainer": false,
"has_linter_config": false,
"typecheck_configs": [],
"agent_commit_share": 0,
"toolchain_manifests": [],
"dependency_bot_commit_share": 0
},
"components": [
{
"key": "one_command_bootstrap",
"name": "One-command bootstrap",
"detail": "Makefile, theories/proof/Makefile, theories/reals/Makefile",
"points": 18,
"status": "met",
"details": [
{
"code": "file_list",
"params": {
"files": "Makefile, theories/proof/Makefile, theories/reals/Makefile"
}
}
],
"max_points": 18
},
{
"key": "automated_tests",
"name": "Automated tests",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 22
},
{
"key": "lint_format_config",
"name": "Lint / format config",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 11
},
{
"key": "static_type_checking",
"name": "Static type checking",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 11
},
{
"key": "reproducible_environment",
"name": "Reproducible environment",
"detail": "Nix",
"points": 10,
"status": "met",
"details": [
{
"code": "file_list",
"params": {
"files": "Nix"
}
}
],
"max_points": 10
},
{
"key": "demonstrated_agent_practice",
"name": "Demonstrated agent practice",
"detail": "no agent-authored commits among the last 100",
"points": 0,
"status": "missed",
"details": [
{
"code": "no_agent_authored_commits",
"params": {
"sampled": 100
}
}
],
"max_points": 10
},
{
"key": "automated_maintenance",
"name": "Automated maintenance",
"detail": "no automated dependency updates observed",
"points": 0,
"status": "missed",
"details": [
{
"code": "no_dependency_automation",
"params": {}
}
],
"max_points": 8
},
{
"key": "openssf_scorecard_pinned_dependencies",
"name": "OpenSSF Scorecard: Pinned-Dependencies",
"detail": "dependency not pinned by hash detected -- score normalized to 0",
"points": 0,
"status": "missed",
"details": [],
"max_points": 10
}
]
},
{
"key": "ai_code_legibility",
"band": "critical",
"name": "Code legibility for models",
"note": "Excluded from scoring (no data or not applicable): Manageable file sizes. Remaining weights renormalized.",
"notes": [
{
"code": "excluded_no_data",
"params": {
"components": [
"manageable_file_sizes"
]
}
},
{
"code": "weights_renormalized",
"params": {}
}
],
"value": 1,
"inputs": {
"primary_language": "Rocq Prover",
"largest_source_bytes": null,
"source_files_sampled": 0,
"oversized_source_files": 0
},
"components": [
{
"key": "type_checkable_code",
"name": "Type-checkable code",
"detail": "Rocq Prover without a type-check config",
"points": 0,
"status": "missed",
"details": [
{
"code": "no_typecheck_config_language",
"params": {
"language": "Rocq Prover"
}
}
],
"max_points": 45
},
{
"key": "manageable_file_sizes",
"name": "Manageable file sizes",
"detail": "no source files detected",
"points": 0,
"status": "excluded",
"details": [
{
"code": "no_source_files",
"params": {}
}
],
"max_points": 55
}
]
}
],
"description": "How well is the repo equipped to be developed and maintained with AI coding agents? Carries a deliberately small weight: agent tooling is a real maintenance signal, but its absence must never gate the top of the scale (calibration saturates at raw 91, so 100/100 remains reachable with AI Readiness at zero)."
}
],
"classification": {
"labels": [],
"scores": {},
"primary": null,
"evidence": [],
"artifacts": [],
"confidence": "none",
"host_extension": false,
"runs_as_process": false,
"consumed_by_code": false
},
"metrics_version": "2.3.1"
},
"warnings": [
"Star history unavailable: GitHub GraphQL error: Resource not accessible by personal access token"
],
"report_type": "repository",
"generated_at": "2026-07-27T23:55:33.277257Z",
"schema_version": "0.27.0",
"badge_url": "https://raw.githubusercontent.com/inspect-software/badges/main/v1/r/rocq-community/fourcolor.svg",
"full_name": "rocq-community/fourcolor",
"license_state": "custom",
"license_spdx": null
}