Collaborative project to add docstrings to MathComp.

All informations are updated once every 15 minutes

Want more details? Jump to progress to see section-by-section status.

LLM4Docq is a collaborative research project with three main objectives:

1. Docstring enrichment for MathComp:
   We aim to add detailed docstrings to all elements of the MathComp library:

   • Definitions: 3,067
   • Lemmas: 14,925
   • Notations: 3,386
   • Theorems: 61
   • Facts: 654
   • Fixpoints: 140
   • Records: 256

2. Embedding-based retrieval system:
   A VSCode plugin for Rocq users, enabling retrieval from natural language query.

3. Annotator–formalizer models:

   • Generate a docstring from a formal statement and its context.
   • Reconstruct a formal statement from a docstring and context.

To gather the underlying dataset, we use an iterative process:

1. LLMs generate initial docstrings.
2. Experts review and give feedback on a subpart of the generated docstrings.
3. Unseen or refused entries are regenerated with new instructions based on previous feedback.

1. Request access to join the project. You can reach me on rocq zulip (Théo Stoskopf).
2. Pick a source file:
   Each file is managed as a separate project in our collaborative platform (Label Studio). Find one in the project hierarchy below.
3. Annotate entries.

• Annotate (required):
  Review the proposed docstring and select its status:

  • Acceptable: The docstring is correct and sufficiently detailed.
  • Needs Improvement: The docstring is mostly correct but could be clearer or more precise.
  • Incorrect: The docstring is wrong or irrelevant.

• Suggest an improved version:
  If the annotation is "Needs Improvement" or "Incorrect", provide a better docstring.

• Add comments:
  Share additional feedback, clarifications, or suggestions for future improvements.

• Skip:
  If you are unsure how to annotate the entry, you can skip it.

• Submit:
  Submit your review once you have finished annotating or commenting.

See below for some examples:

The docstring is correct and complete. Select "Acceptable" and submit.

The docstring is mostly correct, but could be improved or clarified. Select "Needs Improvement”, suggest a better version and leave a comment.

The docstring is incorrect or unrelated to the code. Select "Incorrect" and provide a corrected version and comment.

Below is the overall hierarchy. To contribute, click on a source file in an expandable section.