/isabelle-linter

Linter component for Isabelle.

Primary LanguageScalaMIT LicenseMIT

Isabelle Linter

status

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

NameDescriptionBundles
apply_isar_switchSwitching 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_compositionUsing apply (auto;…) results in a behavior that is hard to predict, so it is discouraged.

Reference		foundational, default
axiomatization_with_whereUnless 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 :: &quot;&apos;a ⇒ bool&quot;
where
  all_true: &quot;∀x. P x&quot; and 
all_false: &quot;∀x. ¬P x&quot;



Reference

default
bad_style_commandThis lint detects bad-style commands: back, apply_endfoundational, default, afp_mandatory
complex_isar_initial_methodInitial 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_methodInitial 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_methodWarns 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_finderThis lint detects counter-example finders with no specific purpose: nitpick, nunchaku, and quickcheck (without expect or satisfy.non_interactive_addon, afp_mandatory
diagnostic_commandThis 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, typnon_interactive_addon
force_failureSince 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_changesChanging 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_lemmaSetting 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_ruleUsing 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_attributeThis 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_chainUsing 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_finderThis lint detects proof-finder commands: sledgehammer, solve_direct, try, try0non_interactive_addon
short_nameFinds functions or definitions with short names (one character).default
smt_oracleUsing 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_proofsWhen 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_tacfoundational, default
unfinished_proofThis lint detects unfinished proofs, characterized by the following commands: sorry, &lt;proof>non_interactive_addon, afp_mandatory
unrestricted_autoUsing 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_applyThis 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_byThe 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_isarThis lint triggers on every use of the apply command and suggests to use an Isar proof instead.pedantic_addon

Bundles

Bundle NameWarningsErrors
foundationalapply_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
defaultapply_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_autoaxiomatization_with_where
pedantic_addonforce_failure, use_isar
non_interactive_addoncounter_example_finder, diagnostic_command, proof_finderunfinished_proof
afp_mandatorybad_style_command, counter_example_finder, global_attribute_on_unnamed_lemma, simplifier_isar_initial_method, smt_oracle, unfinished_proof