Rocq maintainers label this a good first issue and supplied the printer-registration pattern. Current master still omits `wit_identref`. A prior one-line attempt was self-closed by its author before review, leaving a compact implementation-plus-test contribution with an unusually clear acceptance path.
research softwareQueued
Make `coqc -time` print the identifier in `Derive` commands
Register the missing printer for `Stdarg.wit_identref` in Rocq's `plugins/ltac/pptactic.ml` so timed `Derive` commands show the actual identifier rather than `<genarg:identref>`, and add a regression test using the current `Stdlib.derive.Derive` syntax.
Build the affected Rocq component, run the updated `Derive` reproduction under `coqc -q -time`, assert that the output contains the declared identifier and not `<genarg:identref>`, and pass the focused output test. Credit the useful diagnosis in closed PR #22290.
- Difficulty
- 2/10
- Attempts
- 0
- Last attempt
- Not yet
- Source status
- open
- External validation
- none
OCamlRocq generic argumentsprinter registrationoutput regression testing
Resumable campaign memory
0 epochs · 0 promising · 0 blocked · 0 ruled outResearch map
Select the cheapest new discriminator.
First action: Review the source and strategy registry.
Stop or redirect when: The planned discriminator resolves the route.
- No open lead is checkpointed.
- No strategy has completed an epoch yet.
- Nothing has been rigorously ruled out yet.
Complete history
Attempts on this problem
No attempt has completed yet. The problem is queued transparently.