Rename coq references

[Tammo0987]

Description

Renames internal Coq references to Waterproof (editor/UI) or Rocq (language/LSP) for naming consistency across the codebase.

Testing this PR

Pure rename refactor with no behavioral changes. npm run compile passes, unit tests pass (3 pre-existing failures in vFile.test.ts unrelated to this PR).

[Copilot]

Pull request overview

This PR is a naming-consistency refactor that replaces internal “Coq” terminology with Waterproof for editor/UI concepts and Rocq for language/LSP concepts across the extension, webviews, and editor parsing utilities.

Changes:

• Renames key UI/editor/webview classes and identifiers (e.g., CoqWebview → WaterproofPanel, CoqEditorProvider → WaterproofEditorProvider, ProseMirrorWebview → WaterproofWebview).
• Renames Rocq-related UI components/styles (e.g., goal env CSS classes, CoqPp → RocqPp, rocqdoc translation exports).
• Updates tests and Cypress docs/labels to match the new naming.

Reviewed changes

Copilot reviewed 53 out of 54 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
views/styles/rocqpp.css	Adds/renames pretty-print styling sheet for Pp output.
views/styles/goals.css	Renames goal/hypothesis CSS classes from coq-* to rocq-*.
views/goals/RocqPp.tsx	Renames Pp rendering component and updates stylesheet import.
views/goals/Message.tsx	Switches message rendering from CoqPp to RocqPp.
views/goals/Info.tsx	Updates comment naming to Rocq terminology.
views/goals/index.tsx	Updates webview script comment to Waterproof terminology.
views/goals/Goals.tsx	Renames goal env class and swaps CoqPp for RocqPp.
views/goals/ErrorBrowser.tsx	Swaps CoqPp for RocqPp in error rendering.
views/example/exampleIndex.tsx	Updates webview script comment to Waterproof terminology.
views/debug/index.tsx	Updates webview script comment to Waterproof terminology.
views/debug/Hypothesis.tsx	Renames CSS classes/types and swaps CoqPp for RocqPp.
views/debug/Debug.tsx	Updates comment naming to Rocq terminology.
src/webviews/waterproofPanel.ts	Renames base webview abstraction to Waterproof terminology and adjusts HTML title.
src/webviews/standardviews/tactics.ts	Updates base class import/extends to WaterproofPanel.
src/webviews/standardviews/symbols.ts	Updates base class import/extends to WaterproofPanel.
src/webviews/standardviews/search.ts	Updates base class import/extends to WaterproofPanel.
src/webviews/standardviews/execute.ts	Updates base class import/extends to WaterproofPanel.
src/webviews/goalviews/goalsPanel.ts	Updates webview event imports to waterproofPanel.
src/webviews/goalviews/goalsBase.ts	Updates base class to WaterproofPanel.
src/webviews/goalviews/debug.ts	Updates webview event imports to waterproofPanel.
src/webviews/goalviews/compositeGoalsPanel.ts	Updates webview event imports to waterproofPanel.
src/webviewManager.ts	Renames stored webview types/maps to Waterproof terminology.
src/version-checker/version-checker.ts	Renames internal “required version” identifiers toward Rocq terminology.
src/util.ts	Renames exclusion helper to excludeRocqFileTypes.
src/pm-editor/waterproofWebview.ts	Renames ProseMirror webview class/provider types to Waterproof terminology.
src/pm-editor/waterproofEditor.ts	Renames custom editor provider and updates webview creation/registration calls.
src/pm-editor/index.ts	Re-exports WaterproofEditorProvider instead of prior name.
src/mainNode.ts	Renames Rocq client-provider factory symbol and activation wiring.
src/mainBrowser.ts	Renames Rocq client-provider factory symbol and activation wiring (browser).
src/lsp-client/sentenceManager.ts	Updates sentence comment terminology to Rocq.
src/lsp-client/rocq/types.ts	Renames CoqLspServerConfig to RocqLspServerConfig.
src/lsp-client/rocq/requestTypes.ts	Renames Rocq request/notification constants.
src/lsp-client/rocq/client.ts	Updates client to use renamed request/notification constants + comment terminology.
src/lsp-client/commandExecutor.ts	Updates error message from Coq to Rocq terminology.
src/infoview.ts	Updates webview event import to waterproofPanel.
src/extension.ts	Renames status bar + editor provider + Rocq server config usage and helper calls.
src/components/enableButton.ts	Renames status bar component to WaterproofStatusBar.
src/components.ts	Updates file-progress interface comment terminology to rocq.
editor/src/rocqdoc.ts	Renames coqdoc translation exports to rocqdoc equivalents.
editor/src/index.ts	Switches editor configuration to use rocqdocToMarkdown.
editor/src/file-utils.ts	Updates comment terminology from coqblock to rocqblock.
editor/src/document-construction/vFile.ts	Updates parser docstring terminology (Coq → Rocq).
editor/src/document-construction/inner-blocks.ts	Switches extraction helper from extractCoqBlocks to extractRocqBlocks.
editor/src/document-construction/construct-document.ts	Switches top-level construction to use extractRocqBlocks.
editor/src/document-construction/block-extraction.ts	Renames coq-block extraction helpers to Rocq terminology.
cypress/support/commands.ts	Updates Cypress command docstrings (coq → rocq).
cypress/e2e/basic.cy.ts	Updates test name string (coq → rocq).
tests/translate-coqdoc.test.ts	Updates imports/names for rocqdoc translation functions.
tests/prosedoc-construction/top-level-construction.test.ts	Updates comments referencing Coq → Rocq.
tests/prosedoc-construction/newlineblock-lean.test.ts	Updates Lean-equivalence comments to reference Rocq.
tests/prosedoc-construction/inner-blocks.test.ts	Updates comment label for Rocq block content.
tests/prosedoc-construction/inner-blocks-lean.test.ts	Updates Lean-equivalence comments to reference Rocq.
tests/prosedoc-construction/block-extractions.test.ts	Updates imports/names for Rocq extraction helpers and rocqdoc math display extraction.
tests/prosedoc-construction/block-extractions-lean.test.ts	Updates Lean-equivalence comments to reference Rocq.

Comments suppressed due to low confidence (2)

src/webviews/waterproofPanel.ts:189

• showView() sets a hard-coded HTML title of "Rocq's info panel" for every non-infoview webview (tactics, symbols, search, execute, etc.). Given this class is for UI panels (Waterproof) and is not limited to Rocq/infoview, the title is misleading. Consider using a generic Waterproof title and/or including the panel name (e.g., "Waterproof – ${name}").
  editor/src/document-construction/block-extraction.ts:142
• extractMathDisplayBlocksRocqDoc() uses a regex that matches single-dollar math blocks ($...$), but computes innerRange using "$$".length (2) instead of "$".length (1). This makes the innerRange offsets incorrect, which can break block range calculations downstream. Adjust the innerRange trimming to match the actual delimiter length used by the regex.

// Regex for extracting the math display blocks from the rocqdoc comments.
// We need a different regex here, since rocq markdown uses single dollar signs for math display :)
const regexMathDisplay = /\$([\S\s]*?)\$/g;

export function extractMathDisplayBlocksRocqDoc(input: string): MathDisplayBlock[] {
    const mathDisplay = Array.from(input.matchAll(regexMathDisplay));
    const mathDisplayBlocks = Array.from(mathDisplay).map((math) => {
        if (math.index === undefined) throw new Error("Index of math is undefined");
        const range = { from: math.index, to: math.index + math[0].length};
        const innerRange = { from: range.from + "$$".length, to: range.to - "$$".length};
        return new MathDisplayBlock(math[1], range, innerRange, 0);
    });

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[DikieDick]

Thanks! I am very happy with this change.

Looks good as is.
Added two suggestions for updating the references to the Rocq documentation (using the rocq-prover.org domain instead of coq.inria.fr) and a separate comment on the ; in the error output.

[DikieDick]

We should maybe remove this semicolon or create an issue tracking this.

Opinion: now that I know that the semicolon appears in the 'error output' only because there is an (I suppose accidental) semicolon after this line, I think it is really ugly :|

[Tammo0987]

Should be fixed now, I also removed the unused react import here. Now lets wait for #340 to be merged.

[Tammo0987]

@DikieDick thanks for the review, I will fix them. Also Pim suggested to merge impermeable/waterproof-editor#87 first, so we should also wait for that.