Spaces:
Sleeping
Sleeping
File size: 2,429 Bytes
16f1328 313a2ac 8c75600 313a2ac 8c75600 313a2ac 16f1328 8c75600 16f1328 8c75600 16f1328 8c75600 | 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 | from __future__ import annotations
from typing import Literal
from openenv.core.env_server.types import Action, Observation
from pydantic import BaseModel, Field, model_validator
class LeanMigrateReward(BaseModel):
score: float
cumulative_score: float
tests_passed: int | None
tests_total: int | None
proof_compiled: bool | None
breakdown: dict[str, float]
feedback: str
lean_error: str | None
class LeanMigrateAction(Action):
type: Literal["inspect", "analyze_deps", "run_tests", "submit"]
function_name: str
candidate_code: str | None = Field(
default=None,
description="Working implementation used by run_tests.",
)
target_code: str | None = Field(
default=None,
description="Final target-language implementation submitted for verification.",
)
lean_proof: str | None = Field(
default=None,
description="Proof text required only for proof tasks such as payment_saga.",
)
@model_validator(mode="after")
def _validate_payload(self) -> "LeanMigrateAction":
if self.type == "run_tests" and not self.candidate_code:
raise ValueError("run_tests actions require candidate_code")
if self.type == "submit" and not (self.target_code or self.lean_proof):
raise ValueError("submit actions require target_code or lean_proof")
return self
class InspectAction(LeanMigrateAction):
type: Literal["inspect"]
class AnalyzeDepsAction(LeanMigrateAction):
type: Literal["analyze_deps"]
class RunTestsAction(LeanMigrateAction):
type: Literal["run_tests"]
candidate_code: str
class SubmitAction(LeanMigrateAction):
type: Literal["submit"]
target_code: str | None = None
lean_proof: str | None = None
class LeanMigrateObservation(Observation):
episode_id: str
task_id: str
episode_step: int
max_steps: int
source_language: str
target_language: str
source_files: list[str]
verified: list[str]
failing: dict[str, str]
remaining: list[str]
progress: float
last_action_type: str | None
last_action_feedback: str | None
last_step_reward: float | None
reward_details: LeanMigrateReward | None = None
__all__ = [
"AnalyzeDepsAction",
"InspectAction",
"LeanMigrateAction",
"LeanMigrateObservation",
"LeanMigrateReward",
"RunTestsAction",
"SubmitAction",
]
|