From dd2087cd2765ca82ed2e0d8da0f88f45f28accd7 Mon Sep 17 00:00:00 2001 From: Samuel Burnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 5 Feb 2025 10:43:31 -0500 Subject: [PATCH 1/4] feat: CLI stubs for `hash` and `prove` --- Ix.lean | 2 ++ Ix/Cli/HashCmd.lean | 17 +++++++++++++++++ Ix/Cli/ProveCmd.lean | 17 +++++++++++++++++ Main.lean | 21 +++++++++++++++++++-- lake-manifest.json | 12 +++++++++++- lakefile.lean | 3 +++ 6 files changed, 69 insertions(+), 3 deletions(-) create mode 100644 Ix/Cli/HashCmd.lean create mode 100644 Ix/Cli/ProveCmd.lean diff --git a/Ix.lean b/Ix.lean index a690d1bb..2f797c48 100644 --- a/Ix.lean +++ b/Ix.lean @@ -2,4 +2,6 @@ -- Import modules here that should be built as part of the library. import Ix.Basic import Ix.Ixon +import Ix.Cli.ProveCmd +import Ix.Cli.HashCmd diff --git a/Ix/Cli/HashCmd.lean b/Ix/Cli/HashCmd.lean new file mode 100644 index 00000000..e8f5bb92 --- /dev/null +++ b/Ix/Cli/HashCmd.lean @@ -0,0 +1,17 @@ +import Cli + +def runHash (p : Cli.Parsed) : IO UInt32 := do + let input : String := p.positionalArg! "input" |>.as! String + IO.println <| "Input: " ++ input + return 0 + +def hashCmd : Cli.Cmd := `[Cli| + hash VIA runHash; + "Hashes a given Lean source file" + + FLAGS: + e, "example" : String; "Example flag" + + ARGS: + input : String; "Source file input" +] diff --git a/Ix/Cli/ProveCmd.lean b/Ix/Cli/ProveCmd.lean new file mode 100644 index 00000000..a1f40698 --- /dev/null +++ b/Ix/Cli/ProveCmd.lean @@ -0,0 +1,17 @@ +import Cli + +def runProve (p : Cli.Parsed) : IO UInt32 := do + let input : String := p.positionalArg! "input" |>.as! String + IO.println <| "Input: " ++ input + return 0 + +def proveCmd : Cli.Cmd := `[Cli| + prove VIA runProve; + "Generates a ZK proof of a given Lean source file" + + FLAGS: + e, "example" : String; "Example flag" + + ARGS: + input : String; "Source file input" +] diff --git a/Main.lean b/Main.lean index adc9b301..cc0be443 100644 --- a/Main.lean +++ b/Main.lean @@ -1,4 +1,21 @@ import Ix +--import Ix.Cli.ProveCmd +--import Ix.Cli.HashCmd -def main (args : List String) : IO Unit := - IO.println s!"Hello, {args}!" +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: + proveCmd; + hashCmd +] + +def main (args : List String) : IO UInt32 := + --if args.isEmpty then + -- ixCmd.printHelp + --else + ixCmd.validate args diff --git a/lake-manifest.json b/lake-manifest.json index 12ad7779..74f4dc57 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,7 +1,17 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/argumentcomputer/LSpec", + [{"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "", + "rev": "27f69ad2b2b88fb0844b1c17624576a3654a335e", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "27f69ad2b2b88fb0844b1c17624576a3654a335e", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/argumentcomputer/LSpec", "type": "git", "subDir": null, "scope": "", diff --git a/lakefile.lean b/lakefile.lean index 19e83ec0..17565683 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -13,6 +13,9 @@ lean_exe ix where require LSpec from git "https://github.com/argumentcomputer/LSpec" @ "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec" +require Cli from git + "https://github.com/leanprover/lean4-cli" @ "27f69ad2b2b88fb0844b1c17624576a3654a335e" + section Tests lean_exe Tests.Blake3 From f48c749fcae3cec680f3e69521ea23495ea83388 Mon Sep 17 00:00:00 2001 From: Samuel Burnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 5 Feb 2025 10:50:31 -0500 Subject: [PATCH 2/4] Fixup --- Main.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Main.lean b/Main.lean index cc0be443..7030f293 100644 --- a/Main.lean +++ b/Main.lean @@ -14,8 +14,8 @@ def ixCmd : Cli.Cmd := `[Cli| hashCmd ] -def main (args : List String) : IO UInt32 := - --if args.isEmpty then - -- ixCmd.printHelp - --else +def main (args : List String) : IO UInt32 := do + if args.isEmpty then + ixCmd.printHelp + return 0 ixCmd.validate args From 0a07df81a11c7c3bcb80161fb02d4f4f40f4e0b6 Mon Sep 17 00:00:00 2001 From: Samuel Burnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 5 Feb 2025 11:11:44 -0500 Subject: [PATCH 3/4] Bump `Cli` rev --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 74f4dc57..582f4664 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "27f69ad2b2b88fb0844b1c17624576a3654a335e", + "rev": "efa5aa20504b88e2826032ddaa606c7965ec9467", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "27f69ad2b2b88fb0844b1c17624576a3654a335e", + "inputRev": "efa5aa20504b88e2826032ddaa606c7965ec9467", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/argumentcomputer/LSpec", diff --git a/lakefile.lean b/lakefile.lean index 17565683..ec7c1d68 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -14,7 +14,7 @@ require LSpec from git "https://github.com/argumentcomputer/LSpec" @ "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec" require Cli from git - "https://github.com/leanprover/lean4-cli" @ "27f69ad2b2b88fb0844b1c17624576a3654a335e" + "https://github.com/leanprover/lean4-cli" @ "efa5aa20504b88e2826032ddaa606c7965ec9467" section Tests From 2295b7aa696f1b2e67ffe2d97b07c7c327113ee1 Mon Sep 17 00:00:00 2001 From: Samuel Burnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 5 Feb 2025 13:06:31 -0500 Subject: [PATCH 4/4] Address review --- Ix.lean | 2 -- Main.lean | 5 ++--- 2 files changed, 2 insertions(+), 5 deletions(-) diff --git a/Ix.lean b/Ix.lean index 2f797c48..a690d1bb 100644 --- a/Ix.lean +++ b/Ix.lean @@ -2,6 +2,4 @@ -- Import modules here that should be built as part of the library. import Ix.Basic import Ix.Ixon -import Ix.Cli.ProveCmd -import Ix.Cli.HashCmd diff --git a/Main.lean b/Main.lean index 7030f293..9f1db352 100644 --- a/Main.lean +++ b/Main.lean @@ -1,6 +1,5 @@ -import Ix ---import Ix.Cli.ProveCmd ---import Ix.Cli.HashCmd +import Ix.Cli.ProveCmd +import Ix.Cli.HashCmd def VERSION : String := s!"{Lean.versionString}|0.0.1"