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
--import Ix.Cli.StoreCmd
import Ix.Cli.AddrOfCmd
import Ix.Cli.CheckCmd
import Ix.Cli.CheckRsCmd
import Ix.Cli.ClaimCmd
import Ix.Cli.CompileCmd
import Ix.Cli.IngressCmd
import Ix.Cli.ProveCmd
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 :=
  s!"{Lean.versionString}|0.0.1"

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

  SUBCOMMANDS:
    --storeCmd;
    compileCmd;
    checkCmd;
    checkRsCmd;
    claimCmd;
    treeCmd;
    proveCmd;
    verifyCmd;
    addrOfCmd;
    ingressCmd;
    validateCmd;
    serveCmd;
    connectCmd
]

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