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.

Sign up for GitHub

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

Jump to bottom

Allow specifying a path to z3_problems #877

Open
Timmmm opened this issue Jan 14, 2025 · 1 comment · May be fixed by #878
Open

Allow specifying a path to z3_problems #877

Timmmm opened this issue Jan 14, 2025 · 1 comment · May be fixed by #878

Comments

@Timmmm
Copy link
Contributor

Timmmm commented Jan 14, 2025

It would be helpful if a custom filename for z3_problems could be used.

  1. This would allow placing it in a build directory, rather than just the current directory where it often has to be .gitignored.
  2. I guess this might help with parallel builds, e.g. having a unique file for RV32 and RV64 could mean they don't keep overwriting each other. I don't know if it perfectly handles parallelism either - if one Sail compiler is writing to z3_problems while another is reading it does that screw things up? (We run with 4 way parallelism and haven't seen that but I guess it would be quite unlikely anyway.)
@Timmmm Timmmm linked a pull request Jan 14, 2025 that will close this issue
Open
@Alasdair
Copy link
Collaborator

In theory, there could be a bug in the parallel case. It might be hard to trigger as I already made the code robust against parsing errors (it just doesn't use the file) to handle failures we were occasionally seeing in the github CI

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Add --memo-z3-path option Timmmm/sail
2 participants
@Alasdair @Timmmm