diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 0000000..babae05 --- /dev/null +++ b/.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 diff --git a/.vscode/copyright.code-snippets b/.vscode/copyright.code-snippets new file mode 100644 index 0000000..82c5f9d --- /dev/null +++ b/.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", + "-/" + ] + } +} diff --git a/.vscode/extensions.json b/.vscode/extensions.json new file mode 100644 index 0000000..f65ad9c --- /dev/null +++ b/.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" + ] +} diff --git a/.vscode/module-docstring.code-snippets b/.vscode/module-docstring.code-snippets new file mode 100644 index 0000000..1e45c0e --- /dev/null +++ b/.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", + "-/", + "", + ]}, +} diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 0000000..89f72cb --- /dev/null +++ b/.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, +} diff --git a/test.sh b/test.sh new file mode 100755 index 0000000..c7c3d6b --- /dev/null +++ b/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 diff --git a/test/def_eval.expected.out b/test/def_eval.expected.out index 051c701..83bef74 100644 --- a/test/def_eval.expected.out +++ b/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} \ No newline at end of file + "env": 1} diff --git a/test/enableInitializersExecution.expected.out b/test/enableInitializersExecution.expected.out index 5f47dbe..bee2c06 100644 --- a/test/enableInitializersExecution.expected.out +++ b/test/enableInitializersExecution.expected.out @@ -1 +1 @@ -{"sorries": [], "messages": [], "env": 0} \ No newline at end of file +{"sorries": [], "messages": [], "env": 0}