Show status of proof next to PROOF clause #42

New issue

Open

opened 2026-10-15 14:24:18 +02:00 by EatOreo · 4 comments

EatOreo commented 2026-10-15 14:24:18 +02:00

Owner

• Copy link

No description provided.

EatOreo self-assigned this 2026-10-15 15:56:20 +02:00

marfavi changed title from proof status to Show status of proof next to PROOF clause 2026-10-15 15:56:41 +02:00

marfavi referenced this issue from a pull request that will close it, 2026-10-15 15:57:13 +02:00

WIP: proof-of-concept: show proof status #45

marfavi added reference feature/proof-status 2026-10-16 10:14:53 +02:00

EatOreo commented 2026-10-16 10:50:03 +02:00

Author

Owner

• Copy link
• Copy Markdown

idea showcase at #45

idea showcase at #45

EatOreo added the

blocked

label 2026-10-16 11:04:30 +02:00

EatOreo commented 2026-10-16 11:05:20 +02:00

Author

Owner

• Copy link
• Copy Markdown

blocked by #49 and waiting advice from smart people

blocked by #49 and waiting advice from smart people

EatOreo commented 2026-10-16 12:31:56 +02:00

Author

Owner

• Copy link
• Copy Markdown

think about should we? enforce vsrocq settings:
"vsrocq.proof.block": true
"vsrocq.proof.mode": Manual (we should maybe alert that Continuous mode is experimental)

think about should we? enforce vsrocq settings: "vsrocq.proof.block": true "vsrocq.proof.mode": Manual (we should maybe alert that Continuous mode is experimental)

marfavi added this to the Release roadmap project 2026-10-22 14:51:14 +02:00

marfavi removed the

blocked

label 2026-10-28 10:22:22 +01:00

EatOreo commented 2026-10-28 15:46:23 +01:00

Author

Owner

• Copy link
• Copy Markdown

note that nested proofs give unexpected behaviour! in vsrocq getDocumentProofs

note that nested proofs give unexpected behaviour! in vsrocq getDocumentProofs

Sign in to join this conversation.

feature/proof-status

Branches Tags

Clear current reference

main

release/0.1.0

fix/resync-on-v-rename

feat/infer-inline-declare

feat/grammar-highlighting

feat/clightgen-command-in-status

fix/code-lens-annotation-top

feature/proof-status

fix/inline-clauses-review-findings

Clear current reference

v0.1.0

Labels

Clear labels   

blocked

should wait for another issue to be addressed

  

bug

  

priority!

  

quick-pick

No labels

blocked

bug

priority!

quick-pick

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Release roadmap

Assignees

Clear assignees

No assignees

EatOreo

1 participant

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

code2rocq/crocq#42

No description provided.