diff --git a/tests/.gitignore b/tests/.gitignore index 1f28d50dc9..6fc1e663e2 100644 --- a/tests/.gitignore +++ b/tests/.gitignore @@ -2,8 +2,7 @@ /with_*_env.sh # Created by test suite -*.out.produced -*.exit.produced +*.produced # Created by bench suite *.measurements.jsonl diff --git a/tests/README.md b/tests/README.md index 13db992206..f09fc0a747 100644 --- a/tests/README.md +++ b/tests/README.md @@ -209,13 +209,14 @@ These files are available to configure a test: - `.before.sh`: This file is executed before the test/benchmark. - Create or set up temporary resources used by the test here. - Usually, it is better to create temporary files or directories inside the test itself, - so they're also available when opening the file in your editor. + Delete temporary resources created by previous test runs here if necessary. + Don't create temporary resources here, the test file should do so itself if possible. + That way, they're also available when opening the file in your editor. - `.after.sh`: This file is executed after the test/benchmark. - Delete temporary resources used by the test here. + Don't delete temporary resources here; do so in `.before.sh` if necessary. + Instead, add any temporary resources to the directory's `.gitignore` file. - `.out.expected`: The test fails if its stdout and stderr doesn't match this file's contents. @@ -250,13 +251,14 @@ These files are available to configure a test: - `.before.sh`: This file is executed before the test/benchmark. - Create or set up temporary resources used by the test here. - Usually, it is better to create temporary files or directories inside the test itself, - so they're also available when opening the file in your editor. + Delete temporary resources created by previous test runs here if necessary. + Don't create temporary resources here, the test file should do so itself if possible. + That way, they're also available when opening the file in your editor. - `.after.sh`: This file is executed after the test/benchmark. - Delete temporary resources used by the test here. + Don't delete temporary resources here; do so in `.before.sh` if necessary. + Instead, add any temporary resources to the directory's `.gitignore` file. - `.out.expected`: The test fails if its stdout and stderr doesn't match this file's contents. diff --git a/tests/elab/.gitignore b/tests/elab/.gitignore new file mode 100644 index 0000000000..d90bb5c6ab --- /dev/null +++ b/tests/elab/.gitignore @@ -0,0 +1,4 @@ +/IO_test.lean.dir/ +/getline_crash.lean.tmp +/handleLocking.lean.lock +/stdio.lean.stdout*.txt diff --git a/tests/elab/IO_test.lean.after.sh b/tests/elab/IO_test.lean.before.sh similarity index 100% rename from tests/elab/IO_test.lean.after.sh rename to tests/elab/IO_test.lean.before.sh diff --git a/tests/elab/getline_crash.lean.after.sh b/tests/elab/getline_crash.lean.before.sh similarity index 100% rename from tests/elab/getline_crash.lean.after.sh rename to tests/elab/getline_crash.lean.before.sh diff --git a/tests/elab/handleLocking.lean.after.sh b/tests/elab/handleLocking.lean.before.sh similarity index 100% rename from tests/elab/handleLocking.lean.after.sh rename to tests/elab/handleLocking.lean.before.sh diff --git a/tests/elab/stdio.lean.after.sh b/tests/elab/stdio.lean.before.sh similarity index 100% rename from tests/elab/stdio.lean.after.sh rename to tests/elab/stdio.lean.before.sh diff --git a/tests/elab_fail/.gitignore b/tests/elab_fail/.gitignore new file mode 100644 index 0000000000..cc725234d4 --- /dev/null +++ b/tests/elab_fail/.gitignore @@ -0,0 +1 @@ +/file_not_found.lean.readonly.txt diff --git a/tests/elab_fail/file_not_found.lean.after.sh b/tests/elab_fail/file_not_found.lean.before.sh similarity index 100% rename from tests/elab_fail/file_not_found.lean.after.sh rename to tests/elab_fail/file_not_found.lean.before.sh diff --git a/tests/server/diags.lean.after.sh b/tests/server/diags.lean.before.sh similarity index 100% rename from tests/server/diags.lean.after.sh rename to tests/server/diags.lean.before.sh