Fixing --otknl builds (up to hol-base.art in src/boss)

[binghe]

Hi,

This PR tries to fix HOL's --otknl builds, mainly broken due to cv_compute work which now has implicit oracles on arithmetic (and some other) calculations (and thus not more produces complete proofs needed by OT proof logging).

The long term solution may be accepting this fact and produce "imperfect" OT articles leaving those computations as open assumptions. The present PR does the minimal fix to make sure "good" OT articles are still generated. Obviously it cannot support potential user theories depending on heavy arithmetic computations or the cv_compute kernel functions.

The old Arithconv.sml has been recovered as src/num/reduce/conv-old/Arithconv.sml and the existing cv-based version is moved to src/num/reduce/conv/Arithconv.sml. The old one is only used in --otknl builds.

Other fixes in this PR are due to cumulative core theory changes since the last time OT builds were checked.

Since the probability materials started to use real_of_ratTheory, the OT packages hol-integer, etc. must now be included for generating closed OT articles for probabilityTheory. But we are also in the process of upgrading the ring theories using examples/algebra and the old ring theory was another OT package hol-ring closely associated with hol-integer OT package (and then the frac and rational materials). I need to check if the old ring theorems are actually used in proving any (useful) integer theorems and then fix the rest of OT builds.

The Docker CI workflow is further extended with a very core build (up to parallel, i.e. finishes at src/boss) of --otknl. This is important to prevent it being broken in unnoticed way by future commits.

--Chun

[binghe]

A sample build of "hol-base" OT package can be found here: https://github.com/binghe/HOL/releases/tag/hol-base-1.3.0

[mn200]

Thanks for your work on this!

[binghe]

I think the following issue (please confirm) is caused by changes in this PR (i.e. the separation of src/num/reduce/conv): if you rebuild your HOL working directory, it will always rebuild the numheap even nothing has modified:

Building directory src/num/reduce/conv [05 May, 23:17:07]
Uploading files to /Users/binghe/ML/HOL.expk/sigobj
Building directory src/num/reduce/src [05 May, 23:17:07]
Uploading files to /Users/binghe/ML/HOL.expk/sigobj
Building directory src/num/arith/src [05 May, 23:17:07]
Uploading files to /Users/binghe/ML/HOL.expk/sigobj
Building directory src/num [05 May, 23:17:07]
Uploading files to /Users/binghe/ML/HOL.expk/sigobj
Building directory src/num/termination [05 May, 23:17:07]
numheap                                                                                                                                     (11s)     OK
Uploading files to /Users/binghe/ML/HOL.expk/sigobj
Building directory src/num/extra_theories [05 May, 23:17:19]
numpairTheory                                                                                                                                (1s)     OK
dividesTheory                                                                                                                                (1s)     OK
logrootTheory                                                                                                                                (3s)     OK
gcdTheory                                                                                                                                    (2s)     OK
bitTheory                                                                                                                                    (3s)     OK
numeral_bitTheory                  

[binghe]

I think the following issue (please confirm) is caused by changes in this PR (i.e. the separation of src/num/reduce/conv): if you rebuild your HOL working directory, it will always rebuild the numheap even nothing has modified:

Building directory src/num/reduce/conv [05 May, 23:17:07]
Uploading files to /Users/binghe/ML/HOL.expk/sigobj
Building directory src/num/reduce/src [05 May, 23:17:07]
Uploading files to /Users/binghe/ML/HOL.expk/sigobj
Building directory src/num/arith/src [05 May, 23:17:07]
Uploading files to /Users/binghe/ML/HOL.expk/sigobj
Building directory src/num [05 May, 23:17:07]
Uploading files to /Users/binghe/ML/HOL.expk/sigobj
Building directory src/num/termination [05 May, 23:17:07]
numheap                                                                                                                                     (11s)     OK
Uploading files to /Users/binghe/ML/HOL.expk/sigobj
Building directory src/num/extra_theories [05 May, 23:17:19]
numpairTheory                                                                                                                                (1s)     OK
dividesTheory                                                                                                                                (1s)     OK
logrootTheory                                                                                                                                (3s)     OK
gcdTheory                                                                                                                                    (2s)     OK
bitTheory                                                                                                                                    (3s)     OK
numeral_bitTheory                  

I think this annoying rebuilding is not caused by any changes here, but the failure of building src/HolSat/sat_solvers/zc2hs on macOS with Apple's default C++ compiler. I will create a separate issue.