search

prismmodelchecker / prism

The main development version of the PRISM model checker.
http://www.prismmodelchecker.org/
GNU General Public License v2.0
156 stars 72 forks source link

[Tracking] Build toolchain revamp #223

Open spacefrogg opened 1 year ago

spacefrogg commented 1 year ago

This task is tracking the build toolchain reconstruction efforts.

Things to establish:

  1. What are the current final make build targets (from all makefiles throughout the project, except those "internal" to shipped dependencies, i.e., which would be updated with updating the dependencies anyway)?
    • These are the targets that are meant to be called by the user (not those that are internally necessary).
  2. What are the build environments PRISM should build in (platform and runtime environment)?
  3. What are the external dependencies that are shipped with PRISM?
ifndefJOSH commented 1 year ago

Full disclosure: I am somewhat an outsider to this project, but I maintain a project called STAMINA which has a version depending directly on PRISM. Part of my opinion here is influenced by that need to use PRISM as a dependency. STAMINA's PRISM integration (currently) uses the same build system as PRISM (GNU Makefile) but if/when PRISM decides to switch build systems, STAMINA will likely follow suite, so I figured I'd put my two cents in here.

As I mentioned in #234, since PRISM used Java extensively, it may be easiest to use gradle or mvn, which are well-tuned to the Java language and necessary Java dependencies. There are two major locations for Java dependencies to be published: MavenCentral and Apache Ivy. gradle supports both and I think so does mvn, but the latter may only support MavenCentral. Here is some relevant Gradle documentation.

However, one limitation of both gradle and mvn is that it seems to be difficult to create package archives for different Linux distributions' package managers. But, since it is super easy to create a JAR file with these build systems, there seems to be, at least on most Linux distributions, a fairly straightforward way of creating a package archive containing your JAR file, small script to execute java -jar <your jar file> with desired environment, and dependency list.

That said, here are some potential dependency package lists for PRISM on various Linux distros and their install commands:

  1. RHEL & CentOS: sudo yum install java-11-openjdk-devel java-11-openjdk java-11-openjdk-headless libgit2-devel make
  2. Debian-based distros (including Ubuntu, Linux Mint, and Pop!_OS): sudo apt-get install openjdk-11-jdk openjdk-11-jre-headless libgit2-dev git-core build-essential
  3. Fedora 36 or later: sudo dnf install java-11-openjdk-devel java-11-openjdk-headless libgit2-devel make
  4. Arch Linux, Artix, etc: sudo pacman -S jdk openjdk-jre-headless git libgit2 libgit2-headers libgit2-python base-devel
  5. Manjaro: sudo pacman -S jdk openjdk-headless git make libgit2 libgit2-python base-devel
  6. OpenSUSE: sudo zypper in java-11-openjdk-headless libgit2-devel git make
  7. AlmaLinux: sudo yum install java-11-openjdk-headless libgit2-headers git make
  8. Solus: sudo eopkg it java-11-openjdk-headless libget2 libget2-devel git make
  9. MacOS using brew: brew install openjdk git make

These are necessary if the build tool also comes with a packager to create, e.g., deb packages. Obviously, git, make, etc. (development-specific packages) can be omitted when distributing a binary version, and make specifically can be omitted if it is no longer used as the build system.

Additionally, these do not include PRISM's internally shipped dependencies like the CUDD library.

As for the C portion of PRISM, I don't know if mvn supports building C files, but I know gradle does.

Finally, I would be happy to assist in developing a basic build.gradle or build.gradle.kts (or the Maven equivalent) for PRISM.