branch suggestion: create proof files from template #63

marfavi · 2026-10-21T14:20:01+02:00

marfavi commented

2026-10-21 14:20:01 +02:00

Suggestion branch for feature/create-spec-from-template.

What it does

Generates one verif_<file>.v per C file with annotations from the verif/spec/loop/proof templates.
Reads annotations from disk instead of the shared annotation store, so it does not depend on the document sync or on VsRocq being ready.
Never overwrites existing proof files (see #65).
Honours PROOF links: the lemma keeps the linked name, and a proof linked to another document is generated in that document rather than beside the spec.
Keeps the templates in src/templates and ships them through a .vscodeignore exception.

Why the command layer was restructured

The old flow opened every C file and then read the shared store, which is filled asynchronously and only while VsRocq is available: it could run against an empty store, and closing/deleting files left stale entries behind.
The vscode-facing helpers are injected (as in createRocqModel) so the command and the annotation mapping can run in npm run test:unit; before, the unit test failed to load (MODULE_NOT_FOUND: vscode).

Known limitations

The generated specs and loop invariants are placeholders; deriving a VST funspec/invariant from C is not implemented, so the generated file does not compile until they are filled in (see #27).
A PROOF link pointing at a document that does not exist generates a proof-only document; that file references a spec defined elsewhere and will not compile on its own.

npm run check, npm run test:unit and npm run test:integration pass.

Suggestion branch for `feature/create-spec-from-template`. ## What it does - Generates one `verif_<file>.v` per C file with annotations from the `verif`/`spec`/`loop`/`proof` templates. - Reads annotations from disk instead of the shared annotation store, so it does not depend on the document sync or on VsRocq being ready. - Never overwrites existing proof files (see #65). - Honours `PROOF` links: the lemma keeps the linked name, and a proof linked to another document is generated in that document rather than beside the spec. - Keeps the templates in `src/templates` and ships them through a `.vscodeignore` exception. ## Why the command layer was restructured - The old flow opened every C file and then read the shared store, which is filled asynchronously and only while VsRocq is available: it could run against an empty store, and closing/deleting files left stale entries behind. - The vscode-facing helpers are injected (as in `createRocqModel`) so the command and the annotation mapping can run in `npm run test:unit`; before, the unit test failed to load (`MODULE_NOT_FOUND: vscode`). ## Known limitations - The generated specs and loop invariants are placeholders; deriving a VST funspec/invariant from C is not implemented, so the generated file does not compile until they are filled in (see #27). - A `PROOF` link pointing at a document that does not exist generates a proof-only document; that file references a spec defined elsewhere and will not compile on its own. `npm run check`, `npm run test:unit` and `npm run test:integration` pass.

marfavi added 7 commits

2026-10-21 14:20:01 +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

Grammar / Corpus and binding tests (pull_request) Successful in 43s

Details

Extension / Format, types, lint, extension tests (pull_request) Successful in 1m36s

Details

1796da2e71

marfavi force-pushed fix/create-proof-files from 1796da2e71

Grammar / Corpus and binding tests (pull_request) Successful in 43s

Details

Extension / Format, types, lint, extension tests (pull_request) Successful in 1m36s

Details

to 9d5e44b110

Grammar / Corpus and binding tests (pull_request) Successful in 44s

Details

Extension / Format, types, lint, extension tests (pull_request) Successful in 1m43s

Details

2026-10-21 14:37:32 +02:00

Compare

marfavi added 1 commit

2026-10-21 14:55:03 +02:00

Merge branch 'feature/create-spec-from-template' into fix/create-proof-files

Grammar / Corpus and binding tests (pull_request) Successful in 44s

Details

Extension / Format, types, lint, extension tests (pull_request) Successful in 1m40s

Details

6cbcf2d1c2

marfavi added 2 commits

2026-10-21 15:50:54 +02:00

feat(createProofFiles): honour PROOF links when generating proofs b792c88962

- A function whose PROOF clause points at the document that receives its spec
  keeps generating the lemma, now under the lemma name from the clause instead
  of the hard-coded body_<fn>.
- When the PROOF clause points at another document, only the spec is generated
  here: the linked proof already lives there, so generating the lemma again
  would duplicate it.

docs(createProofFiles): spell out placeholder bodies and skip-only policy

Grammar / Corpus and binding tests (pull_request) Successful in 40s

Details

Extension / Format, types, lint, extension tests (pull_request) Successful in 1m32s

Details

21bc88769d

The generated specs and loop invariants are intentionally placeholders until
deriving a VST funspec/invariant from C lands (#27); note it in loop.eta, as
spec.eta already does, and in the README. Also document that existing proof
files are never overwritten and link the force-option issue (#65).

michael added 5 commits

2026-10-22 14:29:06 +02:00

added missing . after Gprog definition in template 4a1f23e0a8

changed default args so that the generated rocq files can be interpeted 3ca9e8de0d

Changed default proof file name to be verif_ with lower case fd86db6fe6

Fixed test failing from change to template 581f89a14f

Changed constructProofArgs to be a mix of the two branches

Extension / Format, types, lint, extension tests (pull_request) Failing after 1m18s

Details

Grammar / Corpus and binding tests (pull_request) Successful in 52s

Details

5e49f2bc99

marfavi added 2 commits

2026-10-22 14:39:37 +02:00

fix(createProofFiles): keep a proof with its spec when there is no PROOF link 50faa91c59

resolveTarget(null) resolves the default document; it does not return
undefined. The "no proof target" branch was therefore dead: a function with
a SPEC link and no PROOF link had its proof generated in a second
verif_<file>.v document instead of next to its spec, and the proof name fell
back to the spec name.

Only resolve a proof target when the PROOF clause exists; otherwise the proof
stays with the spec target and keeps the body_<fn> name.

test/docs: align with the lowercase verif_ default and proof placement

Grammar / Corpus and binding tests (pull_request) Successful in 1m6s

Details

Extension / Format, types, lint, extension tests (pull_request) Successful in 3m22s

Details

e999296734

The default document is verif_<file>.v since the template update; update the
integration expectation and the docs/comments that still said Verif_<file>.v.
The README also now says a linked proof is generated in the document its
PROOF clause points at.

michael changed title from ~~WIP: branch suggestion: create spec from template~~ to branch suggestion: create spec from template

2026-10-23 11:34:45 +02:00

michael approved these changes

2026-10-23 12:02:45 +02:00

extension/.vscodeignore Outdated

					
				@ -22,0 +22,4 @@

				# The proof templates are read from disk at run time, so they are the one

				# thing under `src/` that must survive packaging. Re-include only the `.eta`

				# files: the `.ts` template argument interfaces stay out via `**/*.ts`.

				!src/templates/*.eta

I would do !src/templates//*.eta or just !/*.eta, so that the files are also allowed to be nested in deeper folders without having to change this further

I would do !src/templates/**/*.eta or just !**/*.eta, so that the files are also allowed to be nested in deeper folders without having to change this further

michael marked this conversation as resolved

extension/src/commands/services/files.ts

					
				@ -35,3 +23,1 @@

				 */

				export async function triggerOnDocumentOpen(path: Uri): Promise<void> {

					await workspace.openTextDocument(path).then();

					try {

why change this, it does exactly the same thing, and has just been changed for the hell of it?

michael marked this conversation as resolved

extension/src/commands/services/files.ts

					
				@ -47,3 +41,1 @@

					const lastIndex = fileName.lastIndexOf('.');

					if (lastIndex === -1) return fileName;

					return fileName.substring(0, lastIndex);

					const { name } = parse(path.fsPath);

technically better but harder to understand that Uri destructs to the name of the file

i would do it more explicit with const name = parse(path.fsPath).name if it has to be changed

technically better but harder to understand that Uri destructs to the name of the file i would do it more explicit with `const name = parse(path.fsPath).name` if it has to be changed

michael marked this conversation as resolved

michael changed title from ~~branch suggestion: create spec from template~~ to WIP: branch suggestion: create spec from template

2026-10-23 12:03:27 +02:00

michael added 1 commit

2026-10-23 12:34:00 +02:00

fixed incorrect ignorign of node modules, and made it possible to further nest templates if needed

Extension / Format, types, lint, extension tests (pull_request) Waiting to run

Details

Grammar / Corpus and binding tests (pull_request) Waiting to run

Details

369ae76fb8

michael added 1 commit