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
cv translator #1217
cv translator #1217
Conversation
Co-authored-by: Magnus Myreen <myreen@chalmers.se>
Co-authored-by: Magnus Myreen <myreen@chalmers.se>
Co-authored-by: Magnus Myreen <myreen@chalmers.se>
Co-authored-by: Magnus Myreen <myreen@chalmers.se>
- Unicode violations - Missing `INCLUDES` in `Holmakefile` - Update a `README`
The CI tests in this branch has shown that, with [1] https://github.com/HOL-Theorem-Prover/HOL/actions/runs/8437841269 |
I think I know what's happening: 253 minutes (more than 4 hours) are spent inside
This example was previously disabled for
But now the changes in
|
I don't know when GitHub kills CIs that are taking too long, but that may be the explanation for the failure above. Is there any prospect of the "right" fix coming for the |
GitHub kills CIs only after they exceed 6 hours. The present CI failure on |
Since the branch to be merged is inside this repository, I suggest using the "self-runner" GitHub action to test it again. |
Depends on your definition of "soon". I'm working on a proper fix, i.e. to change all heavy uses of |
I'm actually waiting for the rational-related code changes to be merged into |
You could just cherrypick the commit that adds the theorems about the rationals. |
Thank you for your authorisation on this! |
Note that this commit leaves a cheat that needs removing.
Thanks for this! (I had to resolve a minor/trivial merge conflict pulling this across; regression tests will check if I did it right...) |
Work ported from CakeML/cakeml#985, enabling use of
cv_compute
mostly by supporting automated translations into the:cv
type.