Skip to content

Conversation

@brianhuffman
Copy link
Contributor

No description provided.

@RyanGlScott
Copy link
Contributor

Make sure to also remove the following:

  • The hobbits source repository package, which we no longer need to use:

    saw-script/cabal.project

    Lines 45 to 48 in 68d6efc

    source-repository-package
    type: git
    location: https://github.com/eddywestbrook/hobbits.git
    tag: 70963e0e3eba2b16f6fc030acb582e8100955e47

  • This part of the CI configuration:

    - heapster-tests

    (I think this bit is what is causing the CI not to run on your pull request.)

@brianhuffman brianhuffman force-pushed the bh/no-heapster branch 7 times, most recently from 104003d to 24b5f5a Compare September 4, 2025 13:05
@brianhuffman brianhuffman marked this pull request as ready for review September 5, 2025 17:22
Copy link
Contributor

@sauclovian-g sauclovian-g left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This also definitely needs a changelog entry...

...which should also specifically call out that the signature of write_coq_cryptol_primitives_for_sawcore has changed.

@sauclovian-g
Copy link
Contributor

It looks like heapster/examples/bc-annot/foo.saw came back by accident.

Also, test_type_errors/err053 uses the HeapsterEnv type as a deprecated type to test on, so it will blow up when that's removed. There isn't any other deprecated type at present so we might need to either create a dummy one (which is kind of annoying) or disable the test (which is also kind of annoying).

@brianhuffman
Copy link
Contributor Author

It looks like heapster/examples/bc-annot/foo.saw came back by accident.

Oops, it looks like I made a mistake with my rebase. I'll give it another try.

@brianhuffman brianhuffman force-pushed the bh/no-heapster branch 2 times, most recently from 2c4ab09 to dd0df02 Compare September 15, 2025 21:44
@sauclovian-g
Copy link
Contributor

Oops, it looks like I made a mistake with my rebase. I'll give it another try.

Stuff happens :-)

Also document the changed type for
write_coq_cryptol_primitives_for_sawcore.
Also introduce new deprecated type "__DEPRECATED__" so that we
have a type to use with expected-error tests.
Copy link
Contributor

@sauclovian-g sauclovian-g left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One last kibitz, then I think you can merge it :-)

CHANGES.md Outdated

* The deprecated Heapster, MRSolver, and Monadify features have been
removed.
The following SAW commands are no longer available:
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Might also mention the RefnSet type here since it's not immediately obvious to passersby that it's linked to this stuff. (HeapsterEnv pretty obviously is, so mentioning it probably doesn't matter one way or the other.)

@brianhuffman brianhuffman merged commit bb4e70e into master Sep 17, 2025
12 checks passed
@brianhuffman brianhuffman deleted the bh/no-heapster branch September 17, 2025 19:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants