Merge pull request #2576 from GaloisInc/bh/no-heapster

Remove heapster package (#2574).

Author: brianhuffman

.github/ci.sh

@@ -104,7 +104,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
@@ -470,42 +469,7 @@ jobs:
           publish_dir: gh-pages
           keep_files: true
 
-  mr-solver-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
-
-      - working-directory: examples/mr_solver
-        shell: bash
-        run: |
-          saw monadify.saw
-          saw mr_solver_unit_tests.saw
-
-  heapster-tests:
+  saw-core-coq-tests:
     needs: [build]
     strategy:
       fail-fast: false
@@ -542,10 +506,6 @@ jobs:
 
       - 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
@@ -554,10 +514,6 @@ jobs:
         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 +1048,7 @@ jobs:
     runs-on: ubuntu-24.04
     needs:
       - build
-      - heapster-tests
+      - saw-core-coq-tests
       - crux-mir-comp-tests
       - saw-remote-api-tests
       - cabal-test

CHANGES.md

@@ -4,7 +4,72 @@ This release supports [version
 4](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#4) of
 `mir-json`'s schema.
 
-Nothing yet.
+## Changes
+
+* The deprecated Heapster, MRSolver, and Monadify features have been
+  removed.
+  The following SAW commands and types are no longer available:
+
+  - HeapsterEnv (type)
+  - Refnset (type)
+  - write_coq_cryptol_module_monadic
+  - mrsolver_set_debug_level
+  - mrsolver_set_debug_printing_depth
+  - mrsolver
+  - empty_rs
+  - addrefn
+  - addrefns
+  - mrsolver_with
+  - refines
+  - monadify_term
+  - set_monadification
+  - heapster_init_env
+  - heapster_init_env_debug
+  - heapster_init_env_from_file
+  - heapster_init_env_from_file_debug
+  - heapster_init_env_for_files
+  - heapster_init_env_for_files_debug
+  - heapster_get_cfg
+  - heapster_define_opaque_perm
+  - heapster_define_recursive_perm
+  - heapster_define_reachability_perm
+  - heapster_define_recursive_shape
+  - heapster_define_perm
+  - heapster_define_llvmshape
+  - heapster_define_opaque_llvmshape
+  - heapster_define_rust_type
+  - heapster_define_rust_type_qual
+  - heapster_block_entry_hint
+  - heapster_gen_block_perms_hint
+  - heapster_join_point_hint
+  - heapster_find_symbol
+  - heapster_find_symbols
+  - heapster_find_symbol_with_type
+  - heapster_find_symbols_with_type
+  - heapster_find_symbol_commands
+  - heapster_find_trait_method_symbol
+  - heapster_assume_fun
+  - heapster_assume_fun_rename
+  - heapster_assume_fun_rename_prim
+  - heapster_assume_fun_multi
+  - heapster_typecheck_fun
+  - heapster_typecheck_fun_rename
+  - heapster_typecheck_mut_funs
+  - heapster_set_event_type
+  - heapster_print_fun_trans
+  - heapster_export_coq
+  - heapster_set_debug_level
+  - heapster_set_translation_checks
+  - heapster_trans_rust_type
+  - heapster_parse_test
+  - heapster_dump_ide_info
+
+* Function `write_coq_cryptol_primitives_for_sawcore` no longer
+  generates Coq translations of SAWCore modules `SpecM.sawcore` and
+  `CryptolM.sawcore`, which have been removed.
+  Accordingly, the second and third `String` arguments to
+  `write_coq_cryptol_primitives_for_sawcore` have been removed.
+
 
 # Version 1.4 -- date still TBD
 

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

@@ -90,8 +90,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