ix/Main.lean at main · argumentcomputer/ix · GitHub

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
--import Ix.Cli.StoreCmd
import Ix.Cli.AddrOfCmd
import Ix.Cli.AggregateCmd
import Ix.Cli.BenchReport
import Ix.Cli.CheckCmd
import Ix.Cli.CodegenCmd
import Ix.Cli.CheckRsCmd
import Ix.Cli.CheckLeanCmd
import Ix.Cli.CompileLeanCmd
import Ix.Cli.ValidateLeanCmd
import Ix.Cli.ClaimCmd
import Ix.Cli.CatalogCmd
import Ix.Cli.CompileCmd
import Ix.Cli.DecompileCmd
import Ix.Cli.DiffCmd
import Ix.Cli.IngressCmd
import Ix.Cli.MergeCmd
import Ix.Cli.NameOfCmd
import Ix.Cli.PackCmd
import Ix.Cli.ProfileCmd
import Ix.Cli.ProveCmd
import Ix.Cli.ShardCmd
import Ix.Cli.TreeCmd
import Ix.Cli.ValidateCmd
import Ix.Cli.VerifyCmd
import Ix.Cli.ServeCmd
import Ix.Cli.ConnectCmd
import Ix

def VERSION : String := Ix.versionString

def ixCmd : Cli.Cmd := `[Cli|
  ix NOOP; [VERSION]
  "A tool for generating content-addressed ZK proofs of Lean 4 code"

  SUBCOMMANDS:
    --storeCmd;
    benchCmd;
    aggregateCmd;
    catalogCmd;
    compileCmd;
    decompileCmd;
    mergeCmd;
    checkCmd;
    checkRsCmd;
    checkLeanCmd;
    compileLeanCmd;
    validateLeanCmd;
    claimCmd;
    diffCmd;
    packCmd;
    treeCmd;
    profileCmd;
    proveCmd;
    shardCmd;
    codegenCmd;
    verifyCmd;
    addrOfCmd;
    nameOfCmd;
    ingressCmd;
    validateCmd;
    serveCmd;
    connectCmd
]

def main (args : List String) : IO UInt32 := do
  if args.isEmpty then
    ixCmd.printHelp
    return 0
  ixCmd.validate args