Owner

rocq-prover

8 indexed repositories · View on GitHub

vsrocq
Visual Studio Code extension for Rocq

Rocq Prover · 461 stars
platform
Multi platform setup for Rocq, Rocq libraries and tools

Shell · 247 stars
equations
A function definition package for Rocq

Rocq Prover · 236 stars
opam
Archive for all Rocq and Coq-related opam packages organized in various repositories

OCaml · 173 stars
stdlib
Stdlib for the Rocq Prover

Rocq Prover · 42 stars
bot
The Rocq Prover bot

OCaml · 30 stars
platform-docs
A project of short tutorials and how-to guides for Coq features and Coq Platform packages.

Rocq Prover · 26 stars
rocq-prover.org
The Rocq Prover Website

HTML · 15 stars

Beginner friendly Everything

Open All

Inconsistency with uniform parameter subtyping Open

kind: bug kind: inconsistency needs: triage part: inductives part: modules

Difficulty 4/5 3-5 days Newbie friendliness 35/100

rocq-prover/rocq#22510 · Opened Sep 19, 2026
Difference to fixpoints in catch-all/default branches leading to guard checker problems Open

Difficulty 4/5 3-5 days Newbie friendliness 48/100

rocq-prover/equations#742 · Opened Sep 18, 2026
Anomaly during inductive subtyping check Open

kind: anomaly part: inductives part: modules

Difficulty 4/5 3-5 days Newbie friendliness 30/100

rocq-prover/rocq#22498 · Opened Sep 17, 2026
Only-printing notation changes precedence of a later parsing rule Open

kind: bug needs: triage

Difficulty 3/5 1-2 days Newbie friendliness 68/100

rocq-prover/rocq#22496 · Opened Sep 17, 2026
Specify that Intel Macs require installing from source Open

Difficulty 1/5 Under an hour Newbie friendliness 90/100

rocq-prover/platform#537 · 1 comment · 1 reaction · Opened Sep 16, 2026
Assertion failure in mod_subst Open

kind: anomaly part: modules

Difficulty 4/5 3-5 days Newbie friendliness 48/100

rocq-prover/rocq#22482 · 1 comment · Opened Sep 16, 2026
[FEAT] Extend `textDocument/selectionRange` to be AST aware Open

enhancement

Difficulty 4/5 3-5 days Newbie friendliness 45/100

rocq-prover/vsrocq#1323 · 1 comment · Opened Sep 16, 2026
documentation of install buildtools for Fedora Open

Difficulty 1/5 Under an hour Newbie friendliness 92/100

rocq-prover/platform#536 · 1 comment · 1 reaction · Opened Sep 14, 2026
RocqIDE external command defaults still use compatibility Coq binaries Open

Difficulty 2/5 1-3 hours Newbie friendliness 76/100

rocq-prover/rocq#22473 · Opened Sep 12, 2026
Primitive operations in the VM do not work well with module aliasing Open

part: modules part: VM

Difficulty 4/5 3-5 days Newbie friendliness 48/100

rocq-prover/rocq#22470 · Opened Sep 10, 2026
timelog2html incorrectly considers preceding character as part of a command Open

kind: bug

Difficulty 3/5 1-2 days Newbie friendliness 65/100

rocq-prover/rocq#22467 · Opened Sep 10, 2026
Register Inline is not saved to the .vo, so it has no effect in files that Require the defining one Open

Difficulty 4/5 3-5 days Newbie friendliness 65/100

rocq-prover/rocq#22460 · Opened Sep 9, 2026
Clarify extraction correctness for strict let-bindings and exception-raising external functions Open

Difficulty 4/5 3-5 days Newbie friendliness 48/100

rocq-prover/rocq#22450 · 3 comments · 1 reaction · Opened Sep 9, 2026
Anomaly "Missing VM index" when vm_compute reaches a constant of a module sealed with "with Definition" Open

Difficulty 4/5 3-5 days Newbie friendliness 58/100

rocq-prover/rocq#22449 · Opened Sep 8, 2026
Anomaly "Uncaught exception Failure("List.chop")." when parsing notation. Open

kind: bug needs: triage

Difficulty 4/5 3-5 days Newbie friendliness 55/100

rocq-prover/rocq#22448 · Opened Sep 8, 2026
Add an option for per-file lia caching Open

kind: performance kind: wish part: micromega

Difficulty 4/5 3-5 days Newbie friendliness 48/100

rocq-prover/rocq#22440 · Opened Sep 4, 2026
What would it take for a Vernacstate.t to be transportable between directories or machines? Open

Difficulty 5/5 Over a week Newbie friendliness 30/100

rocq-prover/rocq#22432 · 2 comments · Opened Sep 1, 2026
-async-proofs on: coqc exits 0 and writes a consumable .vo for an ill-typed file Open

kind: bug part: STM

Difficulty 3/5 1-2 days Newbie friendliness 35/100

rocq-prover/rocq#22422 · Opened Aug 29, 2026
Large inclusion of modules is slow due to Libobject expansion Open

kind: performance part: libobject part: modules

Difficulty 4/5 3-5 days Newbie friendliness 42/100

rocq-prover/rocq#22420 · Opened Aug 29, 2026
Anomaly Bad occurrence of recursive call. (with `fix` tactic) Open

kind: anomaly part: fixpoints

Difficulty 3/5 1-2 days Newbie friendliness 65/100

rocq-prover/rocq#22417 · Opened Aug 28, 2026
[BUG] Server republishes diagnostics on every sentence (performance issue) Open

bug

Difficulty 3/5 1-2 days Newbie friendliness 52/100

rocq-prover/vsrocq#1311 · 2 comments · Opened Aug 28, 2026
Bug in `=` mode, or the mode is less useful than expected Open

kind: bug needs: triage

Difficulty 4/5 3-5 days Newbie friendliness 48/100

rocq-prover/rocq#22414 · 17 comments · Opened Aug 28, 2026
Explicit argument is being shadowed by implicit argument Open

Difficulty 3/5 1-2 days Newbie friendliness 55/100

rocq-prover/equations#741 · Opened Aug 27, 2026
RocqIDE executes attacker code on file open by applying an ancestor-directory _RocqProject that injects -l into the coqidetop argv Open

Difficulty 4/5 3-5 days Newbie friendliness 48/100

rocq-prover/rocq#22406 · Opened Aug 26, 2026
Unvalidated bytecode operand counts in rocq_tcode_of_code cause an attacker-length heap buffer overflow when loading a crafted .vo Open

kind: kernel segfault/exploit

Difficulty 4/5 3-5 days Newbie friendliness 48/100

rocq-prover/rocq#22405 · 4 comments · Opened Aug 26, 2026
About the kernel's data structures for renamings and substitutions Open

kind: wish needs: triage

Difficulty 5/5 Over a week Newbie friendliness 25/100

rocq-prover/rocq#22403 · 1 comment · Opened Aug 25, 2026
Unexpected Behavior from `rewrite_strat` when moving terms in and out of binders Open

kind: bug needs: triage

Difficulty 4/5 3-5 days Newbie friendliness 45/100

rocq-prover/rocq#22397 · Opened Aug 21, 2026
`-async-proofs on` silently swallows universe-constraint errors (exit 0, `.vo` silently missing the failed definition) Open

kind: bug needs: triage

Difficulty 4/5 3-5 days Newbie friendliness 52/100

rocq-prover/rocq#22367 · Opened Aug 19, 2026
`Unset Guard Checking` leaks through functor application with `Parameter Inline`: `False` accepted with `Print Assumptions` reporting "Closed under the global context" Open

kind: bug

Difficulty 5/5 Over a week Newbie friendliness 32/100

rocq-prover/rocq#22366 · 1 comment · Opened Aug 19, 2026
Nested Eliminators Open

kind: wish needs: triage

Difficulty 5/5 Over a week Newbie friendliness 45/100

rocq-prover/rocq#22344 · 1 reaction · Opened Aug 12, 2026
Cannot scroll on sidebar Open

Difficulty 3/5 1-2 days Newbie friendliness 58/100

rocq-prover/rocq-prover.org#268 · Opened Aug 12, 2026
When universes are printed, cannot accept the print of an inductive Open

kind: bug needs: triage part: printer

Difficulty 3/5 1-2 days Newbie friendliness 48/100

rocq-prover/rocq#22343 · Opened Aug 11, 2026
Module ascription rejected when a component's type names a sibling module directly instead of through its alias Open

kind: question part: modules

Difficulty 4/5 3-5 days Newbie friendliness 45/100

rocq-prover/rocq#22333 · 1 comment · Opened Aug 6, 2026
Anomaly unknown level with ltac2 notation Open

kind: bug part: ltac2

Difficulty 3/5 1-2 days Newbie friendliness 50/100

rocq-prover/rocq#22330 · Opened Aug 3, 2026
Bidirectional hints change program obligation order in unexpected ways Open

kind: bug needs: triage

Difficulty 4/5 3-5 days Newbie friendliness 48/100

rocq-prover/rocq#22328 · Opened Jul 31, 2026
(auto)rewrite* fails where (auto)rewrite succeeds Open

kind: bug needs: triage

Difficulty 4/5 3-5 days Newbie friendliness 48/100

rocq-prover/rocq#22323 · 4 comments · Opened Jul 29, 2026
[release] for Rocq 9.3.0 Open

Difficulty 4/5 3-5 days Newbie friendliness 25/100

rocq-prover/vsrocq#1291 · 2 comments · Opened Jul 28, 2026
Dependent Elimination is not compatible with Set Mangle Names Open

Difficulty 4/5 3-5 days Newbie friendliness 50/100

rocq-prover/equations#733 · Opened Jul 25, 2026
`vsrocq-language-server` installation fails on OCaml 5.5 Open

Difficulty 3/5 1-2 days Newbie friendliness 55/100

rocq-prover/vsrocq#1287 · 2 comments · Opened Jul 24, 2026
Compilation of critical bugs in stable releases of Coq: add a table Open

kind: wish needs: triage

Difficulty 2/5 1-3 hours Newbie friendliness 68/100

rocq-prover/rocq#22301 · 1 comment · Opened Jul 23, 2026
Remove "vsrocq.proof.delegation" Open

Difficulty 2/5 1-3 hours Newbie friendliness 64/100

rocq-prover/vsrocq#1286 · 1 comment · Opened Jul 21, 2026
The link in repo description is invalid Open

Difficulty 2/5 1-3 hours Newbie friendliness 68/100

rocq-prover/equations#731 · Opened Jul 21, 2026
Universe checking state gets confused when locally changed in module Open

kind: inconsistency part: modules part: universes

Difficulty 3/5 1-2 days Newbie friendliness 48/100

rocq-prover/rocq#22287 · Opened Jul 16, 2026
Chaining module `<+` operator shows quadratic time increase Open

kind: performance part: modules

Difficulty 4/5 3-5 days Newbie friendliness 42/100

rocq-prover/rocq#22279 · 3 comments · Opened Jul 16, 2026
Maintaining NaryFunctions Open

Difficulty 5/5 Over a week Newbie friendliness 25/100

rocq-prover/stdlib#293 · Opened Jul 15, 2026
Rewrite fails to rewrite a list of functions while setoid_rewrite succeeds Open

kind: bug needs: triage

Difficulty 4/5 3-5 days Newbie friendliness 42/100

rocq-prover/rocq#22269 · 2 comments · Opened Jul 12, 2026
Typeclass resolution regression from #22037: goals with no applicable hint fail eagerly, losing solutions found via later unifications (breaks fiat-crypto) Open

Difficulty 4/5 3-5 days Newbie friendliness 45/100

rocq-prover/rocq#22227 · 2 comments · Opened Jul 7, 2026
Autogeneration of transitivity lemma preempts setoid even when it fails Open

kind: bug part: tactics

Difficulty 3/5 1-2 days Newbie friendliness 68/100

rocq-prover/rocq#22224 · Opened Jul 7, 2026
Record `with` syntax that forces the record value Open

kind: wish

Difficulty 5/5 Over a week Newbie friendliness 35/100

rocq-prover/rocq#22222 · Opened Jul 7, 2026
Preterm construction should be referentially transparent Open

kind: bug kind: wish part: elaboration part: ltac2

Difficulty 5/5 Over a week Newbie friendliness 45/100

rocq-prover/rocq#22219 · Opened Jul 6, 2026

Showing the newest 100

This page lists what was indexed most recently. Advanced filter has the whole inventory, narrowed by language, difficulty and how long a task takes.

Open advanced filter

rocq-prover

Showing the newest 100

Get new issues in your inbox