brrr-lint 0.1.0

A fast linter and language server for F* (FStar) with autofix capabilities
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69

//! F* linting infrastructure.

mod comments;
mod dead_code;
mod doc_checker;
mod duplicate_types;
mod effect_checker;
mod engine;
pub mod file_safety;
pub mod fix_applicator;
pub mod fix_validator;
mod import_optimizer;
mod module_deps;
mod naming;
mod output;
mod parser;
mod perf_profiler;
mod proof_hints;
mod refinement_simplifier;
mod reorder_interface;
mod rules;
mod security;
mod spec_extractor;
mod test_generator;
mod unused_opens;
mod z3_complexity;

pub use comments::CommentRule;
pub use dead_code::DeadCodeRule;
pub use doc_checker::DocCheckerRule;
pub use duplicate_types::DuplicateTypesRule;
pub use effect_checker::{Effect, EffectCheckerRule};
pub use engine::{LintConfig, LintEngine};
pub use import_optimizer::ImportOptimizerRule;
pub use module_deps::ModuleDepsRule;
pub use naming::NamingRule;
pub use output::{
    DryRunFormat, DryRunSummary, FixPreview, OutputFormat,
    print_apply_header, print_dry_run, print_dry_run_header,
    print_fixes_applied, print_no_fixes_message,
};
pub use parser::{parse_fstar_file, BlockType, DeclarationBlock};
pub use perf_profiler::PerfProfilerRule;
pub use proof_hints::ProofHintsRule;
pub use refinement_simplifier::RefinementSimplifierRule;
pub use reorder_interface::ReorderInterfaceRule;
pub use rules::{
    print_rules, DeadCodeSafetyLevel, Diagnostic, DiagnosticSeverity, Edit, Fix, FixConfidence,
    Range, Rule, RuleCode,
};
pub use security::SecurityRule;
pub use spec_extractor::SpecExtractorRule;
pub use test_generator::TestGeneratorRule;
pub use unused_opens::UnusedOpensRule;
pub use z3_complexity::Z3ComplexityRule;

// Fix validation exports
pub use fix_validator::{
    content_hash, count_declarations, find_undefined_references, validate_expected_removals,
    validate_fix, validate_fstar_syntax, validate_line_deletion, validate_no_removals,
    validate_whitespace_only_fix, DeclarationChanges, FixValidation,
};

// Fix applicator exports
pub use fix_applicator::{
    AppliedFix, CommitError, ConsoleProgressReporter, FixApplicator, FixApplicatorConfig,
    FixError, FixSummary, InteractiveChoice, InteractivePrompt, ProgressReporter, RollbackError,
    StdinInteractivePrompt,
};