code2rocq/imp2rocq
Archived
Watch
3
0
Fork
You've already forked imp2rocq
 0
Code Issues 25 Pull requests Projects 2 Wiki Activity

Keeping track of correlated pieces of code in annotations and generated Rocq files #14

Open
opened 2026-03-12 15:21:10 +01:00 by EatOreo · 0 comments
EatOreo commented 2026-03-12 15:21:10 +01:00
Owner

So in our generated proof skeleton, some lines/strings correlate exactly to a string in our Imp annotations/comments. Initially they will be exactly the same. We need some smart system/data structure to keep track of pieces of the generated file that depends on the Imp comment for keeping them in sync. And vice versa we need to be able to translate back from the proof skeleton to the position in the comment for propagating diagnostics from the vsrocq lsp.

So in our generated proof skeleton, some lines/strings correlate exactly to a string in our Imp annotations/comments. Initially they will be exactly the same. We need some smart system/data structure to keep track of pieces of the generated file that depends on the Imp comment for keeping them in sync. And vice versa we need to be able to translate back from the proof skeleton to the position in the comment for propagating diagnostics from the vsrocq lsp.
EatOreo added this to the Kanban project 2026-03-12 15:21:10 +01:00
Commenting is not possible because the repository is archived.
No Branch/Tag specified
Branches Tags
main
report
refactor-documents
parser
No results found.
Labels
Clear labels
No items
No labels
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Kanban
Assignees
Clear assignees
No assignees
1 participant
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Blocks
#13 Complete code lenses to jump to proofs
code2rocq/imp2rocq
Reference
code2rocq/imp2rocq#14
No description provided.