aya-dev
aya-dev copied to clipboard
aya-prover
Getting rid of shitty upstream depedencies
We are currently suffering from the following projects:
- (Superseded) Eclipse lsp4j, which is itself a shit mountain (doesn't work with jpms, caused a lot of installation/jlink problems, written in Java 8) and also has shit mountain dependencies (guava, xtext, xtend, etc.)
- I found an alternative, see https://github.com/georgewfraser/java-language-server/issues/197
- Published!
- The badass jlink plugin of Gradle -- it is not itself a shit mountain (it's a great project), but it's designed for shit mountains. It aims at repackaging your fatJar into a jpms module and let jlink process it. Aya is built entirely with jpms, so if we have all upstream deps jpms-ed, we can get rid of this plugin entirely.
- ~~The plugin does not work with Java 19.~~
- There are new maintainers now, works with latest Java
- ~~The plugin does not work with Java 19.~~
- Gradle -- it is fine at the moment because we still want it to offer us the ability to publish to maven central, but Gradle is also designed for maven style projects. Ughh.
- (Superseded) ANTLR4-runtime -- doesn't support jpms is the only problem (yet). Seems not very hard to repackage with jpms support.
- We've decided #466
- (Superseded) Commonmark -- ~~doesn't support jpms, written in Java 8 with a return-void visitor (https://github.com/commonmark/commonmark-java/issues/125). I think we can take some code from it, repackage, and add jpms support.~~
- ~~There is an outdated attempt to add jpms: https://github.com/xzel23/commonmark-java/tree/0.14.0-jigsaw~~
- ~~Already repackaged and redistrubuted, see https://github.com/aya-prover/commonmark-java~~ outdated
- The official distribution how supports jpms
- Now we're using repackaged JetBrains/markdown, which is even better for our own purposes
- (Acceptable) GSON -- it's a PROJECT FROM GOOGLE so it's gonna be a disaster to depend on it. However, it supports jpms, so I think it's fine to use it (well but people are complaining https://github.com/google/gson/issues/1315#issuecomment-733899200).
- (Removed) ~~JImGui -- it doesn't yet have jpms support, but I can add it in a minute since it's my project, so it's a small problem.~~
Also, I propose removing the tgbot subproject since it's useless.
What is jpm?
https://www.oracle.com/corporate/features/understanding-java-9-modules.html
Sounds like Java ecosystem is in a mess. Or probably this is true for every language...
Sounds like Java ecosystem is in a mess.
Yes, this is because Java didn't have a module system or package management system long time ago. The community designed a format called "POM" (probably by maven) and it became the de-facto standard, but starting from Java 9 there is a new, official one. Part of the community is not willing to change, but we're not one of 'em.
Seems to be a bad choice of Oracle for not officialize the community solution already.
Seems to be a bad choice of Oracle for not officialize the community solution already.
I don't know. There are pros and cons. The community solution relies on jars, while the official one is based on modules. By that, we can trim unused modules when packaging the application, giving rise to smaller releases. The jar-based solution often uses some hacks to remove unused classes
Also maybe it's hard for the standard library to be modularized in a way the community do
I decide to delay this until we reach some late-milestone, like 0.12 or 0.15, after some major language features are worked upon.
runtimeClasspath - Runtime classpath of source set 'main'.
+--- org.eclipse.lsp4j:org.eclipse.lsp4j:0.15.0
| +--- org.eclipse.lsp4j:org.eclipse.lsp4j.generator:0.15.0
| | +--- org.eclipse.lsp4j:org.eclipse.lsp4j.jsonrpc:0.15.0
| | | \--- com.google.code.gson:gson:[2.9.0,2.10) -> 2.9.1
| | \--- org.eclipse.xtend:org.eclipse.xtend.lib:2.24.0
| | +--- org.eclipse.xtext:org.eclipse.xtext.xbase.lib:2.24.0
| | | \--- com.google.guava:guava:27.1-jre
| | | +--- com.google.guava:failureaccess:1.0.1
| | | +--- com.google.guava:listenablefuture:9999.0-empty-to-avoid-conflict-with-guava
| | | +--- com.google.code.findbugs:jsr305:3.0.2
| | | +--- org.checkerframework:checker-qual:2.5.2
| | | +--- com.google.errorprone:error_prone_annotations:2.2.0
| | | +--- com.google.j2objc:j2objc-annotations:1.1
| | | \--- org.codehaus.mojo:animal-sniffer-annotations:1.17
| | \--- org.eclipse.xtend:org.eclipse.xtend.lib.macro:2.24.0
| | \--- org.eclipse.xtext:org.eclipse.xtext.xbase.lib:2.24.0 (*)
| \--- org.eclipse.lsp4j:org.eclipse.lsp4j.jsonrpc:0.15.0 (*)
+--- org.eclipse.lsp4j:org.eclipse.lsp4j.jsonrpc:0.15.0 (*)
\--- project :cli
+--- project :base
| +--- project :tools
| | +--- org.jetbrains:annotations:23.0.0
| | +--- org.glavo.kala:kala-common:0.50.0
| | | +--- org.glavo.kala:kala-base:0.50.0
| | | +--- org.glavo.kala:kala-collection:0.50.0
| | | | \--- org.glavo.kala:kala-base:0.50.0
| | | \--- org.glavo.kala:kala-collection-primitive:0.50.0
| | | +--- org.glavo.kala:kala-base:0.50.0
| | | \--- org.glavo.kala:kala-collection:0.50.0 (*)
| | \--- project :pretty
| | +--- org.jetbrains:annotations:23.0.0
| | \--- org.glavo.kala:kala-common:0.50.0 (*)
| +--- project :pretty (*)
| +--- org.aya-prover.guest0x0:cubical:0.17.1
| | \--- org.aya-prover:pretty:0.20 -> project :pretty (*)
| \--- org.aya-prover:commonmark:0.19.1
+--- project :parser
| \--- org.antlr:antlr4-runtime:4.10.1
+--- project :tools-repl
| +--- project :pretty (*)
| +--- project :tools (*)
| +--- org.jline:jline-reader:3.21.0
| | \--- org.jline:jline-terminal:3.21.0
| +--- org.jline:jline-terminal:3.21.0
| \--- org.antlr:antlr4-runtime:4.10.1
+--- com.google.code.gson:gson:2.9.1
+--- info.picocli:picocli:4.6.3
+--- org.jline:jline-terminal-jansi:3.21.0
| +--- org.fusesource.jansi:jansi:2.4.0
| \--- org.jline:jline-terminal:3.21.0
\--- org.jline:jline-builtins:3.21.0
+--- org.jline:jline-reader:3.21.0 (*)
\--- org.jline:jline-style:3.21.0
\--- org.jline:jline-terminal:3.21.0
Removing our own libraries:
runtimeClasspath - Runtime classpath of source set 'main'.
+--- org.eclipse.lsp4j:org.eclipse.lsp4j:0.15.0
| +--- org.eclipse.lsp4j:org.eclipse.lsp4j.generator:0.15.0
| | +--- org.eclipse.lsp4j:org.eclipse.lsp4j.jsonrpc:0.15.0
| | | \--- com.google.code.gson:gson:[2.9.0,2.10) -> 2.9.1
| | \--- org.eclipse.xtend:org.eclipse.xtend.lib:2.24.0
| | +--- org.eclipse.xtext:org.eclipse.xtext.xbase.lib:2.24.0
| | | \--- com.google.guava:guava:27.1-jre
| | | +--- com.google.guava:failureaccess:1.0.1
| | | +--- com.google.guava:listenablefuture:9999.0-empty-to-avoid-conflict-with-guava
| | | +--- com.google.code.findbugs:jsr305:3.0.2
| | | +--- org.checkerframework:checker-qual:2.5.2
| | | +--- com.google.errorprone:error_prone_annotations:2.2.0
| | | +--- com.google.j2objc:j2objc-annotations:1.1
| | | \--- org.codehaus.mojo:animal-sniffer-annotations:1.17
| | \--- org.eclipse.xtend:org.eclipse.xtend.lib.macro:2.24.0
| | \--- org.eclipse.xtext:org.eclipse.xtext.xbase.lib:2.24.0 (*)
| \--- org.eclipse.lsp4j:org.eclipse.lsp4j.jsonrpc:0.15.0 (*)
+--- org.eclipse.lsp4j:org.eclipse.lsp4j.jsonrpc:0.15.0 (*)
\--- project :cli
+--- project :base
| +--- project :tools
| | +--- org.jetbrains:annotations:23.0.0
| | \--- project :pretty
| | +--- org.jetbrains:annotations:23.0.0
+--- project :parser
| \--- org.antlr:antlr4-runtime:4.10.1
+--- project :tools-repl
| +--- org.jline:jline-reader:3.21.0
| | \--- org.jline:jline-terminal:3.21.0
| +--- org.jline:jline-terminal:3.21.0
| \--- org.antlr:antlr4-runtime:4.10.1
+--- com.google.code.gson:gson:2.9.1
+--- info.picocli:picocli:4.6.3
+--- org.jline:jline-terminal-jansi:3.21.0
| +--- org.fusesource.jansi:jansi:2.4.0
| \--- org.jline:jline-terminal:3.21.0
\--- org.jline:jline-builtins:3.21.0
+--- org.jline:jline-reader:3.21.0 (*)
\--- org.jline:jline-style:3.21.0
\--- org.jline:jline-terminal:3.21.0