chore: allow module in tests (#8881)

This PR adjusts the test scripts and adds a simple test-only lakefile so
that `experimental.module` is set both when editing and running tests.

.gitignore

@@ -6,7 +6,6 @@
 lake-manifest.json
 /build
 /src/lakefile.toml
-/tests/lakefile.toml
 /lakefile.toml
 GPATH
 GRTAGS

tests/lakefile.toml

@@ -0,0 +1,5 @@
+name = "tests"
+
+# Allow `module` in tests when opened in the language server.
+# Enabled during actual test runs in the respective test_single.sh.
+moreGlobalServerArgs = ["-Dexperimental.module=true"]

tests/lean/run/1016.lean

@@ -1,3 +1,5 @@
+module
+
 inductive t | one | two
 
 example (h : False) : t.one = t.two := by

tests/lean/test_single.sh

@@ -2,5 +2,5 @@
 source ../common.sh
 
 # these tests don't have to succeed
-exec_capture lean -DprintMessageEndPos=true -Dlinter.all=false -DElab.async=true "$f" || true
+exec_capture lean -DprintMessageEndPos=true -Dlinter.all=false -Dexperimental.module=true "$f" || true
 diff_produced