Remove heapster package (#2574).

Author: brianhuffman

.github/ci.sh

@@ -103,7 +103,6 @@ haddock() {
     saw:saw-core-sbv
     saw:saw-core-aig
     saw:saw-core-coq
-    saw:heapster
     saw:saw-central
     saw:saw-script
     saw:saw-server

.github/workflows/ci.yml

@@ -194,7 +194,6 @@ jobs:
             cryptol-saw-core-tests
             crux-mir-comp-tests
             saw-core-coq-tests
-            heapster-prover-tests
           dest: dist-tests
 
       # In the next 2 steps, we upload to different names depending on whether
@@ -505,59 +504,6 @@ jobs:
           saw monadify.saw
           saw mr_solver_unit_tests.saw
 
-  heapster-tests:
-    needs: [build]
-    strategy:
-      fail-fast: false
-      matrix:
-        os: [ubuntu-24.04, macos-14]
-    runs-on: ${{ matrix.os }}
-    steps:
-      - uses: actions/checkout@v4
-        with:
-          submodules: true
-
-      - shell: bash
-        run: .github/ci.sh install_system_deps
-        env:
-          BUILD_TARGET_OS: ${{ matrix.os }}
-          BUILD_TARGET_ARCH: ${{ runner.arch }}
-
-      - uses: actions/download-artifact@v4
-        with:
-          name: "${{ matrix.os }}-bins"
-          path: dist/bin
-
-      - name: Update PATH to include SAW
-        shell: bash
-        run: |
-          chmod +x dist/bin/*
-          echo $GITHUB_WORKSPACE/dist/bin >> $GITHUB_PATH
-
-      - uses: ocaml/setup-ocaml@v3
-        with:
-          ocaml-compiler: "4.14"
-
-      - run: opam repo add coq-released https://coq.inria.fr/opam/released
-
-      - run: opam install -y coq=8.15.2 coq-bits=1.1.0
-
-        # If you change the entree-specs commit below, make sure you update the
-        # documentation in saw-core-coq/README.md accordingly.
-      - run: opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#f104f6b3e6fe5987d543d90265cdc52f532de5fe
-
-      # FIXME: the following steps generate Coq libraries for the SAW core to
-      # Coq translator and builds them; if we do other Coq tests, these steps
-      # should become their own build artifact, to avoid re-compiling the Coq
-      # libraries
-      - working-directory: saw-core-coq/coq
-        shell: bash
-        run: opam exec -- make -j
-
-      - working-directory: heapster/examples
-        shell: bash
-        run: opam exec -- make -j
-
   crux-mir-comp-tests:
     needs: [build]
     strategy:
@@ -1092,7 +1038,6 @@ jobs:
     runs-on: ubuntu-24.04
     needs:
       - build
-      - heapster-tests
       - crux-mir-comp-tests
       - saw-remote-api-tests
       - cabal-test

CONTRIBUTING.md

@@ -255,8 +255,6 @@ The top-level repository directories are:
   solver queries using the [What4](https://github.com/GaloisInc/what4)
   library.
 
-* `heapster` - The Heapster tool.
-
 * `saw-central` - A library containing the bulk of SAW.
 
 * `saw-script` - A library containing the SAWScript interpreter.

build.sh

@@ -84,8 +84,7 @@ tgt_build() {
                 test-suite:integration-tests test-suite:saw-core-tests \
                 test-suite:crux-mir-comp-tests \
                 test-suite:cryptol-saw-core-tests \
-                test-suite:saw-core-coq-tests \
-                test-suite:heapster-prover-tests
+                test-suite:saw-core-coq-tests
 
     echo "rm -rf bin && mkdir bin"
     rm -rf bin && mkdir bin

cabal.project

@@ -42,11 +42,6 @@ packages:
     deps/rme/rme
     deps/rme/rme-what4
 
-source-repository-package
-    type: git
-    location: https://github.com/eddywestbrook/hobbits.git
-    tag: 70963e0e3eba2b16f6fc030acb582e8100955e47
-
 -- enable ghc >= 9.8's additional build parallelism
 semaphore: true
 

doc/developer/developer.md

@@ -151,18 +151,16 @@ The following can be run with `cabal test`:
 - `saw-core-tests`
 - `cryptol-saw-core-tests`
 - `saw-core-coq-tests`
-- `heapster-prover-tests`
 - `crux-mir-comp-tests`
 
-There are three other sets of tests:
+There are two other sets of tests:
 
 - `saw-remote-api tests`
 - `mr-solver-tests`
-- `heapster-tests`
 
 The saw-remote-api tests can be run with the script
 `saw-remote-api/scripts/run_rpc_tests.sh`.
-The other two are run by the CI but are not currently really intended
+The other one is run by the CI but is not currently really intended
 to be run by hand.
 
 The s2n proofs that are also run by the CI are driven by scripts found

doc/developer/issue-labels.md

@@ -259,9 +259,6 @@ Cryptol-to-saw-core translation in the cryptol-saw-core package.
 
 * _subsystem: hardware_ - issues related to verification of hardware.
 
-* _subsystem: heapster_ - issues related to memory verification using
-Heapster.
-
 * _subsystem: MRSolver_ - issues related to the Mr. Solver
 monadic-recursive solver in Heapster.