Create proof files from templates #28

Merged

marfavi merged 39 commits from feature/create-spec-from-template into main 2026-10-23 15:46:21 +02:00

Conversation 2 Commits 39 Files changed 24 +1417 -66

michael commented 2026-10-14 12:17:36 +02:00

Owner

• Copy link
• Copy Markdown

Adds the Crocq: Create proof files for project command, which scaffolds Verif_<file>.v proof files from templates.

Fixes #27

Adds the `Crocq: Create proof files for project` command, which scaffolds `Verif_<file>.v` proof files from templates. Fixes #27

michael self-assigned this 2026-10-14 12:17:36 +02:00

michael added 11 commits 2026-10-14 12:17:36 +02:00

Added eta (templating engine) dependency and test template bf838aeca0

added command to create proof files (currently just tests the templating works) 1b5c38bbb7

created dependicies for new command 364c03ca2f

Fix F5 debugging window crash (#17) ... 09479ab98e

Reviewed-on: #17
Reviewed-by: EatOreo <[email protected]>
Co-authored-by: Omid Marfavi <[email protected]>
Co-committed-by: Omid Marfavi <[email protected]>

Remove stale out/ before compiling tests (#22) ... 90b87eb09a

* `npm run compile-tests` clears `out/` first so stale test files left behind by other branches are not executed.
* Running tests via the Test Runner panel also clears stale test files.

Reviewed-on: #22
Co-authored-by: Omid Marfavi <[email protected]>
Co-committed-by: Omid Marfavi <[email protected]>

Rename src/commands/dependencies to src/commands/services (#21) ... d20572e091

Pure rename of the VS Code collaborator directory to avoid clashing with the new src/dependencies module. No behaviour change.

Reviewed-on: #21
Reviewed-by: EatOreo <[email protected]>
Co-authored-by: Omid Marfavi <[email protected]>
Co-committed-by: Omid Marfavi <[email protected]>

Quote dynamic values passed to the shell (#20) ... 0a6367063c

Quotes the clightgen file name and the terminal cd target so spaces or metacharacters in a path are not interpreted by the shell.

Reviewed-on: #20
Reviewed-by: EatOreo <[email protected]>
Co-authored-by: marfavi <[email protected]>
Co-committed-by: marfavi <[email protected]>

Add integration tests for Create Rocq Model and deps (#16) ... d24b7fb014

- Cover the command end-to-end via shell integration
- Test the files, logging and terminal dependencies
- Re-create the log output channel after deactivate

fixes #12

Reviewed-on: #16
Reviewed-by: EatOreo <[email protected]>
Reviewed-by: Michael Jeppesen <[email protected]>
Co-authored-by: Omid Marfavi <[email protected]>
Co-committed-by: Omid Marfavi <[email protected]>

Check whether the extension's dependencies are installed (#19) ... 934fa2d166

Adds a src/dependencies module that verifies clightgen and VsRocq on activation, with a status bar chip, dependency panel and settings. Create Rocq Model now gates on the check.

fixes #10

Reviewed-on: #19
Co-authored-by: Omid Marfavi <[email protected]>
Co-committed-by: Omid Marfavi <[email protected]>

added command to create proof files (currently just tests the templating works) 38a1132ca3

created dependicies for new command faa0c7d3bf

michael added 1 commit 2026-10-14 12:18:58 +02:00

fixed errors caused by merge 9f4660eac3

michael added 2 commits 2026-10-14 13:40:54 +02:00

Created general structure for proof templates, still needs some work 79acdd3943

manually create temp data to test templates 0bcd097c6a

michael force-pushed feature/create-spec-from-template from 0bcd097c6a to 9b655d83d6 2026-10-14 13:44:25 +02:00 Compare

michael added 2 commits 2026-10-14 15:10:42 +02:00

Made Gprog array be automatically filled dea1c40431

update template args structure, and make multiple files be generatable at once b7dbff73fb

michael added 5 commits 2026-10-15 14:39:13 +02:00

moved template into a folder together with their interfaces df9b793100

updated path to template folder c7397898bf

Created method for reading annotation store and creating the correct type structure to render the templates 4e17fcb8e7

added utility service method to get the filename without any path or extension from a vscode.Uri 72e7b331d6

changed command to use specific method for creating the type structure for templates 08aee38637

michael force-pushed feature/create-spec-from-template from 08aee38637 to 6c3326dbe7 2026-10-15 14:46:41 +02:00 Compare

michael added 3 commits 2026-10-15 15:21:55 +02:00

added coqproject file to example, as that is required for create proofs command to work with loads 8ee2b72c74

updated template to only allow one file to be loaded 1d618ba951

changed construct proof args with newly merged annotations and template interface structure 0cb9db81f4

michael added 2 commits 2026-10-16 10:53:55 +02:00

Added missing . from load line of proof file cee4388e68

added an uri of where to place the proof files to the template args fd7fb2d37a

michael added 1 commit 2026-10-16 11:11:36 +02:00

minor layout tweaks and improvements 7698c613f3

michael force-pushed feature/create-spec-from-template from 7698c613f3 to 7a229cb9a2 2026-10-16 11:14:58 +02:00 Compare

marfavi changed title from WIP: feature/create-spec-from-template to WIP: Create spec from template 2026-10-16 11:18:03 +02:00

michael added 1 commit 2026-10-16 11:36:18 +02:00

moved files arround 6d1d83889d

michael added 2 commits 2026-10-21 00:35:03 +02:00

Renamed dependicies to services 358e90fd2f

Removed temporary logging and access services correctly 84a0cc6344

michael added 1 commit 2026-10-21 00:39:32 +02:00

Created some tests, might need change as it requires vscode dependencies a93cd8fb51

michael added 1 commit 2026-10-21 10:37:46 +02:00

Added comment to fix tests 916c4c0e77

michael added 1 commit 2026-10-21 13:02:45 +02:00

Added optional argument to createProofFile to specify which file to generate f56d3ccf14

michael force-pushed feature/create-spec-from-template from f56d3ccf14 to 454502c7ae 2026-10-21 13:04:02 +02:00 Compare

michael added 1 commit 2026-10-21 13:08:57 +02:00

Added note about buggy behavior 9968b41607

marfavi self-assigned this 2026-10-21 13:46:50 +02:00

marfavi commented 2026-10-21 13:47:05 +02:00

Owner

• Copy link
• Copy Markdown

Fix #27

Fix #27

marfavi added 7 commits 2026-10-21 14:08:05 +02:00

fix(extension): stop contributing duplicate commands ... b149802d42

crocq.checkDependencies, crocq.openDependencyPanel and crocq.createProofFiles
were each declared twice in contributes.commands, a leftover of the merge with
main. Keep one entry per command.

fix(templates): ship the proof templates with the extension ... 1737b92775

The .eta templates lived under src/templates, which .vscodeignore excludes from
the packaged extension (src/**); esbuild does not copy them either. A packaged
build therefore had no templates to render.

Move them to templates/ at the extension root and point the command at that
directory. spec.eta also notes that its funspec arguments are placeholders.

fix(services): reliable file helpers and on-disk annotation parsing ... f466393501

- fileNameFromUri parses Uri.fsPath with node:path instead of splitting
  uri.toString(), which mishandled percent-encoded names and queries.
- getCFilesInWorkspace uses try/catch (findFiles rejects when no folder is
  open) and logs the failure instead of swallowing it.
- Add fileExists, and make writeFile create missing parent directories.
- Add readFileAnnotations, which parses a C file from disk whether or not it
  is open. The document sync only stores annotations of open documents.
- Add showWarningMessage.

refactor(createProofFiles): generate safely from all C files ... 3d15b19d99

- Inject the vscode-facing services (same convention as createRocqModel) so
  the command and the annotation-to-template mapping are unit testable without
  an extension host. The unit tests previously failed to load because they
  imported vscode.
- Read the annotations of every C file from disk instead of opening all of
  them and hoping the asynchronous onDidOpenTextDocument listener had filled
  the store by then. This removes the empty/stale-store race (and the note
  about proofs for deleted files).
- Never overwrite an existing proof file; skip it and warn instead. The old
  code overwrote Verif_*.v on every run, destroying user proofs.
- Match the optional file argument on path boundaries instead of endsWith, and
  name the "all" argument.
- Report failures instead of rejecting: aggregated, de-duplicated annotation
  errors, per-file read resilience, and an information message when there is
  nothing to generate.
- Drop triggerOnDocumentOpen, which the command no longer uses, and move the
  proof file's uri out of the template arguments (it is not a template input).

test(integration): cover templates, command contributions and file helpers ... d33fc4fba1

- Assert that package.json contributes each command exactly once, guarding the
  duplicate-command merge artifact.
- Assert that the verif/spec/proof templates ship where the command looks for
  them.
- Cover fileNameFromUri, fileExists, writeFile (including parent-directory
  creation) and getTargetUriAndSpec against real vscode URIs.

docs: document the Create proof files command ... 9fad54f72e

Describe what it scaffolds, that it never overwrites existing documents, and
that the generated funspec arguments are placeholders until deriving a VST
funspec from the C source is implemented.

chore(examples): end _CoqProject with a newline 1796da2e71

marfavi changed title from WIP: Create spec from template to Create proof files from templates 2026-10-21 14:08:06 +02:00

marfavi changed title from Create proof files from templates to WIP: Create proof files from templates 2026-10-21 14:14:50 +02:00

marfavi force-pushed feature/create-spec-from-template from 1796da2e71 to 9968b41607 2026-10-21 14:18:43 +02:00 Compare

michael added 4 commits 2026-10-21 14:44:17 +02:00

Add template for loop invariants cc73ba1e29

update proof file template to alse generate loop invariants a3767c9638

Rename function to more relevant name 98c8cdd96e

Add generation of loop invariant template from loop annotations 22a053a523

marfavi added 1 commit 2026-10-23 13:47:16 +02:00

branch suggestion: create proof files from template (#63) ... e893dc7731

Co-authored-by: Michael Jeppesen <[email protected]>
Reviewed-on: #63
Reviewed-by: Michael Jeppesen <[email protected]>
Co-authored-by: Omid Marfavi <[email protected]>
Co-committed-by: Omid Marfavi <[email protected]>

marfavi changed title from WIP: Create proof files from templates to Create proof files from templates 2026-10-23 13:47:38 +02:00

marfavi added 1 commit 2026-10-23 13:47:59 +02:00

Merge branch 'main' into feature/create-spec-from-template d32cf84aae

michael force-pushed feature/create-spec-from-template from d32cf84aae to e3a5e356bf 2026-10-23 15:16:56 +02:00 Compare

michael added 1 commit 2026-10-23 15:18:45 +02:00

Removed non existing command from merge dc2c746240

michael added 1 commit 2026-10-23 15:25:33 +02:00

fixed duplicated commands being registered b59634a13f

michael added 1 commit 2026-10-23 15:28:50 +02:00

formatting 5553fdb070

marfavi added 1 commit 2026-10-23 15:38:49 +02:00

Remove command for opening dependency panel from package.json f531a0a45a

marfavi scheduled this pull request to auto merge when all checks succeed 2026-10-23 15:40:53 +02:00

marfavi added 1 commit 2026-10-23 15:43:04 +02:00

Rename _CoqProject -> _RocqProject d1eff1c6c4

marfavi approved these changes 2026-10-23 15:46:18 +02:00

marfavi merged commit ea1e103328 into main 2026-10-23 15:46:21 +02:00

marfavi deleted branch feature/create-spec-from-template 2026-10-23 15:46:21 +02:00

marfavi referenced this pull request from a commit 2026-10-23 15:46:21 +02:00

Create proof files from templates (#28)

marfavi referenced this pull request from a commit 2026-10-23 16:01:29 +02:00

Merge remote-tracking branch 'origin/main' into proof-of-concept/inline-clauses

Sign in to join this conversation.

Reviewers

No reviewers

marfavi

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

michael

marfavi

2 participants

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!28

No description provided.