VizCAR: A Visualizer for ViCAR

VizCAR is a visualizer developed for the Coq library ViCAR (Visualizing Categories with Automated Rewriting).

Running VizCAR

• Download Visual Studio Code (vscode).
• Install opam.
• Install coq.
• Install coq-lsp on opam, by running opam install coq-lsp.
• Install the vscode extension for coq-lsp, ejgallego.coq-lsp at v0.1.10. Follow all setup instructions for coq-lsp as detailed here.
• Either clone the ViCAR repository, or install it through opam via opam pin -y coq-vicar https://github.com/inQWIRE/ViCAR.git. Detailed instructions for ViCAR can be found on the github homepage.
• Install the vscode extension inqwire.vizcar at the latest version (currently v0.0.6).
• After instantiating the appropriate typeclasses through ViCAR, run the command vizcar.activate to activate automatic rendering of proof terms in Coq. This command can be found via opening the command palette in your vscode instance (shortcut Ctrl (Win, etc) / Cmd (Mac) + Shift + P) and searching for vizcar.activate or vizcar: activate: Start rendering expressions with vizcar automatically.. To stop automatic rendering, run the command vizcar.deactivate or search for vizcar: deactivate: Stop rendering expressions with vizcar automatically.

Paper

The paper for ViCAR and VizCAR can be found on arxiv.