Moscow ML builds broken after `cv_translator`

HOL-Theorem-Prover / HOL

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.

https://hol-theorem-prover.org

Other

621 stars 140 forks source link

Moscow ML builds broken after `cv_translator` #1226

Closed binghe closed 5 months ago

binghe commented 5 months ago

Holmake: Compiling cv_repTheory.sig
Holmake: Compiling cv_repTheory.sml
Holmake: Compiling cv_miscLib.sml
Holmake: Compiling cv_memLib.sml
File "cv_memLib.sml", line 33, characters 51-52:
!     cv_print Verbose ("Took " ^ Time.fmt 1 (finish - start) ^ " seconds.\n");
!                                                    ^
! Overloaded - cannot be applied to argument(s) of type time
*** FATAL: Build failed in directory /Users/binghe/ML/HOL.mosml/src/parallel_builds/core

binghe commented 5 months ago

Full Moscow ML builds are too slow to be part of the CI, but perhaps a small build sequence of (selected) core theories could finish in 1-2 hours (so that we can put it into CI)?