Skip to content
This repository has been archived by the owner on Nov 5, 2021. It is now read-only.

A Linter for Isabelle. Developed for my bachelor's thesis at the Chair For Logic and Verification at the Technical University of Munich

License

Notifications You must be signed in to change notification settings

TheMC47/bachelor-thesis-isabelle-linter

Repository files navigation

READ ONLY

Further developments of the linter are happening at https://github.com/isabelle-prover/isabelle-linter/. This is just to document the work during my bachelor's thesis.

Isabelle linter

A linter for Isabelle. Developed for my bachelor's thesis at the Chair for Logic and Verification at the Department of Informatics of the Technical University of Munich.

How to use

Setup

  1. Checkout Isabelle submodule: git submodule init && git submodule update
  2. Build Isabelle
isabelle/bin/isabelle components -a
isabelle/bin/isabelle components -I
isabelle/bin/isabelle build
  1. Compile the linter: ./sbt "project linter" assembly
  2. For jEdit support: Patch jEdit jars: ./patch_jedit
  3. For the tool support: isabelle/bin/isabelle components -u linter/target

Usage

  • jEdit: isabelle/bin/isabelle jedit -e
  • tool: isabelle/bin/isabelle lint. Use isabelle/bin/isabelle lint -? to see the tool options

About

A Linter for Isabelle. Developed for my bachelor's thesis at the Chair For Logic and Verification at the Technical University of Munich

Resources

License

Stars

Watchers

Forks

Packages

No packages published