Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Put solver bindists into different artifacts than non-solver bindists #1884

Closed
RyanGlScott opened this issue Jun 28, 2023 · 0 comments · Fixed by #1885
Closed

Put solver bindists into different artifacts than non-solver bindists #1884

RyanGlScott opened this issue Jun 28, 2023 · 0 comments · Fixed by #1885
Labels
CI Continuous integration

Comments

@RyanGlScott
Copy link
Contributor

Currently, if you look at a downloads page for a SAW CI workflow, it looks something like this:

saw-script

The saw-1.0.0.99-ubuntu-22.04-x86_64 (GHC 8.10.7) artifact is over 200 megabytes in size! While SAW binaries are somewhat on the large side, I wouldn't expect them to be that large. Part of the reason for it being so large is that this artifact actually includes two bindists: one SAW bindist that includes SMT solvers, and another bindist that doesn't include SMT solvers. Most of the time, I only want to download the bindist that doesn't include the solvers, which means I end up downloading far more than I ever really want.

I would prefer that the solver bindists be split up from the non-solver bindists on the downloads page, similarly to how Cryptol handles it:

cryptol

Notice that the *-with-solvers artifacts are now separate. This wouldn't be too difficult to accomplish in SAW's CI. Currently, we have:

- if: matrix.ghc == '8.10.7'
uses: actions/upload-artifact@v2
with:
name: ${{ steps.config.outputs.name }} (GHC ${{ matrix.ghc }})
path: "${{ steps.config.outputs.name }}.tar.gz*"
if-no-files-found: error
retention-days: ${{ needs.config.outputs.retention-days }}
- if: matrix.ghc == '8.10.7'
uses: actions/upload-artifact@v2
with:
name: ${{ steps.config.outputs.name }} (GHC ${{ matrix.ghc }})
path: "${{ steps.config.outputs.name }}-with-solvers.tar.gz*"
if-no-files-found: error
retention-days: ${{ needs.config.outputs.retention-days }}

Notice that although these use different paths, they are both grouped under the same ${{ steps.config.outputs.name }} (GHC ${{ matrix.ghc }}) name. To fix this issue, it would suffice to change the with-solvers step to use the name ${{ steps.config.outputs.name }}-with-solvers (GHC ${{ matrix.ghc }}), like how Cryptol does it.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
CI Continuous integration
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant