code2rocq/crocq
code2rocq/crocq
Watch
3
2
Fork
You've already forked crocq
 0
Code Issues 18 Pull requests 3 Projects 1 Releases 1 Packages 2 Activity Actions

Add stale model validation, diagnostics and .crocqcache #60

Merged
marfavi merged 7 commits from feat/invalidate-stale-model into main 2026-10-23 14:54:57 +02:00
Conversation 2 Commits 7 Files changed 53 +3812 -1043
marfavi commented 2026-10-21 12:39:58 +02:00
Owner

Track the program hash a generated model was built from in a workspace .crocqcache, show a stale-model diagnostic/code lens and offer regeneration through the existing Create Rocq model command.

New command: "Toggle auto-generation of Rocq model on save". Saves setting to .crocqcache and applies to the folder.

Fix #46

Track the program hash a generated model was built from in a workspace .crocqcache, show a stale-model diagnostic/code lens and offer regeneration through the existing Create Rocq model command. New command: "Toggle auto-generation of Rocq model on save". Saves setting to .crocqcache and applies to the folder. Fix #46
Add stale model validation, diagnostics and .crocqcache
Some checks failed
Grammar / Corpus and binding tests (pull_request) Successful in 44s
Details
Extension / Format, types, lint, extension tests (pull_request) Failing after 2m9s
Details
5ceda6aa1d
 
Track the program hash a generated model was built from in a workspace .crocqcache, show a stale-model diagnostic/code lens and offer regeneration through the existing Create Rocq model command.
marfavi changed title from WIP: Show warning when C file and corresponding Rocq model are out of sync to WIP: Add stale model validation, diagnostics and .crocqcache 2026-10-21 12:45:56 +02:00
Expose auto-generation on save through the command palette
Some checks failed
Grammar / Corpus and binding tests (pull_request) Successful in 43s
Details
Extension / Format, types, lint, extension tests (pull_request) Failing after 1m50s
Details
67460f0efe
 
Contribute and register crocq.toggleAutoGenerateModelOnSave, and regenerate on save when the .crocqcache flag is enabled.
Persist failed model generations and surface them
Some checks failed
Grammar / Corpus and binding tests (pull_request) Successful in 42s
Details
Extension / Format, types, lint, extension tests (pull_request) Failing after 1m33s
Details
6fdf597e0d
 
Await the clightgen exit status, record the literal failed marker in .crocqcache when it fails, and keep the first-character stale diagnostic and lens visible through retries until a generation succeeds.
Wait for the interpret lens in the code lens test
All checks were successful
Grammar / Corpus and binding tests (pull_request) Successful in 42s
Details
Extension / Format, types, lint, extension tests (pull_request) Successful in 1m33s
Details
9e5c4620df
 
The stale lens is available immediately and satisfied the old readiness check before the asynchronous proof lookup had produced the interpret lens, making the assertion race on CI.
marfavi changed title from WIP: Add stale model validation, diagnostics and .crocqcache to Add stale model validation, diagnostics and .crocqcache 2026-10-21 13:35:55 +02:00
EatOreo requested changes 2026-10-22 10:30:16 +02:00
Dismissed
extension/src/extension.ts Outdated
@ -57,0 +82,4 @@
// stale warning while clightgen is running. A failed attempt is persisted
// as the cache's "failed" marker, which keeps the warning visible until a
// later attempt succeeds.
const createRocqModel = async (targetPath?: ParsedPath): Promise<void> => {
EatOreo commented 2026-10-21 14:48:49 +02:00
Owner

does this belong in extension.ts?

does this belong in extension.ts?
marfavi commented 2026-10-22 15:01:27 +02:00
Author
Owner

See !60 (commit 74a66f097e)

See https://git.marfavi.com/code2rocq/crocq/pulls/60/commits/74a66f097edc05f51b96a080a405cb45ac1f715d
EatOreo marked this conversation as resolved
refactor(createRocqModel): own generation tracking in the command
All checks were successful
Grammar / Corpus and binding tests (pull_request) Successful in 45s
Details
Extension / Format, types, lint, extension tests (pull_request) Successful in 2m48s
Details
74a66f097e
 
Move the begin/failure/done bookkeeping out of extension.ts, as raised in review. The handler now brackets the attempt itself; extension.ts only injects the model-validity store and the file-URI mapping.
EatOreo approved these changes 2026-10-22 15:24:49 +02:00
Add status bar modules and primary-side-bar status view (#61)
All checks were successful
Grammar / Corpus and binding tests (pull_request) Successful in 5m22s
Details
Extension / Format, types, lint, extension tests (pull_request) Successful in 6m59s
Details
cb2045aa55 
Moves Crocq's status UI to a primary-side-bar view and replaces the dependency-only status bar chip and floating popover.

- Adds attachable status modules for dependencies and the active C file's model.
- Adds a `Crocq` activity-bar container with a `Status` webview view, and makes the status bar chip focus it.
- Includes the auto-generation-on-save toggle in the status view.
- Removes the old dependency status bar, popup panel and their tests.
- Retains the stale-model behavior from the base branch, including the persisted `"failed"` generation state.
- Merges the old crocq dependencies view into the sidebar.

Reviewed-on: #61
Reviewed-by: EatOreo <[email protected]>
Co-authored-by: Omid Marfavi <[email protected]>
Co-committed-by: Omid Marfavi <[email protected]>
Merge branch 'main' into feat/invalidate-stale-model
All checks were successful
Grammar / Corpus and binding tests (pull_request) Successful in 57s
Details
Extension / Format, types, lint, extension tests (pull_request) Successful in 2m1s
Details
8a211e030e
marfavi scheduled this pull request to auto merge when all checks succeed 2026-10-23 14:53:06 +02:00
marfavi deleted branch feat/invalidate-stale-model 2026-10-23 14:54:58 +02:00
Sign in to join this conversation.
Reviewers
No reviewers
EatOreo
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
Assignees
Clear assignees
No assignees
2 participants
Notifications
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!60
No description provided.