Labels Milestones

Search syntax

See the documentation for further details on search, operators, and filters.

"forgejo"

Include only results that match the term in quotes

assignee:<username>

Filter by assigned user

author:<username>

Filter by the author

is:all

All

is:closed

Closed

is:open

Open

mentions:<username>

Filter by mentioned user

modified:[>|<]<date>

Filter by last modified date

review:<username>

Filter by user who reviewed

sort:<by>:[asc|desc]

Sort by: created|comments|updated|deadline

Close

New issue

18 Open 25 Closed 43 All

Label

Show archived labels

All labels No label

blocked

bug

priority!

quick-pick

Milestone

All milestones No milestones

Project

All projects No project

Open projects

Release roadmap

Author

All authors

Assignee

All assignees No assignee

EatOreo marfavi michael

Sort

Relevance Newest Oldest Recently updated Least recently updated Most commented Least commented Nearest due date Farthest due date

18 Open 25 Closed 43 All

Close

Label

Clear labels

blocked

bug

priority!

quick-pick

Milestone

No milestone

Projects

Clear projects

Open projects

Release roadmap

Assignee

Clear assignees

No assignee

EatOreo

marfavi

michael

Confirm to delete all selected items?

Cancel Confirm

when a new model file is generated the proof file needs to be reloaded to realize it

bug

#98 opened 2026-10-30 13:32:50 +01:00 by EatOreo Release roadmap

F2 rename annotation links

#97 opened 2026-10-30 11:14:24 +01:00 by EatOreo Release roadmap

"Rocq model is stale" diagnostic should only apply if there are any crocq annotations in the C file

bug

#95 opened 2026-10-30 10:34:30 +01:00 by EatOreo Release roadmap

Warn when editing a spec/invariant in .v files where the .c file has defined it inline

priority!

#94 opened 2026-10-29 15:26:59 +01:00 by marfavi Release roadmap

Address errors on opening/loading .v files

priority!

#93 opened 2026-10-29 14:56:52 +01:00 by marfavi Release roadmap

Open newly generated proof document so that navigation works instantly

#92 opened 2026-10-29 14:06:59 +01:00 by EatOreo Release roadmap

Fix CI workflow warning about permissions

#91 opened 2026-10-29 13:50:09 +01:00 by marfavi Release roadmap

Add secondary text for which files will be overwritten when forcing creation of proof files

#90 opened 2026-10-29 13:12:58 +01:00 by michael Release roadmap

Publish extension

priority!

#74 opened 2026-10-23 15:47:53 +02:00 by EatOreo Release roadmap 4 / 4

omit the DECLARE line in INLINE_SPEC clauses

quick-pick

1

#70 opened 2026-10-22 14:42:50 +02:00 by EatOreo Release roadmap

code actions for annotation clauses with diagnostics

#67 opened 2026-10-22 09:50:42 +02:00 by EatOreo Release roadmap

Revisit .crocqcache purpose and format

1

#62 opened 2026-10-21 13:43:32 +02:00 by marfavi Release roadmap

we call vsRocqApi.getDocumentProofs() more than necessary

#59 opened 2026-10-21 10:35:53 +02:00 by EatOreo Release roadmap

general code completions

#56 opened 2026-10-16 14:10:53 +02:00 by EatOreo Release roadmap

Expose interpret proof to the command palette

quick-pick

#55 opened 2026-10-16 14:09:17 +02:00 by marfavi Release roadmap

listen to rename of .v files and update annotationStore & crocq annotations

quick-pick

#43 opened 2026-10-15 15:02:50 +02:00 by EatOreo Release roadmap

Show status of proof next to PROOF clause

4

#42 opened 2026-10-15 14:24:18 +02:00 by EatOreo Release roadmap feature/proof-status

code completions suggesting proofs/definitions to link to when writing a PROOF or SPEC clause

blocked

#23 opened 2026-10-09 15:06:57 +02:00 by EatOreo Release roadmap