[hyperpolymath]

Summary

The roadmap record for work order 1.4. Draft: the THY-1 receipts at the new prover versions join this pull request once the first Guix lane runs pass.

Changes

docs/status/ROADMAP.adoc records:

• the proof lanes. CI is wired to check Agda, Rocq and Lean in the pinned Guix shell on every commit, and to assert Agda 2.7.0.1, Rocq 8.18.0 and Lean 4.29.0;
• that the Agda and Lean receipts of THY-1 are earned again at the new versions;
• the two findings: the broken agda-stdlib 2.3 in Guix, and the missing Guix substitute at ae77aeb that led to the pin move.

Testing

Documentation only. The wording says the first lane runs were still going when it was written.

---

Generated by Claude Code

[coderabbitai]

Caution

Review failed

The pull request is closed.

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

Share

• X
• Mastodon
• Reddit
• LinkedIn

[sonarqubecloud]

Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud

[chatgpt-codex-connector]

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.