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.
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.
- Checkout Isabelle submodule:
git submodule init && git submodule update - Build Isabelle
isabelle/bin/isabelle components -a
isabelle/bin/isabelle components -I
isabelle/bin/isabelle build
- Compile the linter:
./sbt "project linter" assembly - For jEdit support: Patch jEdit jars:
./patch_jedit - For the tool support:
isabelle/bin/isabelle components -u linter/target
- jEdit:
isabelle/bin/isabelle jedit -e - tool:
isabelle/bin/isabelle lint. Useisabelle/bin/isabelle lint -?to see the tool options