Skip to content

Commit 1a987ee

Browse files
soaibsafisoaibsafi
committed
🎉Initialize limboole extension
0 parents  commit 1a987ee

26 files changed

+6106
-0
lines changed

‎.github/workflows/ci.yml

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
name: Publish Limboole VS Code Extension
2+
on:
3+
push:
4+
tags:
5+
- "*"
6+
jobs:
7+
deploy:
8+
runs-on: ubuntu-latest
9+
steps:
10+
- uses: actions/checkout@v4
11+
- uses: actions/setup-node@v4
12+
with:
13+
node-version: 20
14+
- run: npm ci
15+
- name: Publish to Open VSX Registry
16+
uses: HaaLeo/publish-vscode-extension@v1
17+
with:
18+
pat: ${{ secrets.OPEN_VSX_TOKEN }}
19+
- name: Publish to Visual Studio Marketplace
20+
uses: HaaLeo/publish-vscode-extension@v1
21+
with:
22+
pat: ${{ secrets.VS_MARKETPLACE_TOKEN }}
23+
registryUrl: https://marketplace.visualstudio.com

‎.gitignore

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
out
2+
dist
3+
node_modules
4+
.vscode-test/
5+
*.vsix

‎.vscode-test.mjs

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
import { defineConfig } from '@vscode/test-cli';
2+
3+
export default defineConfig({
4+
files: 'out/test/**/*.test.js',
5+
});

‎.vscode/extensions.json

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

‎.vscode/launch.json

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
{
2+
"version": "0.2.0",
3+
"configurations": [
4+
{
5+
"name": "Run Extension",
6+
"type": "extensionHost",
7+
"request": "launch",
8+
"args": [
9+
"--extensionDevelopmentPath=${workspaceFolder}"
10+
],
11+
"outFiles": [
12+
"${workspaceFolder}/dist/**/*.js"
13+
],
14+
"preLaunchTask": "${defaultBuildTask}"
15+
}
16+
]
17+
}

‎.vscode/settings.json

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
// Place your settings in this file to overwrite default and user settings.
2+
{
3+
"files.exclude": {
4+
"out": false, // set this to true to hide the "out" folder with the compiled JS files
5+
"dist": false // set this to true to hide the "dist" folder with the compiled JS files
6+
},
7+
"search.exclude": {
8+
"out": true, // set this to false to include "out" folder in search results
9+
"dist": true // set this to false to include "dist" folder in search results
10+
},
11+
// Turn off tsc task auto detection since we have the necessary tasks as npm scripts
12+
"typescript.tsc.autoDetect": "off"
13+
}

‎.vscode/tasks.json

+18
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
{
2+
"version": "2.0.0",
3+
"tasks": [
4+
{
5+
"type": "npm",
6+
"script": "watch",
7+
"problemMatcher": "$tsc-watch",
8+
"isBackground": true,
9+
"presentation": {
10+
"reveal": "never"
11+
},
12+
"group": {
13+
"kind": "build",
14+
"isDefault": true
15+
}
16+
}
17+
]
18+
}

‎.vscodeignore

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
.vscode/
2+
out/**
3+
node_modules/**
4+
src/**
5+
.gitignore
6+
.yarnrc
7+
esbuild.js
8+
vsc-extension-quickstart.md
9+
**/tsconfig.json
10+
**/eslint.config.mjs
11+
**/*.map
12+
**/*.ts
13+
**/.vscode-test.*
14+
resources/

‎CHANGELOG.md

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
# Change Log
2+
3+
4+
## [0.1.0] - 2024-09-15
5+
6+
- Initial release
7+
- Added support for checking satisfiability and validity of the formula
8+
- Added support for CNF translation
9+
- Added support for running Limboole from command palette
10+
- Added support for setting path to Limboole executable in settings

‎LICENSE

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

‎README.md

+40
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
# Limboole Extension for Visual Studio Code
2+
3+
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/).
4+
5+
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.
6+
7+
8+
## Features
9+
10+
This extension allows you to run Limboole from within Visual Studio Code.
11+
12+
![](resources/demo.gif)
13+
14+
## Usage
15+
16+
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.
17+
18+
19+
## Requirements
20+
21+
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.
22+
23+
## Settings
24+
25+
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.
26+
27+
## Known Issues
28+
29+
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.
30+
31+
## License
32+
33+
This extension is licensed under the MIT License. See [LICENSE](LICENSE) for more information.
34+
35+
### Limboole License
36+
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.
37+
38+
However, linking against Lingeling and PicoSAT will produce a binary, which falls under the license restrictions of those tools, which are more restricted.
39+
40+
Refer to the [Limboole License](https://github.com/maximaximal/limboole/blob/master/LICENSE) for more information.

‎esbuild.js

+56
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
const esbuild = require("esbuild");
2+
3+
const production = process.argv.includes('--production');
4+
const watch = process.argv.includes('--watch');
5+
6+
/**
7+
* @type {import('esbuild').Plugin}
8+
*/
9+
const esbuildProblemMatcherPlugin = {
10+
name: 'esbuild-problem-matcher',
11+
12+
setup(build) {
13+
build.onStart(() => {
14+
console.log('[watch] build started');
15+
});
16+
build.onEnd((result) => {
17+
result.errors.forEach(({ text, location }) => {
18+
console.error(`✘ [ERROR] ${text}`);
19+
console.error(` ${location.file}:${location.line}:${location.column}:`);
20+
});
21+
console.log('[watch] build finished');
22+
});
23+
},
24+
};
25+
26+
async function main() {
27+
const ctx = await esbuild.context({
28+
entryPoints: [
29+
'src/extension.ts'
30+
],
31+
bundle: true,
32+
format: 'cjs',
33+
minify: production,
34+
sourcemap: !production,
35+
sourcesContent: false,
36+
platform: 'node',
37+
outfile: 'dist/extension.js',
38+
external: ['vscode'],
39+
logLevel: 'silent',
40+
plugins: [
41+
/* add to the end of plugins array */
42+
esbuildProblemMatcherPlugin,
43+
],
44+
});
45+
if (watch) {
46+
await ctx.watch();
47+
} else {
48+
await ctx.rebuild();
49+
await ctx.dispose();
50+
}
51+
}
52+
53+
main().catch(e => {
54+
console.error(e);
55+
process.exit(1);
56+
});

‎eslint.config.mjs

+28
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
import typescriptEslint from "@typescript-eslint/eslint-plugin";
2+
import tsParser from "@typescript-eslint/parser";
3+
4+
export default [{
5+
files: ["**/*.ts"],
6+
}, {
7+
plugins: {
8+
"@typescript-eslint": typescriptEslint,
9+
},
10+
11+
languageOptions: {
12+
parser: tsParser,
13+
ecmaVersion: 2022,
14+
sourceType: "module",
15+
},
16+
17+
rules: {
18+
"@typescript-eslint/naming-convention": ["warn", {
19+
selector: "import",
20+
format: ["camelCase", "PascalCase"],
21+
}],
22+
23+
curly: "warn",
24+
eqeqeq: "warn",
25+
"no-throw-literal": "warn",
26+
semi: "warn",
27+
},
28+
}];

‎language-configuration.json

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
{
2+
"comments": {
3+
"lineComment": "%"
4+
},
5+
"brackets": [
6+
[
7+
"(",
8+
")"
9+
],
10+
],
11+
"autoClosingPairs": [
12+
[
13+
"(",
14+
")"
15+
]
16+
],
17+
"surroundingPairs": [
18+
[
19+
"(",
20+
")"
21+
]
22+
]
23+
}

‎lib/LICENSE

+51
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
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.
2+
3+
However, linking against Lingeling and PicoSAT will produce a binary, which falls under the license restrictions of those tools, which are more restricted.
4+
5+
PicoSAT
6+
-------
7+
8+
Copyright (c) 2006 - 2014, Armin Biere, Johannes Kepler University.
9+
10+
Permission is hereby granted, free of charge, to any person obtaining a copy
11+
of this software and associated documentation files (the "Software"), to
12+
deal in the Software without restriction, including without limitation the
13+
rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
14+
sell copies of the Software, and to permit persons to whom the Software is
15+
furnished to do so, subject to the following conditions:
16+
17+
The above copyright notice and this permission notice shall be included in
18+
all copies or substantial portions of the Software.
19+
20+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
21+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
22+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
23+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
24+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
25+
FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
26+
IN THE SOFTWARE.
27+
28+
Lingeling
29+
---------
30+
31+
MIT License
32+
33+
Copyright (c) 2010-2018 Armin Biere, Johannes Kepler University Linz, Austria
34+
35+
Permission is hereby granted, free of charge, to any person obtaining a copy
36+
of this software and associated documentation files (the "Software"), to deal
37+
in the Software without restriction, including without limitation the rights
38+
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
39+
copies of the Software, and to permit persons to whom the Software is
40+
furnished to do so, subject to the following conditions:
41+
42+
The above copyright notice and this permission notice shall be included in all
43+
copies or substantial portions of the Software.
44+
45+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
46+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
47+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
48+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
49+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
50+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
51+
SOFTWARE.

‎lib/limboole-linux-amd64.exe

93.8 KB
Binary file not shown.

‎lib/limboole-linux-x86.exe

89.7 KB
Binary file not shown.

‎lib/limboole.exe

48.5 KB
Binary file not shown.

‎lib/limbooleOSX

569 KB
Binary file not shown.

0 commit comments

Comments
 (0)