rossi-cli 0.1.3

Command-line interface for the Rossi Event-B toolchain
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
70
71
72
73

use std::process::ExitCode;

use clap::{CommandFactory, Parser, Subcommand};

mod commands {
    pub mod build;
    pub mod completions;
    pub mod eventb_io;
    pub mod export;
    pub mod fmt;
    pub mod import;
    pub mod sarif;
    pub mod validate;
}

#[derive(Parser)]
#[command(
    name = "rossi",
    version,
    propagate_version = true,
    about = "Rossi command-line tools for Event-B models"
)]
struct Cli {
    #[command(subcommand)]
    command: Command,
}

#[derive(Subcommand)]
enum Command {
    /// Validate Event-B text files or Rodin ZIP archives.
    #[command(about = "Validate Event-B model files")]
    Validate(commands::validate::ValidateArgs),
    /// Import Rodin archives (.zip/.buc/.bum/dir) into Event-B text.
    #[command(about = "Import Rodin archives into Event-B text")]
    Import(commands::import::ImportArgs),
    /// Export Event-B text (.eventb/.txt/dir) into a Rodin .zip archive.
    #[command(about = "Export Event-B text into a Rodin .zip archive")]
    Export(commands::export::ExportArgs),
    /// Reformat Event-B text/archives in place (operator convention, indentation).
    #[command(about = "Reformat Event-B text/archives in place")]
    Fmt(commands::fmt::FmtArgs),
    /// Static-check a Rodin project and emit `.bcc` / `.bcm` output.
    #[command(about = "Static-check a Rodin project and emit .bcc/.bcm output")]
    Build(commands::build::BuildArgs),
    /// Run the Rossi language server over stdio.
    #[command(about = "Run the Rossi language server over stdio")]
    Lsp,
    /// Generate a shell completion script (bash, zsh, fish, …).
    #[command(about = "Generate a shell completion script")]
    Completions(commands::completions::CompletionsArgs),
}

fn main() -> ExitCode {
    match Cli::parse().command {
        Command::Validate(args) => commands::validate::run(args),
        Command::Import(args) => commands::import::run(args),
        Command::Export(args) => commands::export::run(args),
        Command::Fmt(args) => commands::fmt::run(args),
        Command::Build(args) => commands::build::run_build_command(args),
        // The LSP brings its own runtime (with sized handler stacks); the
        // other commands are fully synchronous.
        Command::Lsp => match eventb_lsp::run_stdio_blocking() {
            Ok(()) => ExitCode::SUCCESS,
            Err(e) => {
                eprintln!("rossi lsp: {e}");
                ExitCode::from(1)
            }
        },
        // Derive the completion script from the same clap command tree the CLI
        // parses with, so it can never drift from the real interface.
        Command::Completions(args) => commands::completions::run(args, &mut Cli::command()),
    }
}