| Summary: | fix cvc5 on ppc64le | ||
|---|---|---|---|
| Product: | Libre-SOC's first SoC | Reporter: | Jacob Lifshay <programmerjake> |
| Component: | Source Code | Assignee: | Jacob Lifshay <programmerjake> |
| Status: | RESOLVED FIXED | ||
| Severity: | major | CC: | libre-soc-bugs, lkcl, programmerjake |
| Priority: | --- | ||
| Version: | unspecified | ||
| Hardware: | PC | ||
| OS: | Linux | ||
| See Also: | https://bugs.libre-soc.org/show_bug.cgi?id=883 | ||
| NLnet milestone: | NLnet.2021.02A.052.CryptoRouter | total budget (EUR) for completion of task and all subtasks: | 600 |
| budget (EUR) for this task, excluding subtasks' budget: | 600 | parent task for budget allocation: | 775 |
| child tasks for budget allocation: | The table of payments (in EUR) for this task; TOML format: |
[jacob]
amount = 600
submitted = 2023-06-05
paid = 2023-06-21
|
|
|
Description
Jacob Lifshay
2022-07-13 05:30:29 BST
tested nmigen, spec_hdl_smtlib2_real_div now passes on ppc64le with the fixed cvc5. I pushed the fixed branch to: https://git.libre-soc.org/?p=cvc5.git;a=summary lkcl, you need to set that to public. once that's done, the dev-env-setup scripts can be changed to use the fix-ppc64le branch until cvc5 upstream accepts my PR. (In reply to Jacob Lifshay from comment #0) > https://bugs.libre-soc.org/show_bug.cgi?id=883#c7 > > PR: https://github.com/cvc5/cvc5/pull/8955 The PR was merged upstream. I pushed that to our cvc5 mirror. all that's left is updating dev-env-setup.git cvc5 1.0.1 was released a few days ago, it includes the ppc64le build fixes. I updated dev-env-setup.git to use that version after some testing on the talos and my desktop. https://git.libre-soc.org/?p=dev-env-setup.git;a=blob;f=hdl-tools-yosys;h=5b54555e527669039e32d945d15236f39b04629f;hb=HEAD unrelated: i noticed other repos (yices, z3) installed by hdl-tools-yosys use whatever is the latest commit on the upstream repos, rather than picking a particular commit/tag for reproducibility -- imho that should probably be fixed. |