lean.code-workspace

{
	"folders": [
		{
			"path": "."
		},
		{
			"path": "src"
		},
		{
			"path": "tests"
		},
		{
			"path": "script"
		}
	],
	"settings": {
		// Open terminal at root, not current workspace folder
		// (there is not way to directly refer to the root folder included as `.` above)
		"terminal.integrated.cwd": "${workspaceFolder:src}/..",
		"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": "build-old",
				"type": "shell",
				"command": "make -C build/release -j$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4) LAKE_EXTRA_ARGS=--old",
				"problemMatcher": [],
				"group": {
					"kind": "build"
				}
			},
			{
				"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
				}
			}
		]
	},
	"extensions": {
		"recommendations": [
			"leanprover.lean4"
		]
	}
}