Bootstrap lean (#4)

Author: tim-br

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"