run tests in CI

.github/workflows/ci.yml

@@ -0,0 +1,24 @@
+name: Run Tests
+
+on: [push, pull_request]
+
+jobs:
+  test:
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Checkout code
+      uses: actions/checkout@v2
+
+    - name: install elan
+      run: |
+        set -o pipefail
+        curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+        ./elan-init -y --default-toolchain none
+        echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+    - name: build
+      run: lake build
+
+    - name: Run tests
+      run: ./test.sh

.vscode/copyright.code-snippets

@@ -0,0 +1,13 @@
+{
+	"Copyright header for mathlib": {
+		"scope": "lean4",
+		"prefix": "copyright",
+		"body": [
+			"/-",
+			"Copyright (c) ${CURRENT_YEAR} $1. All rights reserved.",
+			"Released under Apache 2.0 license as described in the file LICENSE.",
+			"Authors: $1",
+			"-/"
+		]
+	}
+}

.vscode/extensions.json

@@ -0,0 +1,13 @@
+{
+	// See https://go.microsoft.com/fwlink/?LinkId=827846 to learn about workspace recommendations.
+	// Extension identifier format: ${publisher}.${name}. Example: vscode.csharp
+
+	// List of extensions which should be recommended for users of this workspace.
+	"recommendations": [
+		"leanprover.lean4"
+	],
+	// List of extensions recommended by VS Code that should not be recommended for users of this workspace.
+	"unwantedRecommendations": [
+		"ms-vscode-remote.remote-containers"
+	]
+}

.vscode/module-docstring.code-snippets

@@ -0,0 +1,35 @@
+{
+	"Module docstring for mathlib": {
+		"scope": "lean4",
+		"prefix": "module docstring",
+		"body": [
+			"/-!",
+      "# ${TM_FILENAME_BASE/([^_]*)(_?)/${1:/capitalize}${2:+ }/g}",
+			"",
+			"## Main definitions",
+			"",
+			"* `FooBar`",
+			"",
+			"## Main statements",
+			"",
+			"* `fooBar_unique`",
+			"",
+			"## Notation",
+			"",
+			"",
+			"",
+			"## Implementation details",
+			"",
+			"",
+			"",
+			"## References",
+			"",
+			"* [F. Bar, *Quuxes*][bibkey]",
+			"",
+			"## Tags",
+			"",
+			"Foobars, barfoos",
+			"-/",
+			"",
+		]},
+}

.vscode/settings.json

@@ -0,0 +1,10 @@
+{
+  "editor.insertSpaces": true,
+  "editor.tabSize": 2,
+  "editor.rulers" : [100],
+  "files.encoding": "utf8",
+  "files.eol": "\n",
+  "files.insertFinalNewline": true,
+  "files.trimFinalNewlines": true,
+  "files.trimTrailingWhitespace": true,
+}

test.sh

@@ -0,0 +1,34 @@
+#!/bin/bash
+
+# Define the paths
+IN_DIR="test"
+EXPECTED_DIR="test"
+
+# Iterate over each .in file in the test directory
+for infile in $IN_DIR/*.in; do
+    # Extract the base filename without the extension
+    base=$(basename "$infile" .in)
+
+    # Define the path for the expected output file
+    expectedfile="$EXPECTED_DIR/$base.expected.out"
+
+    # Check if the expected output file exists
+    if [[ ! -f $expectedfile ]]; then
+        echo "Expected output file $expectedfile does not exist. Skipping $infile."
+        continue
+    fi
+
+    # Run the command and store its output in a temporary file
+    tmpfile=$(mktemp)
+    build/bin/repl < "$infile" > "$tmpfile"
+
+    # Compare the output with the expected output
+    if diff "$tmpfile" "$expectedfile"; then
+        echo "$base: PASSED"
+    else
+        echo "$base: FAILED"
+    fi
+
+    # Remove the temporary file
+    rm "$tmpfile"
+done

test/def_eval.expected.out

@@ -5,4 +5,4 @@
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 6},
    "data": "rfl : f = f"}],
- "env": 1}
+ "env": 1}

test/enableInitializersExecution.expected.out

@@ -1 +1 @@
-{"sorries": [], "messages": [], "env": 0}
+{"sorries": [], "messages": [], "env": 0}