Skip to content

Proposal: re-organization into separate modules

Viktor Kuncak requested to merge github/fork/FlorianCassayre/modularization into main

Created by: FlorianCassayre

This pull request is a proposal to re-organize the codebase into sub-modules. It also fixes the layout of some packages, everything is now under lisa.

The modules are the following:

  • lisa-kernel, the kernel (the only one to compile in Scala 2)
  • lisa-utils, utilities that are almost necessary for a bare usage of LISA
  • lisa-theories, the available theories (no proofs, just definitions)
  • lisa-tptp, the TPTP-to-LISA module
  • lisa, the module that we actually export; also contains tactics and proofs
  • lisa-examples, a package to store examples, demos and exercises

And in the future we would have the following new modules:

  • lisa-isabelle, a port of lisabelle (find it in the VCS)
  • lisa-ace, the ACE/attempto module
  • lisa-front, an adaptation of FlorianCassayre/master-project

There probably won't be many more modules than these.

flowchart BT

classDef thick stroke-width: 3;
classDef dashed stroke-dasharray: 3 3;

lisa:::thick

lisa-isabelle:::dashed
lisa-ace:::dashed
lisa-front:::dashed

lisa-utils --> lisa-kernel
lisa-theories --> lisa-utils
lisa-tptp --> lisa-utils
lisa --> lisa-theories
lisa -.-> lisa-front
lisa-examples --> lisa
lisa-isabelle -.-> lisa-theories
lisa-front -.-> lisa-theories
lisa-ace -.-> lisa-theories & lisa-tptp
lisa --> lisa-tptp

In my opinion and to the best of my knowledge it makes a lot of sense to organize it that way:

  • The kernel is isolated from the rest, and the source is written in Scala 2
  • The third party components such as TPTP, the former lisabelle and the future ACE are independent and could ideally be bundled separately depending on the need
  • Compilation is faster, and refactoring can be done in intermediary steps
  • Usability (for developers) is unaffected
  • Argument of authority: larger organizations use a similar design pattern (e.g. akka, Play!)

One remark: it might make more sense to move src/ to lisa-core/, since it is named that way after all. src/ was moved to lisa/src/

The Scalafix/fmt tools don't work anymore: to avoid losing time I will fix them only if the proposal is accepted. they were re-enabled

Feedback is of course very welcome.

Merge request reports