Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
This unusual PR is sent to another PR (#1217), to shorten the CI building time with expk kernel.
Previously, examples/cv_compute is always built and examples/bootstrap was part of EX2DIR (level 2 examples not part of the CI tests when sending PRs). Now cv_compute depends on bootstrap, and both them should be tested as part of CI but only for the stdknl (which the new cv_compute facility only supports), so I moved them into EXDIR (level 1 examples, part of one-hour CI tests).
This unusual PR is sent to another PR (#1217), to shorten the CI building time with
expkkernel.Previously,
examples/cv_computeis always built andexamples/bootstrapwas part ofEX2DIR(level 2 examples not part of the CI tests when sending PRs). Nowcv_computedepends onbootstrap, and both them should be tested as part of CI but only for thestdknl(which the new cv_compute facility only supports), so I moved them intoEXDIR(level 1 examples, part of one-hour CI tests).