Skip to content

Opt-in study logging of extension interactions #121

Description

@CatarinaGamboa

Tracking issue for the study side: CatarinaGamboa/building-examples-liquidjava#1

Goal

Add an opt-in study logger that records how participants use the extension (views, interactions, verification results, time per file). It writes the events to a local JSONL file in the workspace. It is off by default and never runs for normal users.

Settings

Add to client/package.json → contributes.configuration:

setting type default purpose
liquidjava.study.enabled boolean false turn logging on (set by the study repo's .vscode/settings.json)
liquidjava.study.participantId string "" included in every event
liquidjava.study.logPath string .liquidjava/study-log.jsonl relative to the workspace root

(Existing settings use the liquidJavaServer. prefix, so we should decide on one naming scheme.)

Proposed design

  • New client/src/services/study-log.ts:
    • log(event: string, data?: object) appends { t, pid, session, event, ...data } as one line
    • no-op when disabled; listens to onDidChangeConfiguration so it can be switched on and off
    • buffered async writes, flushed on deactivate
    • a per-launch session id, so separate VS Code sessions can be told apart
  • Command liquidjava.study.revealLog: opens the log file (for transparency, and to help participants hand it in)

Events

Editor / timing (in client/src/services/events.ts, which already listens to onDidChangeActiveTextEditor / onDidSaveTextDocument)

  • file_focused / file_blurred (active editor changes)
  • file_saved, file_edited (debounced, with a count and no content)
  • window_focus / window_blur via vscode.window.onDidChangeWindowState

Verification (client/src/lsp/client.ts, client/src/services/diagnostics.ts)

  • verify_started / verify_finished (trigger, duration)
  • diagnostic_shown / diagnostic_resolved (file, line, kind: refinement / state / …, plus a stable key so the same error can be matched across runs)

Webview (client/src/webview/script.ts → postMessage({ type: 'log', ... }) → handled in provider.ts, which already forwards messages through onDidReceiveMessage)

  • view_visible / view_hidden
  • tab_selected: diagnostics / context / fsm
  • section_toggled: counterexample, VC changes, VC implications, hint, context variables / ghosts / aliases
  • diagnostic_reveal (the existing openFile message), highlight
  • clipboard_copy

Other

Privacy

  • Log file names, lines and error kinds, but not source code (optional code snapshots are an open question in the study issue).
  • Nothing leaves the machine: participants hand in the file themselves via git.
  • Don't use the VS Code telemetry API. It follows the user's global telemetry setting and would send data elsewhere.

Acceptance criteria

  • No file is created and no overhead is added when liquidjava.study.enabled is false
  • Opening the study repo with the settings file produces a valid JSONL log
  • From the log alone, we can compute time-focused and time-to-fix per exercise file
  • The events listed above are covered; the schema is documented in the README / CONTRIBUTING

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions