Initial commit

Author: TwoFX

.github/workflows/lean_action_ci.yml

@@ -0,0 +1,14 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1

.gitignore

@@ -0,0 +1 @@
+/.lake

.vscode/settings.json

@@ -0,0 +1,5 @@
+{
+    "editor.rulers": [
+        100
+    ]
+}

CreateScaffold.lean

@@ -0,0 +1,40 @@
+import Lean.Data.Json.FromToJson
+import Lean.Data.Json.Parser
+
+namespace HumanEvalLean.CreateScaffold
+
+structure Task where
+  task_id : String
+  prompt : String
+  entry_point : String
+  canonical_solution : String
+  test : String
+deriving Repr, Lean.FromJson
+
+def Task.num? (t : Task) : Option Nat :=
+  t.task_id.dropPrefix? "HumanEval/" |>.map (·.toString) |>.bind String.toNat?
+
+instance : ToString Task where
+  toString t := repr t |>.pretty
+
+def readFile (filename : System.FilePath) : IO (List Task) := do
+  let lines := (← IO.FS.readFile filename).splitOn "\n" |>.filter (fun l => !l.isEmpty)
+  lines.mapM fun line => IO.ofExcept (Lean.Json.parse line >>= Lean.FromJson.fromJson?)
+
+def createScaffoldForTask (t : Task) : IO Unit := do
+  let some num := t.num? | throw (IO.userError "ill-formed task id")
+  let fileName := s!"HumanEvalLean/HumanEval{num}.lean"
+  let content := s!"def {t.entry_point} : Unit :=\n  ()\n\n/-!\n## Prompt\n\n```python3\n{t.prompt}```\n\n## Canonical solution\n\n```python3\n{t.canonical_solution}```\n\n## Tests\n\n```python3\n{t.test}```\n-/"
+  IO.FS.writeFile fileName content
+
+def createScaffold (filename : String) : IO Unit := do
+  let tasks ← HumanEvalLean.CreateScaffold.readFile filename
+  tasks.forM createScaffoldForTask
+
+end HumanEvalLean.CreateScaffold
+
+def main (args : List String) : IO Unit := do
+  if let [filename] := args then do
+    HumanEvalLean.CreateScaffold.createScaffold filename
+  else
+    IO.println "Expected exactly one argument with a filename"

HumanEvalLean.lean

@@ -0,0 +1,55 @@
+def has_close_elements : Unit :=
+  ()
+
+/-!
+## Prompt
+
+```python3
+from typing import List
+
+
+def has_close_elements(numbers: List[float], threshold: float) -> bool:
+    """ Check if in given list of numbers, are any two numbers closer to each other than
+    given threshold.
+    >>> has_close_elements([1.0, 2.0, 3.0], 0.5)
+    False
+    >>> has_close_elements([1.0, 2.8, 3.0, 4.0, 5.0, 2.0], 0.3)
+    True
+    """
+```
+
+## Canonical solution
+
+```python3
+    for idx, elem in enumerate(numbers):
+        for idx2, elem2 in enumerate(numbers):
+            if idx != idx2:
+                distance = abs(elem - elem2)
+                if distance < threshold:
+                    return True
+
+    return False
+```
+
+## Tests
+
+```python3
+
+
+METADATA = {
+    'author': 'jt',
+    'dataset': 'test'
+}
+
+
+def check(candidate):
+    assert candidate([1.0, 2.0, 3.9, 4.0, 5.0, 2.2], 0.3) == True
+    assert candidate([1.0, 2.0, 3.9, 4.0, 5.0, 2.2], 0.05) == False
+    assert candidate([1.0, 2.0, 5.9, 4.0, 5.0], 0.95) == True
+    assert candidate([1.0, 2.0, 5.9, 4.0, 5.0], 0.8) == False
+    assert candidate([1.0, 2.0, 3.0, 4.0, 5.0, 2.0], 0.1) == True
+    assert candidate([1.1, 2.2, 3.1, 4.1, 5.1], 1.0) == True
+    assert candidate([1.1, 2.2, 3.1, 4.1, 5.1], 0.5) == False
+
+```
+-/

HumanEvalLean/HumanEval0.lean

@@ -0,0 +1,66 @@
+def separate_paren_groups : Unit :=
+  ()
+
+/-!
+## Prompt
+
+```python3
+from typing import List
+
+
+def separate_paren_groups(paren_string: str) -> List[str]:
+    """ Input to this function is a string containing multiple groups of nested parentheses. Your goal is to
+    separate those group into separate strings and return the list of those.
+    Separate groups are balanced (each open brace is properly closed) and not nested within each other
+    Ignore any spaces in the input string.
+    >>> separate_paren_groups('( ) (( )) (( )( ))')
+    ['()', '(())', '(()())']
+    """
+```
+
+## Canonical solution
+
+```python3
+    result = []
+    current_string = []
+    current_depth = 0
+
+    for c in paren_string:
+        if c == '(':
+            current_depth += 1
+            current_string.append(c)
+        elif c == ')':
+            current_depth -= 1
+            current_string.append(c)
+
+            if current_depth == 0:
+                result.append(''.join(current_string))
+                current_string.clear()
+
+    return result
+```
+
+## Tests
+
+```python3
+
+
+METADATA = {
+    'author': 'jt',
+    'dataset': 'test'
+}
+
+
+def check(candidate):
+    assert candidate('(()()) ((())) () ((())()())') == [
+        '(()())', '((()))', '()', '((())()())'
+    ]
+    assert candidate('() (()) ((())) (((())))') == [
+        '()', '(())', '((()))', '(((())))'
+    ]
+    assert candidate('(()(())((())))') == [
+        '(()(())((())))'
+    ]
+    assert candidate('( ) (( )) (( )( ))') == ['()', '(())', '(()())']
+```
+-/

HumanEvalLean/HumanEval1.lean

@@ -0,0 +1,61 @@
+def make_palindrome : Unit :=
+  ()
+
+/-!
+## Prompt
+
+```python3
+
+
+def is_palindrome(string: str) -> bool:
+    """ Test if given string is a palindrome """
+    return string == string[::-1]
+
+
+def make_palindrome(string: str) -> str:
+    """ Find the shortest palindrome that begins with a supplied string.
+    Algorithm idea is simple:
+    - Find the longest postfix of supplied string that is a palindrome.
+    - Append to the end of the string reverse of a string prefix that comes before the palindromic suffix.
+    >>> make_palindrome('')
+    ''
+    >>> make_palindrome('cat')
+    'catac'
+    >>> make_palindrome('cata')
+    'catac'
+    """
+```
+
+## Canonical solution
+
+```python3
+    if not string:
+        return ''
+
+    beginning_of_suffix = 0
+
+    while not is_palindrome(string[beginning_of_suffix:]):
+        beginning_of_suffix += 1
+
+    return string + string[:beginning_of_suffix][::-1]
+```
+
+## Tests
+
+```python3
+
+
+METADATA = {
+    'author': 'jt',
+    'dataset': 'test'
+}
+
+
+def check(candidate):
+    assert candidate('') == ''
+    assert candidate('x') == 'x'
+    assert candidate('xyz') == 'xyzyx'
+    assert candidate('xyx') == 'xyx'
+    assert candidate('jerry') == 'jerryrrej'
+```
+-/

HumanEvalLean/HumanEval10.lean

@@ -0,0 +1,47 @@
+def make_a_pile : Unit :=
+  ()
+
+/-!
+## Prompt
+
+```python3
+
+def make_a_pile(n):
+    """
+    Given a positive integer n, you have to make a pile of n levels of stones.
+    The first level has n stones.
+    The number of stones in the next level is:
+        - the next odd number if n is odd.
+        - the next even number if n is even.
+    Return the number of stones in each level in a list, where element at index
+    i represents the number of stones in the level (i+1).
+
+    Examples:
+    >>> make_a_pile(3)
+    [3, 5, 7]
+    """
+```
+
+## Canonical solution
+
+```python3
+    return [n + 2*i for i in range(n)]
+```
+
+## Tests
+
+```python3
+def check(candidate):
+
+    # Check some simple cases
+    assert candidate(3) == [3, 5, 7], "Test 3"
+    assert candidate(4) == [4,6,8,10], "Test 4"
+    assert candidate(5) == [5, 7, 9, 11, 13]
+    assert candidate(6) == [6, 8, 10, 12, 14, 16]
+    assert candidate(8) == [8, 10, 12, 14, 16, 18, 20, 22]
+
+    # Check some edge cases that are easy to work out by hand.
+    assert True, "This prints if this assert fails 2 (also good for debugging!)"
+
+```
+-/

HumanEvalLean/HumanEval100.lean

@@ -0,0 +1,56 @@
+def words_string : Unit :=
+  ()
+
+/-!
+## Prompt
+
+```python3
+
+def words_string(s):
+    """
+    You will be given a string of words separated by commas or spaces. Your task is
+    to split the string into words and return an array of the words.
+    
+    For example:
+    words_string("Hi, my name is John") == ["Hi", "my", "name", "is", "John"]
+    words_string("One, two, three, four, five, six") == ["One", "two", "three", "four", "five", "six"]
+    """
+```
+
+## Canonical solution
+
+```python3
+    if not s:
+        return []
+
+    s_list = []
+
+    for letter in s:
+        if letter == ',':
+            s_list.append(' ')
+        else:
+            s_list.append(letter)
+
+    s_list = "".join(s_list)
+    return s_list.split()
+```
+
+## Tests
+
+```python3
+def check(candidate):
+
+    # Check some simple cases
+    assert True, "This prints if this assert fails 1 (good for debugging!)"
+    assert candidate("Hi, my name is John") == ["Hi", "my", "name", "is", "John"]
+    assert candidate("One, two, three, four, five, six") == ["One", "two", "three", "four", "five", "six"]
+    assert candidate("Hi, my name") == ["Hi", "my", "name"]
+    assert candidate("One,, two, three, four, five, six,") == ["One", "two", "three", "four", "five", "six"]
+
+    # Check some edge cases that are easy to work out by hand.
+    assert True, "This prints if this assert fails 2 (also good for debugging!)"
+    assert candidate("") == []
+    assert candidate("ahmed     , gamal") == ["ahmed", "gamal"]
+
+```
+-/