cv translator

[hrutvik]

Work ported from CakeML/cakeml#985, enabling use of cv_compute mostly by supporting automated translations into the :cv type.

[binghe]

The CI tests in this branch has shown that, with stdknl kernel the entire CI completed in slightly more than 1 hour, same as before; but with expk kernel now the CI needs almost 5 hours [1] to complete. Do we have a good explanation for this phenomenon?

[1] https://github.com/HOL-Theorem-Prover/HOL/actions/runs/8437841269

[binghe]

I think I know what's happening: 253 minutes (more than 4 hours) are spent inside examples/bootstrap:

#17 17341.1 compiler_asm.s                                  examples/bootstrap(253m)     OK

This example was previously disabled for expk kernel, i.e. only enabled for stdknl, in src/parallel_builds/core/Holmakefile:

ifeq ($(KERNELID),stdknl)
INCLUDES += ../../../examples/bootstrap
endif

But now the changes in examples/cv_compute/Holmakefile has put that folder into INCLUDES, causing it being built forcely also under expk kernel:

INCLUDES = $(HOLDIR)/src/num/theories/cv_compute/automation/ \
           $(HOLDIR)/examples/bootstrap

[mn200]

Having just spoken with @hrutvik and @myreen I think there's at least two good ways of fixing this that should be fairly imminent.

[binghe]

I've sent a PR (#1218) (to @hrutvik ) for the cv_translator branch. Because it's not for merging into develop, there's no CI tests triggered, but the tests in my personal repository have shown that, now the CI tests go back to ~1 hour for both stdknl and expk [1]. Please consider merging it.

[1] https://github.com/binghe/HOL/actions/runs/8554133882

[binghe]

Having just spoken with @hrutvik and @myreen I think there's at least two good ways of fixing this that should be fairly imminent.

sorry, I didn't notice this comment... If you have other better solutions, then my above PR #1218 can be ignored.

[mn200]

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 expk issue soon? (Can always take @binghe’s fix otherwise.)

[binghe]

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 expk issue soon? (Can always take @binghe’s fix otherwise.)

GitHub kills CIs only after they exceed 6 hours. The present CI failure on expk indicates something wrong in the code changes, or Poly/ML somehow crashed...

[binghe]

Since the branch to be merged is inside this repository, I suggest using the "self-runner" GitHub action to test it again.

[myreen]

Is there any prospect of the "right" fix coming for the expk issue soon?

Depends on your definition of "soon". I'm working on a proper fix, i.e. to change all heavy uses of EVAL to cv_eval in examples/bootstrap. However, I might not get it done for another week, not because it's taking so long to do the fix, instead it's because a lot of high priority things with deadlines are getting in the way of working on this fix.

[binghe]

Is there any prospect of the "right" fix coming for the expk issue soon?

Depends on your definition of "soon". I'm working on a proper fix, i.e. to change all heavy uses of EVAL to cv_eval in examples/bootstrap. However, I might not get it done for another week, not because it's taking so long to do the fix, instead it's because a lot of high priority things with deadlines are getting in the way of working on this fix.

I'm actually waiting for the rational-related code changes to be merged into develop, for sending more related PRs. Just a suggestion: can we first confirm&fix the CI test failure on expk, or just go back to 3 commits go when expk test passed in 5 hours, then with my trivial changes to shorten it to 1 hour, so that the present work can be merged? The optimization of examples/bootstrap can be done later in another PR...

[myreen]

You could just cherrypick the commit that adds the theorems about the rationals.

[binghe]

You could just cherrypick the commit that adds the theorems about the rationals.

Thank you for your authorisation on this!

[mn200]

Thanks for this!

(I had to resolve a minor/trivial merge conflict pulling this across; regression tests will check if I did it right...)