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...
Ce jour même il y a 35 ans, un homme entra dans un cours à Polytechnique Montréal. Armé d'un fusil, il sépara les hommes des femmes. Finalement il tua 14 femmes pour leur audace d'étudier en ingénierie.
Souvenons-nous de ces quatorze femmes. Combattons la misogynie, même en petits gestes—supporter nos amies, réagir à une remarque sexiste d'un ami, examiner notre sexisme internalisé.
Qqs liens supplémentaires en réplique.
(Le français en réplique.)
35 years ago today, a man walked into an engineering class at Polytechnique Montréal. Firearm in hand, he separated the men and women, and killed 14 women for daring to aspire to a man's profession.
Let us remember the fourteen. Let us fight against misogyny, even in small ways: nudge friends for off-colour remarks. Support women. Challenge your own internalised misogyny.
Some links in thread.
Ted B. Falken, tu Asesor Extraño Clifford/🍩⇔☕️/🔻
Alex Nelson
Laurabunny