Skip to content

Commit 2eec391

Browse files
authored
Merge pull request #41 from dafny-lang/rework
Rework code base
2 parents 1aa8639 + 3a571b6 commit 2eec391

File tree

86 files changed

+2977
-2134
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

86 files changed

+2977
-2134
lines changed

.editorconfig

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
[*.ts]
2+
charset = utf-8
3+
end_of_line = lf
4+
indent_style = space
5+
indent_size = 2

.eslintrc.json

+125
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,125 @@
1+
{
2+
"env": {
3+
"browser": true,
4+
"es6": true
5+
},
6+
"extends": [
7+
"eslint:recommended",
8+
"plugin:@typescript-eslint/eslint-recommended"
9+
],
10+
"globals": {
11+
"Atomics": "readonly",
12+
"SharedArrayBuffer": "readonly"
13+
},
14+
"parser": "@typescript-eslint/parser",
15+
"parserOptions": {
16+
"ecmaVersion": 2018,
17+
"sourceType": "module",
18+
"project": "./tsconfig.json"
19+
},
20+
"plugins": [
21+
"@typescript-eslint"
22+
],
23+
"rules": {
24+
"indent": [ "warn", 2 ],
25+
"max-depth": [ "warn", 3 ],
26+
"linebreak-style": [ "warn", "unix" ],
27+
"max-params": [ "warn", 4 ],
28+
"no-trailing-spaces": "warn",
29+
"no-unreachable": "warn",
30+
"eqeqeq": [
31+
"warn",
32+
"always",
33+
{
34+
"null": "ignore"
35+
}
36+
],
37+
"no-multi-spaces": "warn",
38+
"space-before-blocks": [ "warn", "always" ],
39+
"space-in-parens": [ "warn", "never" ],
40+
"array-bracket-spacing": [ "warn", "always" ],
41+
"semi": "off",
42+
"@typescript-eslint/semi": [ "warn", "always" ],
43+
"no-unused-vars": "off",
44+
"@typescript-eslint/no-unused-vars": [
45+
"warn",
46+
{
47+
"varsIgnorePattern": "^_$"
48+
}
49+
],
50+
"object-curly-spacing": "off",
51+
"@typescript-eslint/object-curly-spacing": [ "warn", "always" ],
52+
"@typescript-eslint/type-annotation-spacing": [ "warn" ],
53+
"@typescript-eslint/prefer-optional-chain": "warn",
54+
"@typescript-eslint/no-implicit-any-catch": "warn",
55+
"@typescript-eslint/strict-boolean-expressions": "warn",
56+
"brace-style": "off",
57+
"@typescript-eslint/brace-style": "warn",
58+
"comma-dangle": "off",
59+
"@typescript-eslint/comma-dangle": "warn",
60+
"comma-spacing": "off",
61+
"@typescript-eslint/comma-spacing": "warn",
62+
"@typescript-eslint/consistent-type-definitions": [ "warn", "interface" ],
63+
"dot-notation": "off",
64+
"@typescript-eslint/dot-notation": "warn",
65+
"@typescript-eslint/explicit-member-accessibility": "warn",
66+
"@typescript-eslint/explicit-module-boundary-types": "warn",
67+
"func-call-spacing": "off",
68+
"@typescript-eslint/func-call-spacing": "warn",
69+
"keyword-spacing": "off",
70+
"@typescript-eslint/keyword-spacing": [
71+
"warn",
72+
{
73+
"overrides": {
74+
"if": { "after": false },
75+
"for": { "after": false },
76+
"while": { "after": false },
77+
"catch": { "after": false },
78+
"switch": { "after": false }
79+
}
80+
}
81+
],
82+
"@typescript-eslint/member-delimiter-style": [
83+
"warn",
84+
{
85+
"multiline": {
86+
"delimiter": "comma",
87+
"requireLast": false
88+
},
89+
"singleline": {
90+
"delimiter": "comma",
91+
"requireLast": false
92+
},
93+
"overrides": {
94+
"interface": {
95+
"multiline": {
96+
"delimiter": "semi",
97+
"requireLast": true
98+
}
99+
}
100+
}
101+
}
102+
],
103+
"@typescript-eslint/method-signature-style": [ "warn", "method" ],
104+
"require-await": "off",
105+
"@typescript-eslint/require-await": "warn",
106+
"@typescript-eslint/await-thenable": "warn",
107+
"quotes": "off",
108+
"@typescript-eslint/quotes": [ "warn", "single" ],
109+
"@typescript-eslint/prefer-readonly": "warn",
110+
"@typescript-eslint/prefer-includes": "warn",
111+
"@typescript-eslint/prefer-string-starts-ends-with": "warn",
112+
"@typescript-eslint/prefer-nullish-coalescing": "warn",
113+
"@typescript-eslint/unbound-method": "warn",
114+
"@typescript-eslint/unified-signatures": "warn",
115+
"@typescript-eslint/restrict-plus-operands": "warn",
116+
"@typescript-eslint/space-infix-ops": "warn",
117+
"@typescript-eslint/prefer-for-of": "warn",
118+
"@typescript-eslint/prefer-regexp-exec": "warn",
119+
"@typescript-eslint/prefer-reduce-type-parameter": "warn",
120+
"@typescript-eslint/padding-line-between-statements": "warn",
121+
"@typescript-eslint/require-array-sort-compare": "warn",
122+
"@typescript-eslint/ban-types": "warn",
123+
"@typescript-eslint/array-type": "warn"
124+
}
125+
}

.gitattributes

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
* text=auto eol=lf

.github/workflows/ci.yaml

+9-5
Original file line numberDiff line numberDiff line change
@@ -19,12 +19,16 @@ jobs:
1919
# uses: warchant/setup-sonar-scanner@v1
2020

2121
- run: npm install
22-
#- run: npm run prettier
23-
- run: npm run build
24-
- run: npm run package
22+
- run: npm run lint
23+
- run: npm run vscode:prepublish
2524
# - run: npm test
2625
# env:
2726
# CI: true
27+
- name: "Prepare: Package VSCode Extension"
28+
uses: actions/setup-node@v1
29+
- run: npm install -g [email protected]
30+
- run: vsce package --out dist/
31+
2832

2933
#- name: "Run sonar-scanner"
3034
# env:
@@ -119,8 +123,8 @@ jobs:
119123
id: get_version
120124
run: echo ::set-output name=VERSION::${GITHUB_REF/refs\/tags\/v/}
121125

122-
- run: npm install
123-
- run: npm run publish -- -p "${MARKETPLACE_TOKEN}" --packagePath dist/${PACKAGE_NAME}-${VERSION}.vsix
126+
- run: npm install -g [email protected]
127+
- run: vsce publish -p "${MARKETPLACE_TOKEN}" --packagePath dist/${PACKAGE_NAME}-${VERSION}.vsix
124128
env:
125129
# Note: Marketplace Token according to:
126130
# https://code.visualstudio.com/api/working-with-extensions/publishing-extension#get-a-personal-access-token

.gitignore

-1
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,6 @@
22
/dafny
33
.vscode-test
44
node_modules/
5-
package-lock.json
65
.DS_Store
76
/dist/*
87
!/dist/.gitkeep

.gitlab-ci.yml

-52
This file was deleted.

.prettierrc.js

-8
This file was deleted.

.vscode/extensions.json

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
{
2+
// See https://go.microsoft.com/fwlink/?LinkId=827846 to learn about workspace recommendations.
3+
// Extension identifier format: ${publisher}.${name}. Example: vscode.csharp
4+
5+
// List of extensions which should be recommended for users of this workspace.
6+
"recommendations": [
7+
"dbaeumer.vscode-eslint"
8+
]
9+
}

.vscode/launch.json

+5-5
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,17 @@
1-
// A launch configuration that compiles the extension and then opens it inside a new window
21
{
3-
"version": "0.1.0",
2+
"version": "0.2.0",
3+
// List of configurations. Add new configurations or edit existing ones.
44
"configurations": [
55
{
6-
"name": "Launch Extension",
76
"type": "extensionHost",
87
"request": "launch",
8+
"name": "Launch Client",
99
"runtimeExecutable": "${execPath}",
1010
"args": ["--extensionDevelopmentPath=${workspaceRoot}" ],
1111
"stopOnEntry": false,
1212
"sourceMaps": true,
13-
"outFiles": [ "${workspaceRoot}/out/src/**/*.js" ],
14-
"preLaunchTask": "npm"
13+
"outFiles": ["${workspaceRoot}/out/**/*.js"],
14+
"preLaunchTask": "npm: watch"
1515
}
1616
]
1717
}

.vscode/settings.json

+4-8
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,6 @@
1-
// Place your settings in this file to overwrite default and user settings.
21
{
3-
"files.exclude": {
4-
"out": false // set this to true to hide the "out" folder with the compiled JS files
5-
},
6-
"search.exclude": {
7-
"out": true // set this to false to include "out" folder in search results
8-
},
9-
"typescript.tsdk": "./node_modules/typescript/lib" // we want to use the TS server from our node_modules folder to control its version
2+
"editor.insertSpaces": false,
3+
"tslint.enable": true,
4+
"typescript.tsc.autoDetect": "off",
5+
"typescript.preferences.quoteStyle": "single"
106
}

.vscode/symbols.json

-1
This file was deleted.

.vscode/tasks.json

+25-32
Original file line numberDiff line numberDiff line change
@@ -1,40 +1,33 @@
1-
// Available variables which can be used inside of strings.
2-
// ${workspaceRoot}: the root folder of the team
3-
// ${file}: the current opened file
4-
// ${fileBasename}: the current opened file's basename
5-
// ${fileDirname}: the current opened file's dirname
6-
// ${fileExtname}: the current opened file's extension
7-
// ${cwd}: the current working directory of the spawned process
8-
9-
// A task runner that calls a custom npm script that compiles the extension.
101
{
112
"version": "2.0.0",
12-
13-
// we want to run npm
14-
"command": "npm",
15-
16-
// we run the custom script "compile" as defined in package.json
17-
"args": ["run", "compile", "--loglevel", "silent"],
18-
19-
// The tsc compiler is started in watching mode
20-
"isWatching": true,
21-
22-
// use the standard tsc in watch mode problem matcher to find compile problems in the output.
23-
"problemMatcher": "$tsc-watch",
243
"tasks": [
254
{
26-
"label": "npm",
27-
"type": "shell",
28-
"command": "npm",
29-
"args": [
30-
"run",
31-
"compile",
32-
"--loglevel",
33-
"silent"
34-
],
5+
"type": "npm",
6+
"script": "compile",
7+
"group": "build",
8+
"presentation": {
9+
"panel": "dedicated",
10+
"reveal": "never"
11+
},
12+
"problemMatcher": [
13+
"$tsc"
14+
]
15+
},
16+
{
17+
"type": "npm",
18+
"script": "watch",
3519
"isBackground": true,
36-
"problemMatcher": "$tsc-watch",
37-
"group": "build"
20+
"group": {
21+
"kind": "build",
22+
"isDefault": true
23+
},
24+
"presentation": {
25+
"panel": "dedicated",
26+
"reveal": "never"
27+
},
28+
"problemMatcher": [
29+
"$tsc-watch"
30+
]
3831
}
3932
]
4033
}

.vscodeignore

-14
This file was deleted.

CHANGELOG.md

+6
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,11 @@
11
# Release Notes
22

3+
## 2.0.0
4+
5+
- Revised the code base
6+
- Setting a custom Dafny installation now disables automatic updates
7+
- Now showing the Dafny installation progress in the terminal
8+
39
## 1.8.0
410

511
- Group verification errors and their related locations by using the "Related Information" UI for diagnostics.

0 commit comments

Comments
 (0)