Create v0.0.1 (#4)

* Initial Commit

* clean up readme

* Add Description for README.md

* Run Kani with command palette on a single file

* Basic Flow for running Kani commands on rust source file

* Refactor main flow outside the activation function (#1)

* Clean up default comments

* Refactor functionality outside the activate function

* Add temp and out files to gitignore

* Create v0.0.1

.eslintrc.js

@@ -9,75 +9,93 @@ module.exports = {
         node: true,
         mocha: true,
     },
-    plugins: ['@typescript-eslint', 'header', 'no-null'],
+    plugins: ['@typescript-eslint', 'header', 'no-null', 'eslint-plugin-tsdoc'],
     extends: [
         'eslint:recommended',
         'plugin:@typescript-eslint/eslint-recommended',
         'plugin:@typescript-eslint/recommended-requiring-type-checking',
         'plugin:@typescript-eslint/recommended',
         'prettier',
+        'plugin:import/recommended',
+        'plugin:import/typescript',
     ],
     rules: {
-        curly: 2, // Enforce braces on "if"/"for"/etc.
-        // TODO reenable this rule (by removing this off)
+        curly: 2,
+        "tsdoc/syntax": "warn",
         'no-async-promise-executor': 'off',
-        // TODO reenable this rule (by removing this off)
         '@typescript-eslint/no-misused-promises': 'off',
-        // TODO reenable this rule (by removing this off)
         '@typescript-eslint/prefer-regexp-exec': 'off',
-        // TODO reenable this rule (by removing this off)
         'no-async-promise-executors': 'off',
-        // TODO reenable this rule (by removing this off)
         '@typescript-eslint/consistent-type-assertions': 'off',
-        // TODO reenable this rule (by removing this off)
         '@typescript-eslint/ban-ts-ignore': 'off',
-        // TODO rennable this rule (by removing this off)
         '@typescript-eslint/class-name-casing': 'off',
-        // TODO rennable this rule (by removing this off)
         '@typescript-eslint/no-inferrable-types': 'off',
-        // TODO rennable this rule (by removing this off)
         '@typescript-eslint/no-unnecessary-type-assertion': 'off',
-        // TODO rennable this rule (by removing this off)
-        // this is another troublesome one, producing ~600 issues
         '@typescript-eslint/no-use-before-define': 'off',
-        // TODO rennable this rule (by removing this off)
         '@typescript-eslint/camelcase': 'off',
-        // TODO rennable this rule (by removing this off)
         'no-useless-escape': 'off',
-        // TODO rennable this rule (by removing this off)
         '@typescript-eslint/require-await': 'off',
-        // TODO rennable this rule (by removing this off)
         '@typescript-eslint/no-non-null-assertion': 'off',
-        // TODO rennable this rule (by removing this off)
         '@typescript-eslint/no-explicit-any': 'off',
         '@typescript-eslint/no-unsafe-argument': 'off',
-        // TODO rennable this rule (by removing this off)
-        '@typescript-eslint/explicit-function-return-type': 'off',
-        // TODO reenable this rule, tests mostly break this one (by changing off to error)
-        // This currently produces 700 non fixable by --fix errors
+        '@typescript-eslint/explicit-function-return-type': 'error',
         'sort-imports': 'off',
-        // TODO rennable this rule (by removing this off)
-        // namespaces are not great and we should stop using them
         '@typescript-eslint/no-namespace': 'off',
-        // Turn this on by removing off when we fix namespaces
         'no-inner-declarations': 'off',
-        // This is off because prettier takes care of it
         'no-extra-semi': 'off',
         'no-null/no-null': 'error',
         '@typescript-eslint/no-empty-function': 'off',
         '@typescript-eslint/no-unused-vars': 'off',
-        // New rules --> New TODOs
-        '@typescript-eslint/no-var-requires': 'off', // Should be able to remove with the full migration of SDK v3
-        '@typescript-eslint/no-unsafe-member-access': 'off', // use typeguard before accessing a member
-        '@typescript-eslint/no-unsafe-assignment': 'off', // 112 errors, similar to above
-        '@typescript-eslint/no-unsafe-return': 'off', // 26 errors, similar to above
-        '@typescript-eslint/no-unsafe-call': 'off', // 24 errors, need types for imported constructors
-        '@typescript-eslint/restrict-template-expressions': 'off', // 294 errors, forces template literals to be a certain type
-        '@typescript-eslint/no-floating-promises': 'off', // 274 errors, promises should catch errors or be awaited
-        '@typescript-eslint/ban-ts-comment': 'off', // 27 errors, bans compiler error exceptions
-        '@typescript-eslint/explicit-module-boundary-types': 'off', // Remove this once 'explicit-function-return-type' is on
-        // Do not check loops so while(true) works. Potentially reevalute this.
+        '@typescript-eslint/no-var-requires': 'off',
+        '@typescript-eslint/no-unsafe-member-access': 'off',
+        '@typescript-eslint/no-unsafe-assignment': 'off',
+        '@typescript-eslint/no-unsafe-return': 'off',
+        '@typescript-eslint/no-unsafe-call': 'off',
+        '@typescript-eslint/restrict-template-expressions': 'off',
+        '@typescript-eslint/no-floating-promises': 'off',
+        '@typescript-eslint/ban-ts-comment': 'off',
+        '@typescript-eslint/explicit-module-boundary-types': 'off',
         'no-constant-condition': ['error', { checkLoops: false }],
-        'no-empty': 'off'
+        'no-empty': 'off',
+        'sort-imports': [
+            'error',
+            {
+                ignoreCase: false,
+                ignoreDeclarationSort: true, // don"t want to sort import lines, use eslint-plugin-import instead
+                ignoreMemberSort: false,
+                memberSyntaxSortOrder: ['none', 'all', 'multiple', 'single'],
+                allowSeparatedGroups: true,
+            },
+        ],
+        // turn on errors for missing imports
+       'import/no-unresolved': 'off',
+       // 'import/no-named-as-default-member': 'off',
+       'import/order': [
+         'error',
+         {
+           groups: [
+             'builtin', // Built-in imports (come from NodeJS native) go first
+             'external', // <- External imports
+             'internal', // <- Absolute imports
+             ['sibling', 'parent'], // <- Relative imports, the sibling and parent types they can be mingled together
+             'index', // <- index imports
+             'unknown', // <- unknown
+           ],
+           'newlines-between': 'always',
+           alphabetize: {
+             /* sort in ascending order. Options: ["ignore", "asc", "desc"] */
+             order: 'asc',
+             /* ignore case. Options: [true, false] */
+             caseInsensitive: true,
+           },
+         },
+       ],
     },
-}
+    settings: {
+      'import/resolver': {
+        typescript: {
+          project: './tsconfig.json',
+        },
+      },
+    },
+};

.gitignore

@@ -53,3 +53,8 @@ tsconfig.lsif.json
 *.lsif
 *.db
 .clang-format
+*.vsix
+.vscode-test/
+out/
+*.d.ts
+.clang-format

.prettierrc

@@ -0,0 +1 @@
+{ "printWidth": 100, "singleQuote": true, "trailingComma": "all", "semi": true, "useTabs": true, "bracketSpacing": true, "tabWidth": 2 }

.vscode/extensions.json

@@ -0,0 +1,7 @@
+{
+	// See http://go.microsoft.com/fwlink/?LinkId=827846
+	// for the documentation about the extensions.json format
+	"recommendations": [
+		"dbaeumer.vscode-eslint"
+	]
+}

.vscode/launch.json

@@ -0,0 +1,34 @@
+// A launch configuration that compiles the extension and then opens it inside a new window
+// Use IntelliSense to learn about possible attributes.
+// Hover to view descriptions of existing attributes.
+// For more information, visit: https://go.microsoft.com/fwlink/?linkid=830387
+{
+	"version": "0.2.0",
+	"configurations": [
+		{
+			"name": "Run Extension",
+			"type": "extensionHost",
+			"request": "launch",
+			"args": [
+				"--extensionDevelopmentPath=${workspaceFolder}"
+			],
+			"outFiles": [
+				"${workspaceFolder}/out/**/*.js"
+			],
+			"preLaunchTask": "${defaultBuildTask}"
+		},
+		{
+			"name": "Extension Tests",
+			"type": "extensionHost",
+			"request": "launch",
+			"args": [
+				"--extensionDevelopmentPath=${workspaceFolder}",
+				"--extensionTestsPath=${workspaceFolder}/out/test/suite/index"
+			],
+			"outFiles": [
+				"${workspaceFolder}/out/test/**/*.js"
+			],
+			"preLaunchTask": "${defaultBuildTask}"
+		}
+	]
+}

.vscode/settings.json

@@ -0,0 +1,18 @@
+// 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
+    },
+    "search.exclude": {
+        "out": true // set this to false to include "out" folder in search results
+    },
+    // Turn off tsc task auto detection since we have the necessary tasks as npm scripts
+    "typescript.tsc.autoDetect": "off",
+      "editor.formatOnSave": false,
+      "eslint.validate": [
+        "typescript"
+      ],
+      "editor.codeActionsOnSave": {
+        "source.fixAll": true
+    }
+}

.vscode/tasks.json

@@ -0,0 +1,20 @@
+// See https://go.microsoft.com/fwlink/?LinkId=733558
+// for the documentation about the tasks.json format
+{
+	"version": "2.0.0",
+	"tasks": [
+		{
+			"type": "npm",
+			"script": "watch",
+			"problemMatcher": "$tsc-watch",
+			"isBackground": true,
+			"presentation": {
+				"reveal": "never"
+			},
+			"group": {
+				"kind": "build",
+				"isDefault": true
+			}
+		}
+	]
+}

.vscodeignore

@@ -1,5 +1,7 @@
 .vscode/**
 .vscode-test/**
+node_modules/**
+out/test/
 src/**
 .gitignore
 .yarnrc

CHANGELOG.md

@@ -0,0 +1,7 @@
+# Change Log
+
+All notable changes to the "Kani" extension will be documented in this file.
+
+## [Unreleased]
+
+- Initial release

CONTRIBUTING.md

@@ -52,6 +52,50 @@ If you think you have discovered a security issue please write to us at kani-ver
 Sensitive information can be encrypted using our [PGP key](https://github.com/model-checking/kani/blob/main/kani-verifier-security.public.key).
 See our [security disclosure instructions](.github/SECURITY.md) for more details.
 
+# Contributing to the Extension
+
+## What's in the folder
+
+* This folder contains all of the files necessary for your extension.
+* `package.json` - this is the manifest file in which you declare your extension and command.
+  * The sample plugin registers a command and defines its title and command name. With this information VS Code can show the command in the command palette. It doesn’t yet need to load the plugin.
+* `src/extension.ts` - this is the main file where you will provide the implementation of your command.
+  * The file exports one function, `activate`, which is called the very first time your extension is activated (in this case by executing the command). Inside the `activate` function we call `registerCommand`.
+  * We pass the function containing the implementation of the command as the second parameter to `registerCommand`.
+
+## Get up and running straight away
+
+* Press `F5` to open a new window with your extension loaded.
+* Run your command from the command palette by pressing (`Ctrl+Shift+P` or `Cmd+Shift+P` on Mac) and typing `Hello World`.
+* Set breakpoints in your code inside `src/extension.ts` to debug your extension.
+* Find output from your extension in the debug console.
+
+## Make changes
+
+* You can relaunch the extension from the debug toolbar after changing code in `src/extension.ts`.
+* You can also reload (`Ctrl+R` or `Cmd+R` on Mac) the VS Code window with your extension to load your changes.
+
+## Explore the API
+
+* You can open the full set of our API when you open the file `node_modules/@types/vscode/index.d.ts`.
+
+## Run tests
+
+* Open the debug viewlet (`Ctrl+Shift+D` or `Cmd+Shift+D` on Mac) and from the launch configuration dropdown pick `Extension Tests`.
+* Press `F5` to run the tests in a new window with your extension loaded.
+* See the output of the test result in the debug console.
+* Make changes to `src/test/suite/extension.test.ts` or create new test files inside the `test/suite` folder.
+  * The provided test runner will only consider files matching the name pattern `**.test.ts`.
+  * You can create folders inside the `test` folder to structure your tests any way you want.
+
+## Go further
+
+* [Follow UX guidelines](https://code.visualstudio.com/api/ux-guidelines/overview) to create extensions that seamlessly integrate with VS Code's native interface and patterns.
+ * Reduce the extension size and improve the startup time by [bundling your extension](https://code.visualstudio.com/api/working-with-extensions/bundling-extension).
+ * [Publish your extension](https://code.visualstudio.com/api/working-with-extensions/publishing-extension) on the VS Code extension marketplace.
+ * Automate builds by setting up [Continuous Integration](https://code.visualstudio.com/api/working-with-extensions/continuous-integration).
+
+
 ## Licensing
 
 This project is distributed under the terms of both the MIT license and the Apache License (Version 2.0).