初步构建完成

Author: maksymilan

LeanEval/__init__.py

@@ -0,0 +1,3 @@
+from prompt import SimplePromptBuilder
+from prompt import FewShotPromptBuilder
+from prompt import get_builder

LeanEval/data/json/data_2.json

@@ -0,0 +1,9 @@
+[
+    {
+        "id": "3d0b29e2-6197-422e-8a1b-97ab7b9d5c83",
+        "imports": ["Mathlib.Data.Set.Basic"],
+        "statement": "theorem subset_refl {α : Type*} (s : Set α) : s ⊆ s",
+        "extra_ctx": "",
+        "difficulty": 1
+    }
+]

LeanEval/data/jsonl/data_1.jsonl

@@ -0,0 +1,6 @@
+from .base import BaseDataset
+from .csv_dataset import CsvDataset
+from .json_dataset import JsonDataset
+from .json_dataset import JsonlDataset
+from .yaml_dataset import YamlDataset
+from .schema import LeanItem

LeanEval/datasets/__init__.py

@@ -1,4 +1,3 @@
-# csv_dataset.py
 from __future__ import annotations
 
 import csv

LeanEval/datasets/__pycache__/__init__.cpython-310.pyc

@@ -13,8 +13,17 @@ class LeanItem(BaseModel, frozen=True, extra="allow"):
     @property
     def prompt_ready_stmt(self) -> str:
         """预拼接好 imports + statement，方便 PromptBuilder 直接用"""
+        parts = []
         if self.imports:
             imports_txt = "\n".join([f"import {i}" for i in self.imports])
-        else:
-            imports_txt = ""
-        return f"{imports_txt}\n\n{self.statement}"
+            parts.append(imports_txt)
+        if self.extra_ctx:
+            parts.append(self.extra_ctx)
+        parts.append(self.statement)
+        return "\n\n".join(parts)
+    
+    @property
+    def difficulty(self) -> int:
+        """返回这道题的难度，用于评分"""
+        return self.difficulty
+