Open hai-nguyen-van opened 1 year ago
Ah, I have a suspicion this is because the MPL install scripts are only slightly modified from MLton's, so it might be overwriting some of the local install of MLton when doing make install
.
Perhaps it's enough to install MPL somewhere else, such as make install PREFIX=/opt/mpl
?
Alternatively, you could try out mpl-switch
, which is a small python script to help manage local installs of MPL. It installs to a directory ~/.mpl/
and lets you have multiple versions of MPL installed simultaneously, so it should work with any local install of MLton you have, too.
I am unable to build a project with MLton after MPL has been installed using its
make install
. I need to build this project usingmake hmc
and I face the following errors:I have discussed with @MatthewFluet about a very similar issue (https://github.com/MLton/mlton/issues/488#issuecomment-1397036002) who seems to indicate that the problem comes from MPL rather than MLton. Interestingly, I am able to build project using the root Docker
shwestrick/mpl
... so I don't really understand 🤔