A VSCode extension that implements outline view and go to definition for Coq files.

Overview

Coq Outline

A VSCode extension that provides outline view for Coq files.

Features

  • Provide outline views for Coq files.
  • Provide go to definition function to track Coq definitions.
  • It supports following types of symbols.
    • Section/Module/Module Type as regions.
    • Modules instances as definitions.
    • (Program) Definition/Fixpoint/CoFixpoint/Function and so on.
    • (Co)Inductive definitions and their constructors.
    • Class/Record as aggregations of their fields.
    • Class/Record fields.
    • Ltac definitions.
    • Parameter/Axiom/Conjecture/Variable/Hypothesis and their plural variants.
    • Definitions by the with keyword.

Screenshots

  • Screenshot of the outline view. outline-screenshot
  • Screenshots of the context menu and peek definition. context-screenshot peek-screenshot

Requirements

  • VS Code 1.72.0, or more recent
  • Coq 8.7.0, or more recent
  • VSCoq 0.3.6

Installation

The extension has not published yet. To install a beta version, please go to the Github Repo and download latest release. Then, either press "Cmd-Shift-P" and "Extensions: Install from VSIX", or run code --install-extension coqoutline-0.2.2.vsix (or whatever version number) from your terminal.

Instructions

  • To open the outline view in case you have turned it off, click View > Open View, then search for and select outline.
  • To lookup the definition of a symbol, right click the symbol and select Go to Definition or Peek > Peek Definition in the context menu.
    • It searches definition by string matching. As a result, it retrieves all definitions with the same name regardless of the context.

Dos and Don'ts when writing Coq

The extension uses regular expressions to analyze Coq documents, thus not all Coq writing styles is accepted. The followings are rules recommended when writing Coq with this extension. Violating them may cause the extension analyze your Coq files in wrong ways.

  • Comments should not be in the middle of a keyword and the symbol it defines.
    (* NOT OK *)
    Definition (* comment *) name ...
  • Any name should be in the same line as its key word. And any keyword must be the first word in a line. For example,
    (* OK *)
    Definition name ...
    (* NOT OK *)
    Definition
        name ...
    (* NOT OK *)
    (* anything *) Definition name ...
  • Keyword with should be treated the same as other key words and follows two rules above.
    (* OK *)
    Inductive a ...
        with b ...
    (* NOT OK *)
    Inductive a ... with b ...
  • Allow multiple definitions of assumptions in the same line.
    (* OK *)
    Parameters a b c : Type.
    Parameters (a : Type) (b c: Type).
    (* NOT OK, only a and b will be parsed *)
    Parameters a b
        c : Type.
  • Fields in classes and records are supported. But field definitions should be in different lines of class names or record names, and each field definition should leads a new line.
    (* OK *)
    Class A : Type := {
        x : Type;
        y: Type
    }.
    (* NOT OK *)
    (* should be put in two lines *)
    Class B : Type := { i : Type;
        (* should be put in two lines *)
        j: Type; k: Type
    }.
  • Inductive definition and its constructors should not be put in the same line, and remember to put at least a white space between items.
    (* OK *)
    Inductive A: Type :=
    | A | B
    | C.
    (* NOT OK *)
    Inductive A: Type := | A
    | B| C.
  • When defining a module instance, the := symbol should be put in the same line as the keyword.
    (* OK *)
    Module A := B.
    (* NOT OK *)
    Module A
        := B.
  • Defined is treated the same as Qed, no succeeding ident is allowed.

Known Issues & ToDos

  • does not support utf-8 characters
  • multiple assumptions by one key word. (supported)
  • the with keyword (supported)
  • the range (end line) of program definitions may be wrong, no "Defined" token (supported)
  • incorrectly includes code in comments (fixed)
  • inductive constructors not handled (fixed)
  • after renaming an open file, the outline view cannot display but definitions can already be located (fixed)
You might also like...

Open source rich text editor based on HTML5 and the progressive-enhancement approach. Uses a sophisticated security concept and aims to generate fully valid HTML5 markup by preventing unmaintainable tag soups and inline styles.

This project isn’t maintained anymore Please check out this fork. wysihtml5 0.3.0 wysihtml5 is an open source rich text editor based on HTML5 technolo

Nov 21, 2022

Personal blog and portfolio with a admin panel and comment system.

Personal blog and portfolio with a admin panel and comment system.

Implementation of a Full Stack Blog With a Comment System And Admin Panel With PHP, React & MYSQL FULL DOCUMENTATION SITE LINK Contents Database Desig

Oct 21, 2022

A modern, simple and elegant WYSIWYG rich text editor.

jQuery-Notebook A simple, clean and elegant WYSIWYG rich text editor for web aplications Note: Check out the fully functional demo and examples here.

Nov 20, 2022

Quill is a modern WYSIWYG editor built for compatibility and extensibility.

Note: This branch and README covers the upcoming 2.0 release. View 1.x docs here. Quill Rich Text Editor Quickstart • Documentation • Development • Co

Nov 27, 2022

The world's #1 JavaScript library for rich text editing. Available for React, Vue and Angular

The world's #1 JavaScript library for rich text editing. Available for React, Vue and Angular

TinyMCE TinyMCE is the world's most advanced open source core rich text editor. Trusted by millions of developers, and used by some of the world's lar

Nov 28, 2022

A lightweight and amazing WYSIWYG JavaScript editor - 20kB only (8kB gzip)

A lightweight and amazing WYSIWYG JavaScript editor - 20kB only (8kB gzip)

Supporting Trumbowyg Trumbowyg is an MIT-licensed open source project and completely free to use. However, the amount of effort needed to maintain and

Nov 23, 2022

:notebook: Our cool, secure, and offline-first Markdown editor.

:notebook: Our cool, secure, and offline-first Markdown editor.

Monod Hi! I'm Monod, the Markdown Editor! Monod is a (relatively) secure and offline-first Markdown editor we have built at TailorDev in order to lear

May 30, 2022

:herb: NodeJS PHP Parser - extract AST or tokens (PHP5 and PHP7)

php-parser This javascript library parses PHP code and convert it to AST. Installation This library is distributed with npm : npm install php-parser -

Nov 22, 2022
Releases(v0.2.2-beta)
  • v0.2.2-beta(Oct 24, 2022)

    v0.2.2-beta

    • provide outline views for Coq files.
    • provide Go to Definition function to track Coq definitions.

    Instruction

    To install this version of CoqOutline,

    1. download the file coqoutline-0.2.2.vsix below
    2. press "Cmd-Shift-P" and "Extensions: Install from VSIX" in your VSCode to install this file, or run code --install-extension coqoutline-0.2.2.vsix (or whatever version number) from your terminal.
    Source code(tar.gz)
    Source code(zip)
    coqoutline-0.2.2.vsix(711.36 KB)
Owner
Wang Zhongye
Wang Zhongye
A React component to view a PDF document

React PDF viewer A React component to view a PDF document. It's written in TypeScript, and powered by React hooks completely. // Core viewer import {

React PDF Viewer 1.4k Nov 23, 2022
Easily convert markdown files to PDF

ezPDF What's this? This is a simple markdown to pdf parser that supports custom CSS stylesheets. In the future, ezPDF will allow you to preview files

Matheus 12 Oct 11, 2022
A web interface to edit TP-Link Router Config export files (typically named config.bin).

TP-Link Router Config Editor A web interface to edit TP-Link Router Config export files (typically named config.bin). Visit the website. Tested on an

Jahed 10 Nov 17, 2022
Browser-based code editor created to edit local or server files online

notIDE Browser-based code editor created to edit local or server files online. Features Autosave while editing Syntax highlight using ace editor Creat

Mr Crypster 15 Nov 21, 2022
⚗️ Zeplin extension that generates Swift snippets from colors, fonts, and layers

Zeplin extension that generates Swift snippets from colors, fonts and layers. Features ?? Color pallette for iOS Example import UIKit extension UICol

Artem Novichkov 83 May 29, 2022
PackageInfo - chrome-extension which provides information about node packages, whenever you select the package name using mouse

PackageInfo chrome-extension which provides information about node packages, whenever you select the package name using mouse Whenever you surf throug

subrahmanya  s hegade 3 Feb 12, 2022
A chrome extension which helps change ace editor to monaco editor in web pages, supporting all features including autocompletes.

Monaco-It Monaco-It is a chrome extension turning Ace Editor into Monaco Editor, supporting all features including autocompletes. 一些中文说明 Supported Lan

null 3 May 17, 2022
An extension that adds an "edit tags" button to every object on osm.org

OpenStreetMap Tags Editor This is a WebExtension that adds an "Edit Tags" button to all node, way, and relation pages on the osm.org website. The butt

Ilya Zverev 12 Aug 19, 2022
Open source rich text editor based on HTML5 and the progressive-enhancement approach. Uses a sophisticated security concept and aims to generate fully valid HTML5 markup by preventing unmaintainable tag soups and inline styles.

This project isn’t maintained anymore Please check out this fork. wysihtml5 0.3.0 wysihtml5 is an open source rich text editor based on HTML5 technolo

Christopher Blum 6.5k Nov 21, 2022
A simple, beautiful, and embeddable JavaScript Markdown editor. Delightful editing for beginners and experts alike. Features built-in autosaving and spell checking.

SimpleMDE - Markdown Editor A drop-in JavaScript textarea replacement for writing beautiful and understandable Markdown. The WYSIWYG-esque editor allo

Sparksuite 9.2k Nov 19, 2022