Bootstrap lean

Dockerfile

@@ -1,8 +1,22 @@
-FROM alpine:3.18
+FROM debian:bookworm-slim
 
-# install packages required to run the tests
-RUN apk add --no-cache jq coreutils
+RUN apt-get update && apt-get install -y --no-install-recommends \
+    curl \
+    ca-certificates \
+    git \
+    jq \
+    && rm -rf /var/lib/apt/lists/*
+
+ENV ELAN_HOME=/usr/local/elan
+ENV PATH="${ELAN_HOME}/bin:${PATH}"
+
+RUN curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --no-modify-path --default-toolchain leanprover/lean4:v4.25.2 \
+    && elan default leanprover/lean4:v4.25.2 \
+    && lean --version \
+    && rm -rf ${ELAN_HOME}/downloads/* /tmp/* /var/tmp/*
 
 WORKDIR /opt/test-runner
-COPY . .
+
+COPY bin/ bin/
+
 ENTRYPOINT ["/opt/test-runner/bin/run.sh"]

bin/run-in-docker.sh

@@ -42,5 +42,5 @@ docker run \
     --read-only \
     --mount type=bind,src="${solution_dir}",dst=/solution \
     --mount type=bind,src="${output_dir}",dst=/output \
-    --mount type=tmpfs,dst=/tmp \
+    --tmpfs /tmp:exec \
     exercism/lean-test-runner "${slug}" /solution /output 

bin/run-tests-in-docker.sh

@@ -24,7 +24,7 @@ docker run \
     --network none \
     --read-only \
     --mount type=bind,src="${PWD}/tests",dst=/opt/test-runner/tests \
-    --mount type=tmpfs,dst=/tmp \
+    --tmpfs /tmp:exec \
     --volume "${PWD}/bin/run-tests.sh:/opt/test-runner/bin/run-tests.sh" \
     --workdir /opt/test-runner \
     --entrypoint /opt/test-runner/bin/run-tests.sh \

bin/run-tests.sh

@@ -1,7 +1,7 @@
 #!/usr/bin/env sh
 
 # Synopsis:
-# Test the test runner by running it against a predefined set of solutions 
+# Test the test runner by running it against a predefined set of solutions
 # with an expected output.
 
 # Output:
@@ -20,17 +20,19 @@ for test_dir in tests/*; do
 
     bin/run.sh "${test_dir_name}" "${test_dir_path}" "${test_dir_path}"
 
-    # OPTIONAL: Normalize the results file
-    # If the results.json file contains information that changes between 
-    # different test runs (e.g. timing information or paths), you should normalize
-    # the results file to allow the diff comparison below to work as expected
-
     file="results.json"
     expected_file="expected_${file}"
     echo "${test_dir_name}: comparing ${file} to ${expected_file}"
 
-    if ! diff "${test_dir_path}/${file}" "${test_dir_path}/${expected_file}"; then
+    # Compare status field (must match exactly)
+    actual_status=$(jq -r '.status' "${test_dir_path}/${file}")
+    expected_status=$(jq -r '.status' "${test_dir_path}/${expected_file}")
+
+    if [ "${actual_status}" != "${expected_status}" ]; then
+        echo "Status mismatch: expected '${expected_status}', got '${actual_status}'"
         exit_code=1
+    else
+        echo "${test_dir_name}: status OK (${actual_status})"
     fi
 done
 

bin/run.sh

@@ -31,30 +31,30 @@ mkdir -p "${output_dir}"
 
 echo "${slug}: testing..."
 
+# Copy solution to a writable temp directory (lake needs to write build files)
+tmp_dir=$(mktemp -d)
+cp -r "${solution_dir}/." "${tmp_dir}"
+cd "${tmp_dir}"
+
 # Run the tests for the provided implementation file and redirect stdout and
 # stderr to capture it
-test_output=$(false)
-# TODO: substitute "false" with the actual command to run the test:
-# test_output=$(command_to_run_tests 2>&1)
+test_output=$(lake test 2>&1)
+exit_code=$?
+
+# Clean up temp directory
+rm -rf "${tmp_dir}"
 
-# Write the results.json file based on the exit code of the command that was 
+# Write the results.json file based on the exit code of the command that was
 # just executed that tested the implementation file
-if [ $? -eq 0 ]; then
+if [ ${exit_code} -eq 0 ]; then
     jq -n '{version: 1, status: "pass"}' > ${results_file}
 else
-    # OPTIONAL: Sanitize the output
-    # In some cases, the test output might be overly verbose, in which case stripping
-    # the unneeded information can be very helpful to the student
-    # sanitized_test_output=$(printf "${test_output}" | sed -n '/Test results:/,$p')
-
-    # OPTIONAL: Manually add colors to the output to help scanning the output for errors
-    # If the test output does not contain colors to help identify failing (or passing)
-    # tests, it can be helpful to manually add colors to the output
-    # colorized_test_output=$(echo "${test_output}" \
-    #      | GREP_COLOR='01;31' grep --color=always -E -e '^(ERROR:.*|.*failed)$|$' \
-    #      | GREP_COLOR='01;32' grep --color=always -E -e '^.*passed$|$')
-
-    jq -n --arg output "${test_output}" '{version: 1, status: "fail", message: $output}' > ${results_file}
+    # Check if this is a compilation/syntax error vs test failure
+    if echo "${test_output}" | grep -q "error:"; then
+        jq -n --arg output "${test_output}" '{version: 1, status: "error", message: $output}' > ${results_file}
+    else
+        jq -n --arg output "${test_output}" '{version: 1, status: "fail", message: $output}' > ${results_file}
+    fi
 fi
 
 echo "${slug}: done"

tests/all-fail/HelloWorld.lean

@@ -0,0 +1,6 @@
+namespace HelloWorld
+
+def hello : String :=
+  "Goodbye, World!"
+
+end HelloWorld

tests/all-fail/HelloWorldTest.lean

@@ -0,0 +1,12 @@
+import LeanTest
+import HelloWorld
+
+open LeanTest
+
+def helloWorldTests : TestSuite :=
+  (TestSuite.empty "HelloWorld")
+  |>.addTest "Say Hi!" (do
+      return assertEqual "Hello, World!" HelloWorld.hello)
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [helloWorldTests]

tests/all-fail/expected_results.json

@@ -1,5 +1,4 @@
 {
   "version": 1,
-  "status": "fail",
-  "message": "TODO: replace with correct output"
+  "status": "fail"
 }

tests/all-fail/lake-manifest.json

@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "«hello-world»",
+ "lakeDir": ".lake"}

tests/all-fail/lakefile.toml

@@ -0,0 +1,15 @@
+name = "hello-world"
+version = "0.1.0"
+defaultTargets = ["HelloWorldTest"]
+testDriver = "HelloWorldTest"
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "HelloWorld"
+
+[[lean_exe]]
+name = "HelloWorldTest"
+root = "HelloWorldTest"

tests/all-fail/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.25.2

tests/all-fail/vendor/LeanTest/LeanTest.lean

@@ -0,0 +1,5 @@
+-- This module serves as the root of the `LeanTest` library.
+-- Import modules here that should be built as part of the library.
+import LeanTest.Assertions
+import LeanTest.Test
+import LeanTest.Basic

tests/all-fail/vendor/LeanTest/LeanTest/Assertions.lean

@@ -0,0 +1,166 @@
+/-
+Assertion functions for unit testing.
+-/
+
+namespace LeanTest
+
+/-- Result of a test assertion -/
+inductive AssertionResult where
+  | success : AssertionResult
+  | failure (message : String) : AssertionResult
+  deriving Repr, BEq
+
+namespace AssertionResult
+
+def isSuccess : AssertionResult → Bool
+  | success => true
+  | failure _ => false
+
+def getMessage : AssertionResult → String
+  | success => "Assertion passed"
+  | failure msg => msg
+
+end AssertionResult
+
+/-- Assert that a boolean condition is true -/
+def assert (condition : Bool) (message : String := "Assertion failed") : AssertionResult :=
+  if condition then
+    .success
+  else
+    .failure message
+
+/-- Assert that two values are equal -/
+def assertEqual [BEq α] [Repr α] (expected : α) (actual : α) (message : String := "") : AssertionResult :=
+  if expected == actual then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected: {repr expected}\nActual: {repr actual}"
+    else
+      s!"{message}\nExpected: {repr expected}\nActual: {repr actual}"
+    .failure msg
+
+/-- Assert that two values are not equal -/
+def assertNotEqual [BEq α] [Repr α] (expected : α) (actual : α) (message : String := "") : AssertionResult :=
+  if expected != actual then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected values to be different, but both were: {repr expected}"
+    else
+      s!"{message}\nExpected values to be different, but both were: {repr expected}"
+    .failure msg
+
+/-- Refute that a boolean condition is true (assert it's false) -/
+def refute (condition : Bool) (message : String := "Refute failed - condition was true") : AssertionResult :=
+  if !condition then
+    .success
+  else
+    .failure message
+
+/-- Assert that a value is true -/
+def assertTrue (value : Bool) (message : String := "Expected true but got false") : AssertionResult :=
+  assert value message
+
+/-- Assert that a value is false -/
+def assertFalse (value : Bool) (message : String := "Expected false but got true") : AssertionResult :=
+  refute value message
+
+/-- Assert that an Option is some -/
+def assertSome [Repr α] (opt : Option α) (message : String := "Expected Some but got None") : AssertionResult :=
+  match opt with
+  | some _ => .success
+  | none => .failure message
+
+/-- Assert that an Option is none -/
+def assertNone [Repr α] (opt : Option α) (message : String := "") : AssertionResult :=
+  match opt with
+  | none => .success
+  | some val =>
+    let msg := if message.isEmpty then
+      s!"Expected None but got Some: {repr val}"
+    else
+      s!"{message}\nExpected None but got Some: {repr val}"
+    .failure msg
+
+/-- Assert that a list is empty -/
+def assertEmpty [Repr α] (list : List α) (message : String := "") : AssertionResult :=
+  match list with
+  | [] => .success
+  | _ =>
+    let msg := if message.isEmpty then
+      s!"Expected empty list but got: {repr list}"
+    else
+      s!"{message}\nExpected empty list but got: {repr list}"
+    .failure msg
+
+/-- Assert that a list contains an element -/
+def assertContains [BEq α] [Repr α] (list : List α) (element : α) (message : String := "") : AssertionResult :=
+  if list.contains element then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected list to contain {repr element}\nList: {repr list}"
+    else
+      s!"{message}\nExpected list to contain {repr element}\nList: {repr list}"
+    .failure msg
+
+/-- Assert that a value is within a range (inclusive) -/
+def assertInRange [LE α] [DecidableRel (· ≤ · : α → α → Prop)] [Repr α]
+    (value : α) (min : α) (max : α) (message : String := "") : AssertionResult :=
+  if min ≤ value ∧ value ≤ max then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected {repr value} to be in range [{repr min}, {repr max}]"
+    else
+      s!"{message}\nExpected {repr value} to be in range [{repr min}, {repr max}]"
+    .failure msg
+
+/-- Assert that an Except value is an error -/
+def assertError [Repr ε] [Repr α] (result : Except ε α) (message : String := "") : AssertionResult :=
+  match result with
+  | .error _ => .success
+  | .ok val =>
+    let msg := if message.isEmpty then
+      s!"Expected error but got Ok: {repr val}"
+    else
+      s!"{message}\nExpected error but got Ok: {repr val}"
+    .failure msg
+
+/-- Assert that an Except value is ok -/
+def assertOk [Repr ε] [Repr α] (result : Except ε α) (message : String := "") : AssertionResult :=
+  match result with
+  | .ok _ => .success
+  | .error err =>
+    let msg := if message.isEmpty then
+      s!"Expected Ok but got error: {repr err}"
+    else
+      s!"{message}\nExpected Ok but got error: {repr err}"
+    .failure msg
+
+/-- Assert that an IO action throws an error -/
+def assertThrows (action : IO α) (message : String := "") : IO AssertionResult := do
+  try
+    let _ ← action
+    let msg := if message.isEmpty then
+      "Expected IO action to throw an error, but it succeeded"
+    else
+      s!"{message}\nExpected IO action to throw an error, but it succeeded"
+    return .failure msg
+  catch _ =>
+    return .success
+
+/-- Assert that an IO action succeeds (doesn't throw) -/
+def assertSucceeds (action : IO α) (message : String := "") : IO AssertionResult := do
+  try
+    let _ ← action
+    return .success
+  catch e =>
+    let msg := if message.isEmpty then
+      s!"Expected IO action to succeed, but it threw: {e}"
+    else
+      s!"{message}\nExpected IO action to succeed, but it threw: {e}"
+    return .failure msg
+
+end LeanTest

tests/all-fail/vendor/LeanTest/LeanTest/Basic.lean

@@ -0,0 +1 @@
+def hello := "world"