Skip to content

add sdk and library support #238

add sdk and library support

add sdk and library support #238

Triggered via push November 16, 2024 13:34
Status Failure
Total duration 12m 9s
Artifacts 3

build.yml

on: push
Fit to window
Zoom out
Zoom in

Annotations

1 error, 167 warnings, and 95 notices
Test
Process completed with exit code 1.
Build
This job uses deprecated functionality from the 'gradle/actions/setup-gradle' action. Consult the Job Summary for more details.
Test
This job uses deprecated functionality from the 'gradle/actions/setup-gradle' action. Consult the Job Summary for more details.
Verify plugin
This job uses deprecated functionality from the 'gradle/actions/setup-gradle' action. Consult the Job Summary for more details.
Local 'var' is never modified and can be declared as 'val': src/main/kotlin/lean4ij/language/InlayHints.kt#L351
Variable is never modified, so it can be declared using 'val'
Unresolved reference in KDoc: src/main/kotlin/lean4ij/lsp/LeanLanguageServer.kt#L97
Cannot resolve symbol 'CodeWithInfos'
Usage of redundant or deprecated syntax or deprecated symbols: src/main/kotlin/lean4ij/infoview/external/Route.kt#L233
Unnecessary non-null assertion (!!) on a non-null receiver of type JsonElement
Obvious explicit type: src/main/kotlin/lean4ij/util/OsUtil.kt#L32
Explicitly given type is redundant here
Redundant nullable return type: src/main/kotlin/lean4ij/language/InlayHints.kt#L463
'getTextAttributes' always returns non-null type
Redundant nullable return type: src/main/kotlin/lean4ij/lsp/data/SubexprInfo.kt#L14
'contextInfo' always returns non-null type
Redundant semicolon: build.gradle.kts#L273
Redundant semicolon
Redundant semicolon: build.gradle.kts#L265
Redundant semicolon
Unstable API Usage: src/main/kotlin/lean4ij/lsp/LeanLanguageServerFactory.kt#L76
'getProject()' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.LSPClientFeatures' marked with @ApiStatus.Experimental
Unstable API Usage: src/main/kotlin/lean4ij/lsp/LeanLSPCompletionFeature.kt#L12
'LSPCompletionFeature()' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.LSPCompletionFeature' marked with @ApiStatus.Experimental
Unstable API Usage: src/main/kotlin/lean4ij/lsp/LeanLanguageServerFactory.kt#L75
Overridden method 'isEnabled(com.intellij.openapi.vfs.@org.jetbrains.annotations.NotNull VirtualFile)' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.LSPClientFeatures' marked with @ApiStatus.Experimental
Unstable API Usage: src/main/kotlin/lean4ij/infoview/InfoviewPopupDocumentation.kt#L72
'getPreferredContentWidth(int)' is declared in unstable class 'com.intellij.codeInsight.documentation.DocumentationEditorPane' marked with @ApiStatus.Internal
Unstable API Usage: src/main/kotlin/lean4ij/lsp/LeanLanguageServerFactory.kt#L67
'setCompletionFeature(com.redhat.devtools.lsp4ij.client.features.@org.jetbrains.annotations.NotNull LSPCompletionFeature)' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.LSPClientFeatures' marked with @ApiStatus.Experimental
Unstable API Usage: src/main/kotlin/lean4ij/infoview/InfoviewPopupDocumentation.kt#L96
'com.intellij.codeInsight.documentation.DocumentationEditorPane' is marked unstable with @ApiStatus.Internal
Unstable API Usage: src/main/kotlin/lean4ij/lsp/LeanLSPCompletionFeature.kt#L12
'com.redhat.devtools.lsp4ij.client.features.LSPCompletionFeature' is marked unstable with @ApiStatus.Experimental
Unstable API Usage: src/main/kotlin/lean4ij/lsp/LeanLanguageServerFactory.kt#L65
'LSPClientFeatures()' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.LSPClientFeatures' marked with @ApiStatus.Experimental
Unstable API Usage: src/main/kotlin/lean4ij/infoview/InfoviewPopupDocumentation.kt#L42
'com.intellij.codeInsight.documentation.DocumentationScrollPane' is marked unstable with @ApiStatus.Internal
Unstable API Usage: src/main/kotlin/lean4ij/project/leanFileProgressFinishedFillingLineMarkerRender.kt#L11
'com.intellij.openapi.editor.markup.FillingLineMarkerRenderer' is marked unstable with @ApiStatus.Experimental
Unstable API Usage: src/main/kotlin/lean4ij/infoview/InfoviewPopupDocumentation.kt#L42
'setViewportView(com.intellij.codeInsight.documentation.@org.jetbrains.annotations.NotNull DocumentationEditorPane, javax.swing.@org.jetbrains.annotations.NotNull JLabel)' is declared in unstable class 'com.intellij.codeInsight.documentation.DocumentationScrollPane' marked with @ApiStatus.Internal
Unstable API Usage: src/main/kotlin/lean4ij/project/leanFileProgressFillingLineMarkerRender.kt#L23
Overridden method 'getTextAttributesKey()' is declared in unstable 'com.intellij.openapi.editor.markup.FillingLineMarkerRenderer' marked with @ApiStatus.Experimental
Unstable API Usage: src/main/kotlin/lean4ij/lsp/LeanLanguageServerFactory.kt#L65
'com.redhat.devtools.lsp4ij.client.features.LSPClientFeatures' is marked unstable with @ApiStatus.Experimental
Unstable API Usage: src/main/kotlin/lean4ij/lsp/LeanLanguageServerFactory.kt#L68
'setDiagnosticFeature(com.redhat.devtools.lsp4ij.client.features.@org.jetbrains.annotations.NotNull LSPDiagnosticFeature)' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.LSPClientFeatures' marked with @ApiStatus.Experimental
Unstable API Usage: src/main/kotlin/lean4ij/infoview/InfoviewPopupDocumentation.kt#L72
'com.intellij.codeInsight.documentation.DocumentationEditorPane' is marked unstable with @ApiStatus.Internal
Unstable API Usage: src/main/kotlin/lean4ij/project/leanFileProgressFinishedFillingLineMarkerRender.kt#L23
Overridden method 'getTextAttributesKey()' is declared in unstable 'com.intellij.openapi.editor.markup.FillingLineMarkerRenderer' marked with @ApiStatus.Experimental
Unstable API Usage: src/main/kotlin/lean4ij/infoview/InfoviewPopupDocumentation.kt#L206
'com.intellij.codeInsight.documentation.DocumentationScrollPane' is marked unstable with @ApiStatus.Internal
Unstable API Usage: src/main/kotlin/lean4ij/lsp/LeanLanguageServerFactory.kt#L69
Overridden method 'isEnabled(com.intellij.psi.@org.jetbrains.annotations.NotNull PsiFile)' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.AbstractLSPDocumentFeature' marked with @ApiStatus.Experimental
Unstable API Usage: src/main/kotlin/lean4ij/infoview/InfoviewPopupDocumentation.kt#L206
'setViewportView(com.intellij.codeInsight.documentation.@org.jetbrains.annotations.NotNull DocumentationEditorPane, javax.swing.@org.jetbrains.annotations.NotNull JLabel)' is declared in unstable class 'com.intellij.codeInsight.documentation.DocumentationScrollPane' marked with @ApiStatus.Internal
Unstable API Usage: src/main/kotlin/lean4ij/project/leanFileProgressFillingLineMarkerRender.kt#L10
'com.intellij.openapi.editor.markup.FillingLineMarkerRenderer' is marked unstable with @ApiStatus.Experimental
Unstable API Usage: src/main/kotlin/lean4ij/lsp/LeanLanguageServerFactory.kt#L68
'com.redhat.devtools.lsp4ij.client.features.LSPDiagnosticFeature' is marked unstable with @ApiStatus.Experimental
Unstable API Usage: src/main/kotlin/lean4ij/lsp/LeanLanguageServerFactory.kt#L68
'LSPDiagnosticFeature()' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.LSPDiagnosticFeature' marked with @ApiStatus.Experimental
Unstable API Usage: src/main/kotlin/lean4ij/infoview/InfoviewPopupDocumentation.kt#L96
'getPreferredHeightByWidth(int)' is declared in unstable class 'com.intellij.codeInsight.documentation.DocumentationEditorPane' marked with @ApiStatus.Internal
Unstable API Usage: src/main/kotlin/lean4ij/lsp/LeanLSPCompletionFeature.kt#L15
Overridden method 'isEnabled(com.intellij.psi.@org.jetbrains.annotations.NotNull PsiFile)' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.AbstractLSPDocumentFeature' marked with @ApiStatus.Experimental
Unstable API Usage: src/main/kotlin/lean4ij/lsp/LeanLanguageServerFactory.kt#L64
'com.redhat.devtools.lsp4ij.client.features.LSPClientFeatures' is marked unstable with @ApiStatus.Experimental
Unused receiver parameter: src/main/kotlin/lean4ij/util/ProjectUtil.kt#L37
Receiver parameter is never used
Unused symbol: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L158
Function "nextSiblingIsAssign" is never used
Unused symbol: src/main/kotlin/lean4ij/lsp/data/InteractiveGoal.kt#L13
Property "isRemoved" is never used
Unused symbol: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L39
Property "BAD_CHAR_KEYS" is never used
Unused symbol: src/main/kotlin/lean4ij/project/LeanProjectService.kt#L130
Function "updateInfoviewFor" is never used
Unused symbol: src/main/kotlin/lean4ij/project/LeanFile.kt#L71
Property "progressingLineMarker" is never used
Unused symbol: src/main/kotlin/lean4ij/lsp/data/CodeWithInfos.kt#L140
Property "indent" is never used
Unused symbol: src/main/kotlin/lean4ij/infoview/external/KtorSseUtil.kt#L19
Function "respondSse" is never used
Unused symbol: src/main/kotlin/lean4ij/lsp/data/CodeWithInfos.kt#L140
Class "MsgEmbedTrace" is never used
Unused symbol: src/main/kotlin/lean4ij/lsp/data/InteractiveGoals.kt#L99
Function "highlight" is never used
Unused symbol: src/main/kotlin/lean4ij/language/InlayHints.kt#L575
Class "DiagInlayHintsCollector" is never used
Unused symbol: src/main/kotlin/lean4ij/lsp/LeanLanguageServer.kt#L34
Function "plainTermGoal" is never used
Unused symbol: src/main/kotlin/lean4ij/lsp/LeanLanguageServer.kt#L16
Function "fromJson" is never used
Unused symbol: src/main/kotlin/lean4ij/lsp/data/InteractiveGoal.kt#L12
Property "goalPrefix" is never used
Unused symbol: src/main/kotlin/lean4ij/infoview/LeanInfoViewWindow.kt#L63
Property "BORDER" is never used
Unused symbol: src/main/kotlin/lean4ij/infoview/LeanInfoviewColorSettingPage.kt#L23
Function "createTextAttributesKey" is never used
Unused symbol: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L40
Property "SEPARATOR_KEYS" is never used
Unused symbol: src/main/kotlin/lean4ij/lsp/LeanLanguageServer.kt#L30
Function "plainGoal" is never used
Unused symbol: src/main/kotlin/lean4ij/language/Lean4ParserDefinition.kt#L30
Class "Lean4ElementImpl" is never used
Unused symbol: src/main/kotlin/lean4ij/lsp/LeanLsp4jClient.kt#L24
Function "leanFileProgress" is never used
Unused symbol: src/main/kotlin/lean4ij/util/ProjectUtil.kt#L29
Function "notify" is never used
Unused symbol: src/main/kotlin/lean4ij/util/Constants.kt#L24
Property "EXTERNAL_INFOVIEW_SERVER_INITIALIZED" is never used
Unused symbol: src/main/kotlin/lean4ij/infoview/external/Route.kt#L319
Function "toJsonElement" is never used
Unused symbol: src/main/kotlin/lean4ij/infoview/LeanInfoViewWindow.kt#L79
Function "updateGoal" is never used
Unused symbol: src/main/kotlin/lean4ij/util/LeanUtil.kt#L10
Function "runCommand" is never used
Unused symbol: src/main/kotlin/lean4ij/infoview/LeanInfoviewService.kt#L11
Property "project" is never used
Unused symbol: src/main/kotlin/lean4ij/lsp/data/InteractiveGoal.kt#L11
Property "ctx" is never used
Unused symbol: src/main/kotlin/lean4ij/infoview/LeanInfoViewWindow.kt#L66
Function "render" is never used
Unused symbol: src/main/kotlin/lean4ij/project/FileProgressGutterIconRender.kt#L7
Class "FileProgressGutterIconRender" is never used
Unused symbol: src/main/kotlin/lean4ij/lsp/data/InteractiveGoal.kt#L9
Property "isInserted" is never used
Unused symbol: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L42
Property "VALUE_KEYS" is never used
Unused symbol: src/main/kotlin/lean4ij/infoview/InfoviewPopupDocumentation.kt#L197
Function "createExprPanel" is never used
Unused symbol: src/main/kotlin/lean4ij/lsp/data/CodeWithInfos.kt#L140
Property "cls" is never used
Unused symbol: src/main/kotlin/lean4ij/lsp/data/InteractiveGoal.kt#L8
Property "mvarId" is never used
Inspect code
You are running a Qodana linter without an exact version tag: jetbrains/qodana-jvm-community:latest
Inspect code
You are running a Qodana linter without an exact version tag: jetbrains/qodana-jvm-community:latest
Inspect code
You are running a Qodana linter without an exact version tag: jetbrains/qodana-jvm-community:latest
Class naming convention: src/main/kotlin/lean4ij/project/leanFileProgressFinishedFillingLineMarkerRender.kt#L11
Class name `leanFileProgressFinishedFillingLineMarkerRender` should start with an uppercase letter
Class naming convention: src/main/kotlin/lean4ij/project/leanFileProgressFillingLineMarkerRender.kt#L10
Class name `leanFileProgressFillingLineMarkerRender` should start with an uppercase letter
Local variable naming convention: src/main/kotlin/lean4ij/infoview/external/JcefInfoviewTooWindowFactory.kt#L94
Local variable name `user_gesture` should not contain underscores
Local variable naming convention: src/main/kotlin/lean4ij/infoview/external/JcefInfoviewTooWindowFactory.kt#L144
Local variable name `request_url` should not contain underscores
Local variable naming convention: src/main/kotlin/lean4ij/infoview/external/JcefInfoviewTooWindowFactory.kt#L130
Local variable name `origin_url` should not contain underscores
Local variable naming convention: src/main/kotlin/lean4ij/infoview/external/JcefInfoviewTooWindowFactory.kt#L111
Local variable name `user_gesture` should not contain underscores
Local variable naming convention: src/main/kotlin/lean4ij/infoview/external/JcefInfoviewTooWindowFactory.kt#L95
Local variable name `is_redirect` should not contain underscores
Local variable naming convention: src/main/kotlin/lean4ij/infoview/external/JcefInfoviewTooWindowFactory.kt#L143
Local variable name `cert_error` should not contain underscores
Local variable naming convention: src/main/kotlin/lean4ij/infoview/external/JcefInfoviewTooWindowFactory.kt#L110
Local variable name `target_url` should not contain underscores
Class member can have 'private' visibility: src/main/kotlin/lean4ij/lsp/LeanLanguageServer.kt#L90
Function 'getInteractiveDiagnosticsAsync' could be private
Class member can have 'private' visibility: src/main/kotlin/lean4ij/sdk/SdkService.kt#L31
Function 'getLeanVersion' could be private
Class member can have 'private' visibility: src/main/kotlin/lean4ij/lsp/LeanLanguageServer.kt#L84
Function 'getInteractiveTermGoalAsync' could be private
Class member can have 'private' visibility: src/main/kotlin/lean4ij/lsp/LeanLanguageServer.kt#L100
Function 'infoToInteractiveAsync' could be private
Class member can have 'private' visibility: src/main/kotlin/lean4ij/lsp/LeanLanguageServer.kt#L66
Function 'plainTermGoalAsync' could be private
Class member can have 'private' visibility: src/main/kotlin/lean4ij/lsp/LeanLanguageServer.kt#L78
Function 'getInteractiveGoalsAsync' could be private
Nested lambda has shadowed implicit parameter: src/main/kotlin/lean4ij/lsp/data/CodeWithInfos.kt#L61
Implicit parameter 'it' of enclosing lambda is shadowed
Nested lambda has shadowed implicit parameter: src/main/kotlin/lean4ij/lsp/data/CodeWithInfos.kt#L62
Implicit parameter 'it' of enclosing lambda is shadowed
Nested lambda has shadowed implicit parameter: src/main/kotlin/lean4ij/lsp/data/CodeWithInfos.kt#L62
Implicit parameter 'it' of enclosing lambda is shadowed
Nested lambda has shadowed implicit parameter: src/main/kotlin/lean4ij/lsp/data/CodeWithInfos.kt#L61
Implicit parameter 'it' of enclosing lambda is shadowed
Private property naming convention: src/main/kotlin/lean4ij/infoview/LeanInfoViewWindow.kt#L63
Private property name `BORDER` should not start with an uppercase letter
Property naming convention: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L42
Property name `VALUE_KEYS` should start with a lowercase letter
Property naming convention: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L41
Property name `KEY_KEYS` should start with a lowercase letter
Property naming convention: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L37
Property name `KEYWORD_IN_PROOF` should start with a lowercase letter
Property naming convention: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L46
Property name `SORRY_KEYS` should start with a lowercase letter
Property naming convention: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L32
Property name `KEY` should start with a lowercase letter
Property naming convention: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L47
Property name `KEYWORD_IN_PROOF_KEYS` should start with a lowercase letter
Property naming convention: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L44
Property name `NUMBER_KEYS` should start with a lowercase letter
Property naming convention: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L45
Property name `EMPTY_KEYS` should start with a lowercase letter
Property naming convention: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L33
Property name `VALUE` should start with a lowercase letter
Property naming convention: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L34
Property name `COMMENT` should start with a lowercase letter
Property naming convention: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L36
Property name `SORRY` should start with a lowercase letter
Property naming convention: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L31
Property name `SEPARATOR` should start with a lowercase letter
Property naming convention: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L40
Property name `SEPARATOR_KEYS` should start with a lowercase letter
Property naming convention: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L35
Property name `NUMBER` should start with a lowercase letter
Property naming convention: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L43
Property name `COMMENT_KEYS` should start with a lowercase letter
Property naming convention: src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt#L39
Property name `BAD_CHAR_KEYS` should start with a lowercase letter
Negated call can be simplified: src/main/kotlin/lean4ij/language/InlayHints.kt#L265
Replace negated 'isEmpty' with 'isNotEmpty'
Negated call can be simplified: src/main/kotlin/lean4ij/language/InlayHints.kt#L339
Replace negated 'isEmpty' with 'isNotEmpty'
Unnecessary '@OptIn' annotation: src/main/kotlin/lean4ij/infoview/external/Route.kt#L40
The opt-in annotation is redundant: no matching experimental API is used
Unnecessary '@OptIn' annotation: src/main/kotlin/lean4ij/infoview/LeanInfoviewColorSettingPage.kt#L56
The opt-in annotation is redundant: no matching experimental API is used
Unnecessary '@OptIn' annotation: src/main/kotlin/lean4ij/infoview/LeanInfoviewColorSettingPage.kt#L90
The opt-in annotation is redundant: no matching experimental API is used

Artifacts

Produced during runtime
Name Size
lean4ij-0.1.4
13 MB
pluginVerifier-result
15.1 KB
tests-result
12.3 KB