Building under Moscow ML is still broken

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

Building under Moscow ML is still broken #670

Closed binghe closed 5 years ago

binghe commented 5 years ago

Hi,

currently the building of HOL under Moscow ML is still broken in both master and develop at the following position:

Holmake: Compiling alist_treeLib.sml
File "alist_treeLib.sml", line 253, characters 37-38:
!     val time = Portable.timestamp () - start
!                                      ^
! Overloaded - cannot be applied to argument(s) of type time
Build failed in directory /Users/binghe/ML/HOL.mosml/src/finite_maps

The solution is out of my knowledge, so I have to report this issue instead of submitting a PR.

Regards,

Chun Tian

binghe commented 5 years ago

Hi Michael,

thanks for your fixes. It's almost successful, except at the end it shows this error:

Directory /Users/binghe/ML/HOL.mosml/help/Docfiles:  100%
...ASCII Docfiles done
Generating HTML versions of Docfiles...
Directory /Users/binghe/ML/HOL.mosml/help/Docfiles:  100%
...HTML Docfiles done
Building Help DB
sh: /Users/binghe/ML/HOL.mosml/help/src-sml/makebase.exe: No such file or directory
Couldn't make help database

The source file help/src-sml/makebase.sml exists, but somehow it's not built into .exe. Can you reproduce it?

--Chun