Skip to content

tamarin-prover/vscode-tamarin

This branch is 9 commits ahead of hugotvn/vscode-tamarin:master.

Folders and files

NameName
Last commit message
Last commit date

Latest commit

2639bc5 · Aug 21, 2024
Jun 17, 2024
Jul 18, 2024
Aug 2, 2024
Jun 17, 2024
Aug 2, 2024
Aug 2, 2024
Jul 25, 2024
Aug 2, 2024
Aug 2, 2024
Sep 3, 2021
Jul 25, 2024
Jul 22, 2024
Jun 25, 2024
Aug 2, 2024
Aug 2, 2024
Jun 17, 2024

Repository files navigation

Tamarin Visual Studio Code extension

The official Visual Studio Code extension for Tamarin files (.spthy) supported by the Tamarin team. Based on giclu-3's extension and using Tamarin's tree-sitter grammar.

Example

Features:

  • Enhances giclu-3's syntax highlighting.

  • Adds comprehensive syntax error detection based on the grammar with MISSING or ERROR messages.

  • Provides various wellformedness checks:

    • Checks position and usage of reserved facts (Fr, Out, In, K, KD, KU).
    • Checks whether variable are used consistly inside a rule, i.e., using the same capitalization and sort.
    • Spellcheck on facts (must start with an uppercase letter).
    • Checks whether all variables in the conclusion of a rule appear in the premises (except public variables).
    • Checks the arity of facts and functions.
    • Checks whether a lemma uses free terms.
    • Checks whether all facts in the premises of the rules appear in the conclusion of some (other) rule (provides a quick fix by using the closest exisiting fact, based on editing distance).
    • Checks wether all variables in the right hand side of a macro are in the left hand side or public.
    • Checks wether all variable in the right hand side of an equation are in the left hand side.
    • Provides a quick fix for function names (suggestions based on editing distance).
    • Checks wether built-ins are imported when encountering corresponding functions or symbols (provides a quick fix to import the right built-in).

    This is a subset of the checks performed by Tamarin. For more details on Tamarin's wellformedness checks, see the corresponding Tamarin Prover manual section.

  • Use right click and Rename on an indentifier to rename all occurences of it inside a rule or a lemma.

  • Use right click and Search Definition on facts or function names and press CTRL+TAB to navigate through all occurences.

About

A VSCode plugin for Tamarin files

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • TypeScript 70.8%
  • JavaScript 27.0%
  • C 2.2%