Check whether the extension's dependencies are installed #19

marfavi · 2026-10-09T11:30:24+02:00

marfavi commented

2026-10-09 11:30:24 +02:00

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

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

marfavi added 1 commit

2026-10-09 11:30:24 +02:00

Check extension's dependencies are installed

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

Details

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

Details

47733048f7

Verify on activation (and when clightgen or VsRocq may have changed) that
the toolchain is present, callable and new enough. Adds a src/dependencies
module with an injectable exec layer, a status bar chip, a dependency
panel, settings for the clightgen and vsrocqtop paths, and the
crocq.checkDependencies / crocq.openDependencyPanel commands. The Create
Rocq Model command now gates on the dependency check and uses the
configured clightgen path.

marfavi referenced this pull request

2026-10-09 11:33:51 +02:00

WIP: Check Crocq dependencies and add relevant UI #18

marfavi added 1 commit

2026-10-09 12:52:02 +02:00

Merge branch 'main' into feat/dependency-checking

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

Details

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

Details

bd4c89a6d1

marfavi changed title from ~~WIP: Check extension's dependencies are installed~~ to Check extension's dependencies are installed

2026-10-09 12:52:04 +02:00

marfavi added 2 commits

2026-10-09 13:03:07 +02:00

Merge branch 'main' into feat/dependency-checking 2bcaf83fbe

# Conflicts:
#	extension/src/commands/createRocqModel.ts
#	extension/src/commands/services/terminal.ts
#	extension/src/test/unit/createRocqModel.test.ts

Dedupe quoteShellArgument into util/shell

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

Details

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

Details

48ea386832

Remove the copy left in src/dependencies/checks.ts by the merge so there is
a single implementation, and drop the duplicated shell-quoting tests from
checks.test.ts (already covered by util/shell.test.ts).

marfavi added 1 commit

2026-10-09 13:57:02 +02:00

Merge branch 'main' into feat/dependency-checking

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

Details

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

Details

c8c4d1d7dd

marfavi changed title from ~~Check extension's dependencies are installed~~ to Check whether the extension's dependencies are installed

2026-10-09 14:19:31 +02:00

marfavi added 5 commits

2026-10-09 14:19:46 +02:00

test: give the create Rocq model integration test a fake toolchain 09eda0a62f

crocq.createRocqModel now stops at the dependency gate, so the integration test
only observed a terminal on hosts that happened to have a real clightgen and
vsrocqtop on PATH; it timed out in CI. Point the two path settings at fake
executables, wait for the check to be ready, and assert the terminal received
the configured executable. Verified with the opam toolchain off PATH.

fix: hold the vsrocqtop dependency to the Rocq version requirement eb71961a84

checkVsrocq used the VsRocq extension version (2.3.2) as requiredVersion even
when it fell back to vsrocqtop, whose version output reports Rocq version
(checked against 9.1), so the panel showed "Required version 2.3.2 or later"
next to a summary demanding Rocq 9.1. Use a server-specific base, assert the
requirement in the ok and mismatch server tests, and cover the missing-path
branch and the not-executable/timeout to error mapping. Also document where
the Exec type is implemented.

fix: re-check dependencies when the installed extensions change a38f947557

VsRocq is one of the checked dependencies, so installing or removing it - which
the panel does with its own Install VsRocq extension button - changes the
result. Subscribe to vscode.extensions.onDidChange and refresh the state right
after the panel install command resolves.

feat: activate crocq on startup 11639d5951

The status bar chip only appeared once a C file was opened because onLanguage:c
was the only activation event. Add onStartupFinished so the dependency check and
the chip are ready when the window opens.

docs: refresh the extension README

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

Details

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

Details

f621fb7d94

Describe when the dependency check runs (startup, settings and extension
changes, annotated C files), and drop the leftover quickstart Known Issues and
Release Notes placeholder sections.

marfavi added 6 commits

2026-10-09 14:50:07 +02:00

fix: only warn about missing dependencies after crocq is used ca73d10124

Installing the extension (which now activates on onStartupFinished) popped a missing-dependency error at every window startup. Gate the notification behind a user engagement - a crocq command or an annotated C file - while the status bar chip stays ambient. The reporter forgets the state it saw while silent so the first engaged failure still notifies.

docs: correct when the dependency check runs 7945013045

The README claimed the toolchain is verified whenever any C file is opened or any Crocq command runs. Name the real triggers and note that the missing-dependency notification only appears once crocq is actually used.

refactor: pass argv to the terminal command service 32fe4d6ea6

executeTerminalCommand quoted cd itself but required every caller to pre-quote the command, a contract that is easy to get wrong. Take the program and its arguments as an argv array and quote each one inside the service, so a dynamic value cannot reach the shell unquoted.

fix: gate create Rocq model on the settled dependency check 7b0e25919b

A request that joins an in-flight check only schedules a follow-up run, so ensureDependenciesReady could read the stale state of the run it happened to join. Add CheckScheduler.whenIdle() and wait for any follow-up to settle before reading the state.

refactor: scan lines for the annotation marker 5e53c96427

onDocumentOpened materialised the whole document with getText() just to look for '/*@'. Move the scan to a pure, unit-tested hasAnnotationMarker(LineReader) helper that walks the lines instead.

chore: drop the redundant onLanguage:c activation event

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

Details

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

Details

98e335c620

onStartupFinished already activates the extension at window start, so the onLanguage:c event can never fire first.

marfavi added 5 commits

2026-10-09 15:20:29 +02:00

fix: omit the version bar when no VsRocq route is configured b912ba96ee

checkVsrocq reported requiredVersion 2.3.2 for the result where neither
the VsRocq extension nor a vsrocqtop path is configured, while every
other server-branch outcome uses the Rocq bar (9.1). No single version
is truthful there - the extension route needs VsRocq, the server route
needs Rocq - so omit it. The summary and hint already name both routes.

Cover the previously untested branch.

fix: ignore a dependency check that settles after dispose 3e8450616d

The manager is disposed with the extension while a check may still be in
flight (a tool is allowed to run for 10 s). Applying that settled result
fired the disposed emitter, updated the disposed status bar item and
could still notify the user during shutdown.

Guard the settle path and the UI choke point, and cover both with an
integration test.

fix: expand a leading ~ in the configured tool paths 1650fb941b

Neither the dependency checks (which run the executable with execFile) nor
the terminal command (which quotes its arguments) expands ~, so a ~/...
clightgen or vsrocq path silently failed. Expand it in the settings layer
where the paths are already resolved, and keep the helper in a pure module
so it is unit tested.

fix: surface webview command failures to the user ed63a5f15b

onDidReceiveMessage discarded the handler's promise, so a rejected command
such as workbench.extensions.installExtension (offline, no marketplace)
became an unhandled rejection and the user saw nothing. Catch it at the
message boundary and report it.

fix: warn about missing dependencies when the window is restored

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

Details

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

Details

0bb97e9628

crocq activates on onStartupFinished, so the documents of a restored
window are already open before the manager's onDidOpenTextDocument
listener exists. An annotated C file that was restored therefore never
engaged the manager, and since the missing-dependency warning is gated on
engagement it stayed silent until another file was opened - or this one
was closed and reopened.

Replay the open documents on construction, like extension.ts already does
for the language features. Add a DependencyNotifications seam so the
integration tier can assert the warning, which is otherwise pure UI.

EatOreo reviewed

2026-10-09 16:26:05 +02:00

extension/package.json Outdated

					
				@ -31,0 +46,4 @@

				          "order": 1,

				          "markdownDescription": "Path to the `clightgen` executable shipped with [CompCert](https://compcert.org/) 3.17 or later. Use the bare name to look it up on `PATH`."

				        },

				        "crocq.vsrocq.path": {

jeg synes fjern vsrocqtop support

done

marfavi marked this conversation as resolved

extension/src/extension.ts

					
				@ -30,3 +41,3 @@

				export async function activate(

					context: vscode.ExtensionContext,

				): Promise<void> {

				): Promise<CrocqExtensionApi> {

skal vi virkelig retunere en external vscode api? dvs andre extensions kan calle den, er det ikke ude af scope?

OK, fjernet

marfavi marked this conversation as resolved

extension/src/extension.ts Outdated

					
				@ -92,2 +126,4 @@

						),

					);

					return { dependencies: dependencyManager };

external vscode api

fjernet

marfavi marked this conversation as resolved

marfavi added 4 commits

2026-10-09 16:29:25 +02:00

refactor: inline the dependency check queue into the manager 662b516f49

The coalescing lived in a separate, generic CheckScheduler<T> whose only
caller was DependencyManager. Fold it into the manager as a serial promise
chain: check() appends its run to a tail and returns that run's own promise.

The properties that matter are kept - runs never overlap, a request made
mid-check is never dropped, and ensureDependenciesReady reads a fresh (not a
joined, possibly stale) result, so whenIdle() is gone. A burst of N requests
now runs N sequential checks instead of collapsing to two, which the existing
15s recheck throttle already bounds. Tests move to the integration tier, where
a slow fake tool proves the checks never overlap.

refactor: inline the annotation marker scan into the manager 41ca322fb8

documentText.ts existed only to hold a four-line line scan behind a structural
LineReader interface, purely so it could be unit tested without vscode. Fold the
scan into the manager as a plain function typed against vscode.TextDocument and
drop the module and its test; detection stays covered by the integration test
that opens an annotated C file before the manager exists.

refactor: build dependency check results from a shared base 0bfb8c0362

Every branch of checkClightgen/checkVsrocq re-listed all eight fields of
DependencyCheckResult, so adding a field meant editing a dozen returns. Add a
private outcome(base, fields) helper whose hint/foundVersion default to
undefined, and let each branch name only what it sets.

Also drop the unused DEPENDENCY_IDS runtime array (the type alias is enough) and
unexport dependencyStatusIcon/dependencyStatusLine, which only ever served
dependencyTooltip and the tests.

perf: activate crocq only in workspaces with C files

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

Details

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

Details

43863a0a7e

onStartupFinished activated the extension - and its clightgen/vsrocqtop check -
in every window, including workspaces with no C content, and showed a toolchain
status chip there too. Scope activation to C workspaces instead
(workspaceContains:**/*.c plus onLanguage:c).

The contributed commands still activate the extension in any window, so the
dependency panel and setup entry points stay reachable everywhere.

marfavi added 3 commits

2026-10-09 21:55:38 +02:00

refactor: require the VsRocq extension 195c119e6c

crocq accepted either the VsRocq extension or a callable vsrocqtop server.
The extension is the supported route, so drop the server fallback: checkVsrocq
no longer execs anything, and the crocq.vsrocq.path setting, the result's
source field, and the panel's VsRocq path/Source UI all go with it.

Integration tests can no longer satisfy the check with a fake executable, so a
fixture extension (rocq-prover.vsrocq, version 2.5.0) is loaded into the test
host via extensionDevelopmentPath.

refactor: stop exporting an extension API e9f1e572c9

activate returned CrocqExtensionApi, which turns the manager's state and
check() into a public extension API that any other extension can call. crocq
has no consumer for it - it existed only so the integration tests could reach
the activated manager - so activate now returns void and the API types are
gone.

The integration tests own a DependencyManager instance instead; it reads the
same settings as the activated one, so it observes the same results.

fix: don't claim the VsRocq extension is missing

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

Details

Extension / Format, types, lint, extension tests (pull_request) Successful in 2m56s

Details

6359a6fd37

marfavi requested review from EatOreo

2026-10-09 21:59:22 +02:00

marfavi scheduled this pull request to auto merge when all checks succeed

2026-10-14 10:36:46 +02:00

EatOreo scheduled this pull request to auto merge when all checks succeed

2026-10-14 10:45:10 +02:00