#PolyML

2025-03-29

If you are trying to get HOL4 working on a Raspberry Pi, you need to use MoscowML.

Poly/ML native compilation is not really supported for Raspberry Pi, and its bytecode interpreter performs worse than MoscowML's bytecode interpreter anyways.

I learned this after spending a few frustrating days trying to get PolyML to build HOL4, fruitlessly, then gave Mosml a shot (and it worked like a charm).

The things you learn...

#HOL #MoscowML #PolyML #StandardML #RaspberryPi

2024-12-07
2024-12-07

Client Info

Server: https://mastodon.social
Version: 2025.04
Repository: https://github.com/cyevgeniy/lmst