CI job with minimal dependencies (#520)

.github/workflows/buildtest.yml

@@ -70,7 +70,18 @@ jobs:
  AllSanitizers: "ON",
  cmakeArgs: "-DMSAT_ROOT="
  }
-
+ - {name: "Minimal dependencies",
+ baseImg: "storm-basesystem:minimal_dependencies",
+ buildType: "Debug",
+ Gurobi: "OFF",
+ Soplex: "OFF",
+ Spot: "OFF",
+ Developer: "ON",
+ ClnExact: "OFF",
+ ClnRatfunc: "ON",
+ AllSanitizers: "ON",
+ cmakeArgs: "-DMSAT_ROOT="
+ }
  steps:
  - name: Git clone
  uses: actions/checkout@v4

CMakeLists.txt

@@ -178,8 +178,14 @@ else()
 ENDIF()
 message(STATUS "Storm - Detected operating system ${OPERATING_SYSTEM}.")
 
-set(SHIPPED_CARL_USE_CLN_NUMBERS ON)
-set(SHIPPED_CARL_USE_GINAC ON)
+# Set compile flags for dependencies
+if(STORM_USE_CLN_EA OR STORM_USE_CLN_RF)
+ set(SHIPPED_CARL_USE_CLN_NUMBERS ON)
+ set(SHIPPED_CARL_USE_GINAC ON)
+else()
+ set(SHIPPED_CARL_USE_CLN_NUMBERS OFF)
+ set(SHIPPED_CARL_USE_GINAC OFF)
+endif()
 
 # Warning for Apple Silicon
 if(APPLE_SILICON)

doc/update_resources.md

@@ -15,6 +15,14 @@ In case a new patch needs to be created follow these steps:
 4. Resolve issues, make changes, and commit them
 5. Create a new patch file via `git format-patch <tag> --stdout > eigen.patch`, where `<tag>` is the tag, branch or commit from step 1
 
+## GLPK
+
+To update GLPK, download the new sources from [here](https://ftp.gnu.org/gnu/glpk/) and put them into `$STORM_DIR/resources/3rdparty/glpk-5.0`.
+We remove some unnecessary files to reduce the size of the folder:
+1. Remove the folders `doc` and `examples`
+2. Remove these folders from the `SUBDIRS` in `Makefile.am`
+3. Recreate the `configure` script via `autoconf`
+
 ## googletest / gtest
 
 To update gtest, simply download the new sources from [here](https://github.com/google/googletest/releases) and put them to `$STORM_DIR/resources/3rdparty/googletest`.
@@ -29,7 +37,7 @@ We add some extra code to gtest located in `$STORM_DIR/src/test/storm_gtest.h`.
 
 ## nlohmann/json for Modern C++
 
-The currently shipped version is forked from the [official github](https://github.com/nlohmann/json) commit `6eab7a2b187b10b2494e39c1961750bfd1bda500`.
+The currently shipped version is forked from the [official GitHub](https://github.com/nlohmann/json) commit `6eab7a2b187b10b2494e39c1961750bfd1bda500`.
 We extended the library towards rational numbers, see [here](../resources/3rdparty/modernjson/README_STORM.md).
 To update, you can follow these steps:
 
@@ -38,13 +46,13 @@ To update, you can follow these steps:
 3. The diff for that commit shows you the exact modifications we made.
 4. Merge the json version you want to update to into your branch.
 5. Resolve potential conflicts and review what has changed, in particular if it affects handling of floating point numbers.
-7. When this is all done, copy the contents back into the storm directory. Make sure to not apply any unnecessary code formatting to keep the diff smallish.
-8. *Update the commit hash mentioned in this document*
+6. When this is all done, copy the contents back into the storm directory. Make sure to not apply any unnecessary code formatting to keep the diff smallish.
+7. *Update the commit hash mentioned in this document*
 
 
 ## parallel hashmap
 
-Download the new sources from [github](https://github.com/greg7mdp/parallel-hashmap) and put them to `$STORM_DIR/resources/3rdparty/parallel_hashmap/`.
+Download the new sources from [GitHub](https://github.com/greg7mdp/parallel-hashmap) and put them to `$STORM_DIR/resources/3rdparty/parallel_hashmap/`.
 Remove directories that are not needed, e.g, `rm -r doc examples html css benchmark tests index.html`.
 
 
@@ -62,7 +70,7 @@ To update, you can follow these steps:
 1. Check out the above commit in a separate repository
 2. Copy the contents of `$STORM_DIR/resources/3rdparty/sylvan` to the repository you just checked out and commit to a fresh branch
 3. The diff for that commit shows you the modifications we made to the sylvan source code. 
- We also include *lace* (`lace.c` and `lace.h`) which is a dependency of sylvan that is normally downloaded by sylvans build scripts via cmake `FetchContent`.
+ We also include *lace* (`lace.c` and `lace.h`) which is a dependency of sylvan that is normally downloaded by sylvan's build scripts via cmake `FetchContent`.
  As this requires cmake 3.14 and complicates the overall build process, we decided to ship the files `lace.c` and `lace.h` directly (see Storm commit 095e78a897b01db20df95bca89e746229e6a85c8)
 4. Merge the `master` of sylvan (or whatever version you want to update to) into your branch
 5. Resolve potential conflicts and review what has changed, in particular if it affects the API that Storm uses

resources/3rdparty/glpk-5.0/Makefile.am

@@ -2,6 +2,6 @@
 
 ACLOCAL_AMFLAGS=-I m4
 
-SUBDIRS = src examples
+SUBDIRS = src
 
 ## eof ##

resources/3rdparty/glpk-5.0/Makefile.in

@@ -156,6 +156,7 @@ ECHO_T = @ECHO_T@
 EGREP = @EGREP@
 EXEEXT = @EXEEXT@
 FGREP = @FGREP@
+FILECMD = @FILECMD@
 GREP = @GREP@
 INSTALL = @INSTALL@
 INSTALL_DATA = @INSTALL_DATA@
@@ -170,6 +171,7 @@ LIBTOOL = @LIBTOOL@
 LIPO = @LIPO@
 LN_S = @LN_S@
 LTLIBOBJS = @LTLIBOBJS@
+LT_SYS_LIBRARY_PATH = @LT_SYS_LIBRARY_PATH@
 MAKEINFO = @MAKEINFO@
 MANIFEST_TOOL = @MANIFEST_TOOL@
 MKDIR_P = @MKDIR_P@
@@ -247,7 +249,7 @@ top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
 ACLOCAL_AMFLAGS = -I m4
-SUBDIRS = src examples
+SUBDIRS = src
 all: config.h
  $(MAKE) $(AM_MAKEFLAGS) all-recursive
 

resources/3rdparty/glpk-5.0/config.h.in

@@ -1,30 +1,88 @@
-/* config.h.in (GLPK configuration template file) */
+/* config.h.in. Generated from configure.ac by autoheader.  */
 
-#undef HAVE_SYS_TIME_H
-/* defined if the <sys/time.h> header can be used */
+/* N/A */
+#undef HAVE_DLFCN
 
+/* Define to 1 if you have the <dlfcn.h> header file. */
+#undef HAVE_DLFCN_H
+
+/* N/A */
 #undef HAVE_GETTIMEOFDAY
-/* defined if the gettimeofday function can be used */
 
+/* N/A */
 #undef HAVE_GMP
-/* defined if the GNU MP bignum library is available */
-/* requires <gmp.h> and -lgmp */
 
+/* Define to 1 if you have the <inttypes.h> header file. */
+#undef HAVE_INTTYPES_H
+
+/* Define to 1 if you have the `m' library (-lm). */
+#undef HAVE_LIBM
+
+/* N/A */
 #undef HAVE_LTDL
-/* defined if the GNU Libtool shared library support is enabled */
-/* requires <ltdl.h> and -lltdl */
 
-#undef HAVE_DLFCN
-/* defined if the POSIX shared library support is enabled */
-/* requires <dlfcn.h> */
+/* Define to 1 if you have the <memory.h> header file. */
+#undef HAVE_MEMORY_H
 
-#undef ODBC_DLNAME
-/* ODBC shared library name if this feature is enabled */
+/* Define to 1 if you have the <stdint.h> header file. */
+#undef HAVE_STDINT_H
+
+/* Define to 1 if you have the <stdlib.h> header file. */
+#undef HAVE_STDLIB_H
+
+/* Define to 1 if you have the <strings.h> header file. */
+#undef HAVE_STRINGS_H
+
+/* Define to 1 if you have the <string.h> header file. */
+#undef HAVE_STRING_H
+
+/* Define to 1 if you have the <sys/stat.h> header file. */
+#undef HAVE_SYS_STAT_H
+
+/* N/A */
+#undef HAVE_SYS_TIME_H
 
+/* Define to 1 if you have the <sys/types.h> header file. */
+#undef HAVE_SYS_TYPES_H
+
+/* Define to 1 if you have the <unistd.h> header file. */
+#undef HAVE_UNISTD_H
+
+/* Define to the sub-directory where libtool stores uninstalled libraries. */
+#undef LT_OBJDIR
+
+/* N/A */
 #undef MYSQL_DLNAME
-/* MySQL shared library name if this feature is enabled */
 
+/* N/A */
+#undef ODBC_DLNAME
+
+/* Name of package */
+#undef PACKAGE
+
+/* Define to the address where bug reports for this package should be sent. */
+#undef PACKAGE_BUGREPORT
+
+/* Define to the full name of this package. */
+#undef PACKAGE_NAME
+
+/* Define to the full name and version of this package. */
+#undef PACKAGE_STRING
+
+/* Define to the one symbol short name of this package. */
+#undef PACKAGE_TARNAME
+
+/* Define to the home page for this package. */
+#undef PACKAGE_URL
+
+/* Define to the version of this package. */
+#undef PACKAGE_VERSION
+
+/* Define to 1 if you have the ANSI C header files. */
+#undef STDC_HEADERS
+
+/* N/A */
 #undef TLS
-/* thread local storage-class specifier for re-entrancy (if any) */
 
-/* eof */
+/* Version number of package */
+#undef VERSION