Isabelle Linter

Linter for Isabelle, with jEdit integration.

Setup

Requires Isabelle >= 2021-1-RC0. The linter can be used as a stand-alone tool or as a jEdit component.

Install with: isabelle components -u <DIR>. On Windows, use the Cygwin-Terminal.

For stand-alone (cli) tool only, add the component <REPO_DIR>/linter_base instead.

Usage

Automatically starts with jEdit. On windows, start jEdit in the Cygwin-Terminal with isabelle jedit. Configuration can be done via the Linter panel and/or Isabelle options (base, jedit). Without further configuration, the default bundle is activated.

CLI usage: isabelle lint -?.

Auxiliary tools

Run with isabelle <tool> -?. Available tools:

• lint_descriptions: prints information about all lints
• lint_bundles: prints information about available bundles

Lints

Name	Description	Bundles
apply_isar_switch	Switching from an apply script to a structured Isar proof results in an overall proof that is hard to read without relying on Isabelle. The Isar proof is also sensitive to the output of the apply script, and might therefore break easily. Reference	foundational, default
auto_structural_composition	Using apply (auto;…) results in a behavior that is hard to predict, so it is discouraged. Reference	foundational, default
axiomatization_with_where	Unless when creating a new logic or extending an existing one with new axioms,the axiomatization command, when used, should not include a where clause. The problem with the where clause is that it can introduce inconsistenciesinto the logic, for example: axiomatization P :: "'a ⇒ bool" where all_true: "∀x. P x" and all_false: "∀x. ¬P x" Reference	default
bad_style_command	This lint detects bad-style commands: back, apply_end	foundational, default, afp_mandatory
complex_isar_initial_method	Initial proof methods should be kept simple, in order to keep the goals of the proof clear. For instance, not too many methods should be combined. This lint finds complex methods in proof commands. Reference	foundational, default
simplifier_isar_initial_method	Initial proof methods should not use the simplifier, in order to keep the goals of the proof clear and unchanged. Reference	foundational, default, afp_mandatory
complex_method	Warns users from using overly complex methods, i.e. if one of the following holds: has more than one modifier (?, +, or []), for example auto?[4] has three or more combinators (|, ;, ,), for example auto ; rule , (force | blast)	foundational, default
counter_example_finder	This lint detects counter-example finders with no specific purpose: nitpick, nunchaku, and quickcheck (without expect or satisfy.	non_interactive_addon, afp_mandatory
diagnostic_command	This lint finds diagnostic commands: ML_val, class_deps, code_deps, code_thms, find_consts, find_theorems, find_unused_assms, full_prf, help, locale_deps, prf, print_ML_antiquotations, print_abbrevs, print_antiquotations, print_attributes, print_bnfs, print_bundles, print_case_translations, print_cases, print_claset, print_classes, print_codeproc, print_codesetup, print_coercions, print_commands, print_context, print_definitions, print_defn_rules, print_facts, print_induct_rules, print_inductives, print_interps, print_locale, print_locales, print_methods, print_options, print_orders, print_quot_maps, print_quotconsts, print_quotients, print_quotientsQ3, print_quotmapsQ3, print_record, print_rules, print_simpset, print_state, print_statement, print_syntax, print_term_bindings, print_theorems, print_theory, print_trans_rules, smt_status, thm_deps, thm_oracles, thy_deps, unused_thms, welcome, term, prop, thm, typ	non_interactive_addon
force_failure	Since some methods do not guarantee to solve all their goals, it might be helpful to consider forcing their failure (e.g. using apply (simp; fail) instead of just apply simp) in order to make debugging proofs easier. Reference	pedantic_addon
global_attribute_changes	Changing lemma attributes (e.g. simp) to to accomodate to a local proof discouraged, as it is error-prone and might result in hard-to debug problems. Concretely, the lints warns the users of using this pattern: declare word_neq_0_conv [simp] lemma … lemma … declare word_neq_0_conv [simp del] Instead, users should use the context, notes or bundle commands. Reference	foundational, default
global_attribute_on_unnamed_lemma	Setting a global attribute (like simp or elim) on an unnamed lemma should be avoided, since it can make debugging proofs and removing the effect of that attribute harder. Reference	foundational, default, afp_mandatory
implicit_rule	Using apply rule results in Isabelle finding the suitable rule for the given context. However, if the process for finding the rule changes in the future, the proof might break. Instead, users should explicitly state which rule is needed. Reference	foundational, default
lemma_transforming_attribute	This lint warns of using transforming attributes (simplified, rule_format, andunfolded) on lemmas. Instead, the user should write the transformed form. Reference	foundational, default
low_level_apply_chain	Using long apply-scripts with low-level methods can quickly make proofs unreadable and unnecessarily long. This lints flags such scripts that are longer than 100 commands.	foundational, default
proof_finder	This lint detects proof-finder commands: sledgehammer, solve_direct, try, try0	non_interactive_addon
short_name	Finds functions or definitions with short names (one character).	default
smt_oracle	Using declare [[smt_oracle]] will make all smt act as an oracle. This might prove to be problematic, as oracle proofs are usually not to be trusted.	default, afp_mandatory
tactic_proofs	When using tactics, avoid outdated induct_tac, and do not refer to system-generated names. The lints warns about using the following methods: induct_tac, rule_tac, case_tac	foundational, default
unfinished_proof	This lint detects unfinished proofs, characterized by the following commands: sorry, <proof>	non_interactive_addon, afp_mandatory
unrestricted_auto	Using auto in the middle of a proof on all goals (i.e. unrestricted) might produce an unpredictable proof state. It should rather be used as a terminal proof method, or be restricted to a set of goals that it fully solves. Reference	foundational, default
use_apply	This lint is the inverse direction of the use_by lint: it identifies usages of the by command and suggests toexpand the methods. As an example, it helps transform lemma … by (induction xs) auto into lemma … apply (induction xs) apply auto done
use_by	The by command allows to express method applications using apply more concisely. For example, instead of lemma … apply (induction xs) apply auto done bycan be used: lemma … by (induction xs) auto
use_isar	This lint triggers on every use of the apply command and suggests to use an Isar proof instead.	pedantic_addon

Bundles

Bundle Name	Warnings	Errors
foundational	apply_isar_switch, auto_structural_composition, bad_style_command, complex_isar_initial_method, complex_method, global_attribute_changes, global_attribute_on_unnamed_lemma, implicit_rule, lemma_transforming_attribute, low_level_apply_chain, simplifier_isar_initial_method, tactic_proofs, unrestricted_auto
default	apply_isar_switch, auto_structural_composition, bad_style_command, complex_isar_initial_method, complex_method, global_attribute_changes, global_attribute_on_unnamed_lemma, implicit_rule, lemma_transforming_attribute, low_level_apply_chain, short_name, simplifier_isar_initial_method, smt_oracle, tactic_proofs, unrestricted_auto	axiomatization_with_where
pedantic_addon	force_failure, use_isar
non_interactive_addon	counter_example_finder, diagnostic_command, proof_finder	unfinished_proof
afp_mandatory		bad_style_command, counter_example_finder, global_attribute_on_unnamed_lemma, simplifier_isar_initial_method, smt_oracle, unfinished_proof