Skip to content

Fix plugin ID mismatch between Gradle plugin and compiler plugin #55

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
pawinkler wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Fix plugin ID mismatch between Gradle plugin and compiler plugin #55

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions formver.common/src/org/jetbrains/kotlin/formver/common/PluginConfiguration.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,4 +18,9 @@ class PluginConfiguration(
"Conversion options may not be stricter than verification options; converting $conversionSelection but verifying $verificationSelection."
}
}

override fun toString(): String =
Copy link
Collaborator

@jesyspa jesyspa Mar 4, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not just make this a data class?

Copy link
Collaborator Author

@pawinkler pawinkler Mar 5, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seemed like the safer option for permanent modification, but after a bit of research, this is unsupported. Should I change it?

Copy link
Collaborator

@jesyspa jesyspa Mar 5, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes please

"PluginConfiguration(logLevel=$logLevel, errorStyle=$errorStyle, behaviour=$behaviour, " +
"conversionSelection=$conversionSelection, verificationSelection=$verificationSelection, " +
"checkUniqueness=$checkUniqueness)"
}
3 changes: 3 additions & 0 deletions ...in/cli/src/org/jetbrains/kotlin/formver/cli/FormalVerificationPluginComponentRegistrar.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,10 @@ package org.jetbrains.kotlin.formver.cli
import org.jetbrains.kotlin.compiler.plugin.CompilerPluginRegistrar
import org.jetbrains.kotlin.compiler.plugin.ExperimentalCompilerApi
import org.jetbrains.kotlin.config.CompilerConfiguration
import org.jetbrains.kotlin.config.messageCollector
import org.jetbrains.kotlin.fir.extensions.FirExtensionRegistrarAdapter
import org.jetbrains.kotlin.formver.common.*
import org.jetbrains.kotlin.cli.common.messages.CompilerMessageSeverity
import org.jetbrains.kotlin.formver.plugin.compiler.FormalVerificationPluginExtensionRegistrar

@OptIn(ExperimentalCompilerApi::class)
Expand Down Expand Up @@ -42,6 +44,7 @@ class FormalVerificationPluginComponentRegistrar : CompilerPluginRegistrar() {
logLevel, errorStyle, behaviour, conversionSelection, verificationSelection,
checkUniqueness
)
configuration.messageCollector.report(CompilerMessageSeverity.INFO, "Formal verification plugin: $config")
Copy link
Collaborator

@jesyspa jesyspa Mar 4, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@ligee Does this look reasonable? I am a bit concerned about adding a diagnostic to every build that uses our plugin.

FirExtensionRegistrarAdapter.registerExtension(FormalVerificationPluginExtensionRegistrar(config))
}
}
3 changes: 1 addition & 2 deletions formver.gradle-plugin/src/org/jetbrains/kotlin/formver/gradle/FormVerSubplugin.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,8 +60,7 @@ class FormVerGradleSubplugin
}
}

override fun getCompilerPluginId(): String =
"${BuildConfig.COMPILER_PLUGIN_GROUP}.${BuildConfig.COMPILER_PLUGIN_NAME}"
override fun getCompilerPluginId(): String = FormalVerificationPluginNames.PLUGIN_ID
Copy link
Collaborator

@jesyspa jesyspa Mar 4, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For my understanding: why is this the correct place to adjust? (If the problem is because of a mismatch between two places, why make the change at A instead of B?)

Copy link
Collaborator Author

@pawinkler pawinkler Mar 5, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The old code produced org.jetbrains.kotlin.formver.formver.compiler-plugin, which seemed deprecated to me, as it contains formver twice and only refers to the sub-project. Also, as far as I understand, changing the PLUGIN_ID would invalidate all existing Gradle configurations.

Copy link
Collaborator

@jesyspa jesyspa Mar 5, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, I think I see. Invalidating existing configurations isn't a big deal (we have zero users).

Is it okay that the PLUGIN_ID here ends up being shared by the gradle plugin and the compiler plugin? My understanding is that PLUGIN_ID was intended to refer to the gradle one.


override fun getPluginArtifact(): SubpluginArtifact =
SubpluginArtifact(
Expand Down
Loading