aya-prover / aya-dev

A proof assistant and a dependently-typed language
https://www.aya-prover.org
MIT License
282 stars 18 forks source link

Getting rid of shitty upstream depedencies #35

Open ice1000 opened 3 years ago

ice1000 commented 3 years ago

We are currently suffering from the following projects:

Also, I propose removing the tgbot subproject since it's useless.

re-xyr commented 3 years ago

What is jpm?

ice1000 commented 3 years ago

What is jpm?

https://www.oracle.com/corporate/features/understanding-java-9-modules.html

re-xyr commented 3 years ago

Sounds like Java ecosystem is in a mess. Or probably this is true for every language...

ice1000 commented 3 years ago

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.

re-xyr commented 3 years ago

Seems to be a bad choice of Oracle for not officialize the community solution already.

ice1000 commented 3 years ago

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

ice1000 commented 3 years ago

Also maybe it's hard for the standard library to be modularized in a way the community do

ice1000 commented 3 years ago

Idk

ice1000 commented 3 years ago

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.

ice1000 commented 2 years ago
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
ice1000 commented 2 years ago

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
ice1000 commented 1 week ago

Latest

+--- project :ide
|    \--- project :cli-impl
|         +--- project :base
|         |    +--- project :syntax
|         |    |    +--- project :tools-kala
|         |    |    |    +--- org.glavo.kala:kala-common:0.74.0
|         |    |    |    |    +--- org.glavo.kala:kala-base:0.74.0
|         |    |    |    |    |    \--- org.jetbrains:annotations:24.1.0 -> 26.0.1
|         |    |    |    |    +--- org.glavo.kala:kala-collection:0.74.0
|         |    |    |    |    |    +--- org.glavo.kala:kala-base:0.74.0 (*)
|         |    |    |    |    |    \--- org.jetbrains:annotations:24.1.0 -> 26.0.1
|         |    |    |    |    +--- org.glavo.kala:kala-collection-primitive:0.74.0
|         |    |    |    |    |    +--- org.glavo.kala:kala-base:0.74.0 (*)
|         |    |    |    |    |    +--- org.glavo.kala:kala-collection:0.74.0 (*)
|         |    |    |    |    |    \--- org.jetbrains:annotations:24.1.0 -> 26.0.1
|         |    |    |    |    \--- org.jetbrains:annotations:24.1.0 -> 26.0.1
|         |    |    |    \--- project :tools
|         |    |    |         +--- org.jetbrains:annotations:26.0.1
|         |    |    |         +--- org.glavo.kala:kala-collection:0.74.0 (*)
|         |    |    |         +--- project :pretty
|         |    |    |         |    +--- org.jetbrains:annotations:26.0.1
|         |    |    |         |    \--- org.glavo.kala:kala-collection:0.74.0 (*)
|         |    |    |         \--- org.aya-prover.upstream:ij-util-text:0.0.28
|         |    |    |              +--- org.jetbrains:annotations:26.0.1
|         |    |    |              +--- org.glavo.kala:kala-collection:0.74.0 (*)
|         |    |    |              \--- org.jetbrains.kotlin:kotlin-stdlib:2.0.21
|         |    |    |                   \--- org.jetbrains:annotations:13.0 -> 26.0.1
|         |    |    +--- project :tools-md
|         |    |    |    +--- project :tools-kala (*)
|         |    |    |    +--- org.jetbrains:annotations:26.0.1
|         |    |    |    \--- org.commonmark:commonmark:0.24.0
|         |    |    +--- project :pretty (*)
|         |    |    \--- org.aya-prover.upstream:ij-parsing-core:0.0.28
|         |    |         +--- org.glavo.kala:kala-common:0.74.0 (*)
|         |    |         +--- org.aya-prover.upstream:ij-util-text:0.0.28 (*)
|         |    |         +--- org.aya-prover.upstream:lang-syntax:0.0.28
|         |    |         |    \--- org.jetbrains.kotlin:kotlin-stdlib:2.0.21 (*)
|         |    |         \--- org.jetbrains.kotlin:kotlin-stdlib:2.0.21 (*)
|         |    \--- project :tools-md (*)
|         +--- project :parser
|         |    +--- org.jetbrains:annotations:26.0.1
|         |    +--- org.aya-prover.upstream:ij-parsing-core:0.0.28 (*)
|         |    \--- org.aya-prover.upstream:ij-parsing-wrapper:0.0.28
|         |         \--- org.aya-prover.upstream:ij-parsing-core:0.0.28 (*)
|         +--- com.google.code.gson:gson:2.11.0
|         |    \--- com.google.errorprone:error_prone_annotations:2.27.0
|         +--- project :producer
|         |    +--- project :syntax (*)
|         |    \--- project :parser (*)
|         +--- project :jit-compiler
|         |    \--- project :base (*)
|         \--- org.commonmark:commonmark:0.24.0
+--- org.aya-prover.upstream:javacs-protocol:0.0.28
|    +--- org.jetbrains:annotations:26.0.1
|    +--- org.glavo.kala:kala-common:0.74.0 (*)
|    \--- com.google.code.gson:gson:2.11.0 (*)
+--- project :cli-console
|    +--- project :tools-repl
|    |    +--- project :tools (*)
|    |    +--- org.jline:jline-reader:3.27.1
|    |    |    \--- org.jline:jline-terminal:3.27.1
|    |    |         \--- org.jline:jline-native:3.27.1
|    |    \--- org.jline:jline-terminal:3.27.1 (*)
|    +--- project :cli-impl (*)
|    +--- project :producer (*)
|    +--- info.picocli:picocli:4.7.6
|    +--- org.jline:jline-terminal-jni:3.27.1
|    |    +--- org.jline:jline-native:3.27.1
|    |    \--- org.jline:jline-terminal:3.27.1 (*)
|    \--- org.jline:jline-builtins:3.27.1
|         +--- org.jline:jline-reader:3.27.1 (*)
|         \--- org.jline:jline-style:3.27.1
|              \--- org.jline:jline-terminal:3.27.1 (*)
\--- info.picocli:picocli:4.7.6
ice1000 commented 1 week ago

It may look like more dependencies, but most of them are actually very small libraries maintained by us. So it should be an improvement.