Skip to content
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.

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

Modularize Arend #169

Closed
ice1000 opened this issue Mar 9, 2020 · 0 comments · Fixed by #177
Closed

Modularize Arend #169

ice1000 opened this issue Mar 9, 2020 · 0 comments · Fixed by #177
Assignees
Labels
Milestone

Comments

@ice1000
Copy link
Contributor

@ice1000 ice1000 commented Mar 9, 2020

We can modularize Arend into three projects right now:

  • The org.arend.ext package -- it should be self-contained, let's call it api
  • All the other code except the org.arend.frontend package -- it depends on api, let's call it main
  • The org.arend.frontend package -- it depends on main, let's call it cli
  • In the future, when we move the intellij plugin repo into this repo, we can make it another subproject as well, which depends on main (so no cli, and we don't even need to declare the exclusion).
    • This helps us get rid of the two-git-repo-in-the-same-dir hack too, so the setup of the intellij plugin will become a simple git clone and a ./gradlew build, easy peasy.
  • The tests will be moved into a separate module depending on cli because it uses the ANTLR parser
    • Maybe it makes sense to split cli into two, the real cli frontend and the ANTLR parser?
  • We may have a proto subproject, containing the generated protos

By doing this, all the include/exclude hacks like

include("org/arend/ext/**")
and
exclude("**/frontend/**")
and

Arend/build.gradle.kts

Lines 96 to 98 in b59d273

if (isTrue("AREND_EXCLUDE_CONSOLE")) {
exclude("**/frontend/**")
}
could disappear, because when we want the api module, we build it directly (via ./gradlew :api:assemble), when we want Arend without the cli frontend, we build it without it (via ./gradlew :main:assemble).

The sources task can be created easier because we can now use built-in tasks.

This also introduce extra flexibility in the future. Say, when we want a literate programming mode/documentation generator/linting tool for Arend, we can add 'em as another gradle subproject.

@ice1000 ice1000 added the build label Mar 9, 2020
@ice1000 ice1000 self-assigned this Mar 11, 2020
@ice1000 ice1000 added this to TODO in Project migration Mar 11, 2020
Project migration automation moved this from TODO to Done Mar 12, 2020
@ice1000 ice1000 added this to the 1.3 milestone Mar 12, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
No open projects
Development

Successfully merging a pull request may close this issue.

1 participant