(argv=None)
| 52 | |
| 53 | |
| 54 | def main(argv=None) -> int: |
| 55 | ap = argparse.ArgumentParser( |
| 56 | description="Generate a Lean 4 structural verification file from a YAML workflow.", |
| 57 | ) |
| 58 | ap.add_argument("yaml_path", help="Path to the YAML workflow file") |
| 59 | ap.add_argument("-o", "--output", |
| 60 | help="Output .lean path (default: <yaml>.generated.lean next to input)") |
| 61 | ap.add_argument("--prefix", default=None, |
| 62 | help="Lean definition name prefix (default: derived from workflow name)") |
| 63 | ap.add_argument("--env_file", action="append", default=[], |
| 64 | help="Load env vars from file(s) before parsing (repeatable)") |
| 65 | ap.add_argument("--save_ir", default=None, |
| 66 | help="Optional path to save the intermediate WorkflowIR JSON") |
| 67 | args = ap.parse_args(argv) |
| 68 | |
| 69 | yaml_path = Path(args.yaml_path) |
| 70 | if not yaml_path.is_file(): |
| 71 | print(f"ERROR: YAML file not found: {yaml_path}", file=sys.stderr) |
| 72 | return 1 |
| 73 | |
| 74 | # Load env files first so ${VAR} references in the YAML can resolve. |
| 75 | if args.env_file: |
| 76 | from WorkflowToLean import _load_env_file |
| 77 | for ef in args.env_file: |
| 78 | print(f"Loading env: {ef}") |
| 79 | _load_env_file(ef) |
| 80 | |
| 81 | # 1. Parse YAML → task dict |
| 82 | parser = YAMLTaskParser() |
| 83 | task_data = parser.load_task(str(yaml_path)) |
| 84 | |
| 85 | # 2. Serialize to a temporary JSON for parse_task_json to consume. |
| 86 | with tempfile.NamedTemporaryFile("w", suffix=".json", delete=False) as tf: |
| 87 | json.dump(task_data, tf, ensure_ascii=False) |
| 88 | tmp_json = tf.name |
| 89 | |
| 90 | try: |
| 91 | # 3. Build the structural WorkflowIR |
| 92 | ir = parse_task_json(tmp_json) |
| 93 | finally: |
| 94 | try: |
| 95 | os.unlink(tmp_json) |
| 96 | except OSError: |
| 97 | pass |
| 98 | |
| 99 | # 4. Derive prefix |
| 100 | prefix = args.prefix or _derive_prefix(ir.name) |
| 101 | |
| 102 | # 5. Optionally save IR |
| 103 | if args.save_ir: |
| 104 | ir.save_json(args.save_ir) |
| 105 | print(f"Saved IR: {args.save_ir}") |
| 106 | |
| 107 | # 6. Generate Lean |
| 108 | lean_src = generate_lean(ir, prefix) |
| 109 | |
| 110 | # 7. Write to output |
| 111 | out_path = Path(args.output) if args.output else yaml_path.with_suffix(".generated.lean") |
no test coverage detected