oxilean-cli 0.1.0

OxiLean command-line interface
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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95

# oxilean-cli

[![Crates.io](https://img.shields.io/crates/v/oxilean-cli.svg)](https://crates.io/crates/oxilean-cli)
[![Docs.rs](https://docs.rs/oxilean-cli/badge.svg)](https://docs.rs/oxilean-cli)

> **Command-line interface for the OxiLean theorem prover**

The CLI provides the user-facing entry point for checking proofs, running the REPL, and managing OxiLean projects.

64,163 SLOC -- fully implemented CLI with argument parsing, subcommand dispatch, file checking, and interactive REPL.

## Usage

```bash
# Show version
oxilean --version
oxilean -v

# Show help
oxilean --help
oxilean -h

# Check a file
oxilean check file.oxilean

# Start interactive REPL
oxilean repl
```

## Commands

| Command | Status | Description |
|---------|--------|-------------|
| `check <file>` | Implemented | Type-check an `.oxilean` source file |
| `repl` | Implemented | Interactive proof REPL |
| `--version` / `-v` | Implemented | Print version information |
| `--help` / `-h` | Implemented | Print usage information |

## Architecture

```
CLI Argument Parsing
    |
    +-- "check" <file>
    |       |
    |       +-- Read file
    |       +-- Lex -> Token stream       (oxilean-parse)
    |       +-- Parse -> Surface AST       (oxilean-parse)
    |       +-- Elaborate -> Kernel Exprs  (oxilean-elab)
    |       +-- Type-check via Kernel      (oxilean-kernel)
    |       +-- Report success / errors
    |
    +-- "repl"
    |       |
    |       +-- Interactive loop:
    |           +-- Read input
    |           +-- Parse + Elaborate
    |           +-- Display goals / results
    |           +-- Accept tactic commands
    |
    +-- "--version"
    |       +-- Print version string
    |
    +-- "--help"
            +-- Print usage information
```

## Dependencies

- `oxilean-kernel` -- core type checking
- `oxilean-parse` -- lexing and parsing
- `oxilean-elab` -- elaboration and tactics

## Building

```bash
# Build the CLI binary
cargo build -p oxilean-cli

# Build in release mode
cargo build -p oxilean-cli --release

# Run directly
cargo run --bin oxilean -- --version
```

## Testing

```bash
cargo test -p oxilean-cli
```

## License

Copyright COOLJAPAN OU (Team Kitasan). Apache-2.0 -- See [LICENSE](../../LICENSE) for details.