Bug 2445873 - Review Request: rocq - Proof management system
Summary: Review Request: rocq - Proof management system
Keywords:
Status: NEW
Alias: None
Product: Fedora
Classification: Fedora
Component: Package Review
Version: rawhide
Hardware: All
OS: Linux
medium
medium
Target Milestone: ---
Assignee: Nobody's working on this, feel free to take it
QA Contact: Fedora Extras Quality Assurance
URL:
Whiteboard:
Depends On:
Blocks: 2445874
TreeView+ depends on / blocked
 
Reported: 2026-03-09 21:34 UTC by Jerry James
Modified: 2026-03-09 21:54 UTC (History)
1 user (show)

Fixed In Version:
Clone Of:
Environment:
Last Closed:
Type: ---
Embargoed:


Attachments (Terms of Use)

Description Jerry James 2026-03-09 21:34:00 UTC
Spec URL: https://jjames.fedorapeople.org/rocq/rocq.spec
SRPM URL: https://jjames.fedorapeople.org/rocq/rocq-9.1.1-1.fc45.src.rpm
Fedora Account System Username: jjames
Description: This is a rename request.  The current package name is coq.

Rocq is a formal proof management system.  It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, or the Bedrock verified low-level programming library), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching.

Test builds for (and using) this package have been done in a COPR: https://copr.fedorainfracloud.org/coprs/jjames/Rocq9/builds/.

I am willing to swap reviews.

Comment 1 Fedora Review Service 2026-03-09 21:54:31 UTC
Copr build:
https://copr.fedorainfracloud.org/coprs/build/10205104
(succeeded)

Review template:
https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-review-2445873-rocq/fedora-rawhide-x86_64/10205104-rocq/fedora-review/review.txt

Please take a look if any issues were found.


---
This comment was created by the fedora-review-service
https://github.com/FrostyX/fedora-review-service

If you want to trigger a new Copr build, add a comment containing new
Spec and SRPM URLs or [fedora-review-service-build] string.


Note You need to log in before you can comment on or make changes to this bug.