🎉Initialize limboole extension

.github/workflows/ci.yml

@@ -0,0 +1,23 @@
+name: Publish Limboole VS Code Extension
+on:
+  push:
+    tags:
+      - "*"
+jobs:
+  deploy:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-node@v4
+        with:
+          node-version: 20
+      - run: npm ci
+      - name: Publish to Open VSX Registry
+        uses: HaaLeo/publish-vscode-extension@v1
+        with:
+          pat: ${{ secrets.OPEN_VSX_TOKEN }}
+      - name: Publish to Visual Studio Marketplace
+        uses: HaaLeo/publish-vscode-extension@v1
+        with:
+          pat: ${{ secrets.VS_MARKETPLACE_TOKEN }}
+          registryUrl: https://marketplace.visualstudio.com

.gitignore

@@ -0,0 +1,5 @@
+out
+dist
+node_modules
+.vscode-test/
+*.vsix

.vscode-test.mjs

@@ -0,0 +1,5 @@
+import { defineConfig } from '@vscode/test-cli';
+
+export default defineConfig({
+	files: 'out/test/**/*.test.js',
+});

.vscode/extensions.json

@@ -0,0 +1,5 @@
+{
+  // See http://go.microsoft.com/fwlink/?LinkId=827846
+  // for the documentation about the extensions.json format
+  "recommendations": ["dbaeumer.vscode-eslint", "connor4312.esbuild-problem-matchers", "ms-vscode.extension-test-runner"]
+}

.vscode/launch.json

@@ -0,0 +1,17 @@
+{
+	"version": "0.2.0",
+	"configurations": [
+		{
+			"name": "Run Extension",
+			"type": "extensionHost",
+			"request": "launch",
+			"args": [
+				"--extensionDevelopmentPath=${workspaceFolder}"
+			],
+			"outFiles": [
+				"${workspaceFolder}/dist/**/*.js"
+			],
+			"preLaunchTask": "${defaultBuildTask}"
+		}
+	]
+}

.vscode/settings.json

@@ -0,0 +1,13 @@
+// Place your settings in this file to overwrite default and user settings.
+{
+    "files.exclude": {
+        "out": false, // set this to true to hide the "out" folder with the compiled JS files
+        "dist": false // set this to true to hide the "dist" folder with the compiled JS files
+    },
+    "search.exclude": {
+        "out": true, // set this to false to include "out" folder in search results
+        "dist": true // set this to false to include "dist" folder in search results
+    },
+    // Turn off tsc task auto detection since we have the necessary tasks as npm scripts
+    "typescript.tsc.autoDetect": "off"
+}

.vscode/tasks.json

@@ -0,0 +1,18 @@
+{
+	"version": "2.0.0",
+	"tasks": [
+		{
+			"type": "npm",
+			"script": "watch",
+			"problemMatcher": "$tsc-watch",
+			"isBackground": true,
+			"presentation": {
+				"reveal": "never"
+			},
+			"group": {
+				"kind": "build",
+				"isDefault": true
+			}
+		}
+	]
+}

.vscodeignore

@@ -0,0 +1,14 @@
+.vscode/
+out/**
+node_modules/**
+src/**
+.gitignore
+.yarnrc
+esbuild.js
+vsc-extension-quickstart.md
+**/tsconfig.json
+**/eslint.config.mjs
+**/*.map
+**/*.ts
+**/.vscode-test.*
+resources/

CHANGELOG.md

@@ -0,0 +1,10 @@
+# Change Log
+
+
+## [0.1.0] - 2024-09-15
+
+- Initial release
+- Added support for checking satisfiability and validity of the formula
+- Added support for CNF translation
+- Added support for running Limboole from command palette
+- Added support for setting path to Limboole executable in settings

LICENSE

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2024 Soaibuzzaman
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

README.md

@@ -0,0 +1,40 @@
+# Limboole Extension for Visual Studio Code
+
+Limboole is a tool for checking satisfiability and tautology in arbitrary structural boolean formulas, and can also translate these problems into CNF. For more information, see the [Limboole website](https://fmv.jku.at/limboole/).
+
+If you prefer to use Limboole online, you can use the [FM Playground](https://play.formal-methods.net/). It offers a web interface for Limboole and other formal methods tools.
+
+
+## Features
+
+This extension allows you to run Limboole from within Visual Studio Code. 
+
+![](resources/demo.gif)
+
+## Usage
+
+For `.limboole` files, you can check satisfiability and validity of the formula by clicking on the `▶ Check SAT` and `▶ Check VAL` buttons in top left corner of the editor. The result will be displayed in the output window. For other file types e.g. .txt, you can run Limboole by opening the command palette (Ctrl+Shift+P) and typing `Limboole: ...`. You can check *satisfiability*, *validity*, and *CNF translation* of the formula.
+
+
+## Requirements
+
+This extension is packaged with Limboole executable for Windows, Linux, and macOS. If you have different operating system, you can download the latest version from the [Limboole website](https://fmv.jku.at/limboole/) and set the path to the executable in the settings.
+
+## Settings
+
+You can set the path to the Limboole executable in the settings. Open the settings by clicking on the gear icon in the bottom left corner of the window, then click on `Extensions` and `Limboole`. You can also open the settings by pressing `Ctrl+,` and typing `Limboole` in the search bar.
+
+## Known Issues
+
+The extension is tested on Windows and Linux. Unfortunately, I don't have access to macOS, so I can't test it there. If you encounter any issues, please report them on [GitHub](https://github.com/soaibsafi/limboole-vscode/issues) or open a PR.
+
+## License
+
+This extension is licensed under the MIT License. See [LICENSE](LICENSE) for more information.
+
+### Limboole License
+There is no specific license for the Limboole SAT solver front-end software. It is provided "as is" and can be used in any way without warranty of any kind.
+
+However, linking against Lingeling and PicoSAT will produce a binary, which falls under the license restrictions of those tools, which are more restricted.
+
+Refer to the [Limboole License](https://github.com/maximaximal/limboole/blob/master/LICENSE) for more information.

esbuild.js

@@ -0,0 +1,56 @@
+const esbuild = require("esbuild");
+
+const production = process.argv.includes('--production');
+const watch = process.argv.includes('--watch');
+
+/**
+ * @type {import('esbuild').Plugin}
+ */
+const esbuildProblemMatcherPlugin = {
+	name: 'esbuild-problem-matcher',
+
+	setup(build) {
+		build.onStart(() => {
+			console.log('[watch] build started');
+		});
+		build.onEnd((result) => {
+			result.errors.forEach(({ text, location }) => {
+				console.error(`✘ [ERROR] ${text}`);
+				console.error(`    ${location.file}:${location.line}:${location.column}:`);
+			});
+			console.log('[watch] build finished');
+		});
+	},
+};
+
+async function main() {
+	const ctx = await esbuild.context({
+		entryPoints: [
+			'src/extension.ts'
+		],
+		bundle: true,
+		format: 'cjs',
+		minify: production,
+		sourcemap: !production,
+		sourcesContent: false,
+		platform: 'node',
+		outfile: 'dist/extension.js',
+		external: ['vscode'],
+		logLevel: 'silent',
+		plugins: [
+			/* add to the end of plugins array */
+			esbuildProblemMatcherPlugin,
+		],
+	});
+	if (watch) {
+		await ctx.watch();
+	} else {
+		await ctx.rebuild();
+		await ctx.dispose();
+	}
+}
+
+main().catch(e => {
+	console.error(e);
+	process.exit(1);
+});

eslint.config.mjs

@@ -0,0 +1,28 @@
+import typescriptEslint from "@typescript-eslint/eslint-plugin";
+import tsParser from "@typescript-eslint/parser";
+
+export default [{
+    files: ["**/*.ts"],
+}, {
+    plugins: {
+        "@typescript-eslint": typescriptEslint,
+    },
+
+    languageOptions: {
+        parser: tsParser,
+        ecmaVersion: 2022,
+        sourceType: "module",
+    },
+
+    rules: {
+        "@typescript-eslint/naming-convention": ["warn", {
+            selector: "import",
+            format: ["camelCase", "PascalCase"],
+        }],
+
+        curly: "warn",
+        eqeqeq: "warn",
+        "no-throw-literal": "warn",
+        semi: "warn",
+    },
+}];

language-configuration.json

@@ -0,0 +1,23 @@
+{
+  "comments": {
+    "lineComment": "%"
+  },
+  "brackets": [
+    [
+      "(",
+      ")"
+    ],
+  ],
+  "autoClosingPairs": [
+    [
+      "(",
+      ")"
+    ]
+  ],
+  "surroundingPairs": [
+    [
+      "(",
+      ")"
+    ]
+  ]
+}

lib/LICENSE

@@ -0,0 +1,51 @@
+There is no specific license for the Limboole SAT solver front-end software. It is provided "as is" and can be used in any way without warranty of any kind.
+
+However, linking against Lingeling and PicoSAT will produce a binary, which falls under the license restrictions of those tools, which are more restricted.
+
+PicoSAT
+-------
+
+Copyright (c) 2006 - 2014, Armin Biere, Johannes Kepler University.
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to
+deal in the Software without restriction, including without limitation the
+rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
+sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
+IN THE SOFTWARE.
+
+Lingeling
+---------
+
+MIT License
+
+Copyright (c) 2010-2018 Armin Biere, Johannes Kepler University Linz, Austria
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.