lean4-htt/lean.code-workspace
Eric Wieser 93a6279025
chore: add vscode cmake configuration (#3008)
This sets the build directory to `build/release` for the "CMake Tools
for Visual Studio Code" extension documented at
https://vector-of-bool.github.io/docs/vscode-cmake-tools/settings.html#cmake-builddirectory.

It also sets the generator to `make`, since otherwise it tries `Ninja`
which doesn't work.

Without these settings, the extension runs configure in a bad place at
startup.

This does *not* add the cmake tools extension to the default workspace
configuration; the goal is simply to prevent bad behavior for users who
already have the extension enabled.

# Summary

Screenshot of this in action:


![image](https://github.com/leanprover/lean4/assets/425260/6a08e5e5-77af-4ac5-85ed-a149a128e2ca)


Link to `RFC` or `bug` issue: N/A, this is not a bug nor a user-visible
feature.
2023-12-04 16:35:03 +00:00

52 lines
1 KiB
Text

{
"folders": [
{
"path": "."
},
{
"path": "src"
},
{
"path": "tests"
}
],
"settings": {
"files.insertFinalNewline": true,
"files.trimTrailingWhitespace": true,
"cmake.buildDirectory": "${workspaceFolder}/build/release",
"cmake.generator": "Unix Makefiles",
"[markdown]": {
"rewrap.wrappingColumn": 70
},
"[lean4]": {
"editor.rulers": [
100
]
}
},
"tasks": {
"version": "2.0.0",
"tasks": [
{
"label": "build",
"type": "shell",
"command": "make -C build/release -j$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)",
"problemMatcher": [],
"group": {
"kind": "build",
"isDefault": true
}
},
{
"label": "test",
"type": "shell",
"command": "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4); CTEST_OUTPUT_ON_FAILURE=1 make -C build/release test -j$NPROC ARGS=\"-j$NPROC\"",
"problemMatcher": [],
"group": {
"kind": "test",
"isDefault": true
}
}
]
}
}