On 3/28/2019 11:24 AM, Gergely Buday wrote:
Eliot Moss wrote:
My whole setup on my laptop is Cygwin based. If I can use Cygwin HOL4 and Windows polyml, that would be ok, but I can also imagine a number of ways that would break, particularly around handling filenames ... What do you think?
I used MobaXterm to run HOL4. HOL4 runs fine on it, unfortunately the hol-vim plugin does not work there.
MobaXterm is a cygwin-based distribution for Windows:
https://mobaxterm.mobatek.net/download-home-edition.html
For compiling polyml on MobaXterm you need a minor tweak in configure:
https://stackoverflow.com/questions/55097775/compiling-poly-ml-on-mobaxterm-...
And you need to install make and g++ via mobapt or apt-get.
Thank you, Gergely for the suggestions.
... but I already have a significant Cygwin installation. This would seem to duplicate that. (And it's known that having more than one Cygwin installation can lead to interferences if one does not take particular care.) I'm not quite seeing the advantages here ...
I run HOL4 under emacs and use unicode capabilities and the HOL4 emacs setup. (So lacking vim won't bother me, but not operating with emacs would.) I run this all under Cygwin's X windows support.
Here's a further wondering. It sounds as if your setup is using a (possibly stripped down) Cygwin to build polyml. Are you running polyml 5.7, 5.7.1, or 5.8? An earlier version worked well for me, but these later ones fail with HOL4 unless I use -j1 (the default is -j4) for Hol's build, Holmake, etc. David has fixed the failure-to-compile problem that I reported, so 5.8 should compile going forward. So, does your setup actually work properly with polyml 5.8? I would be a bit surprised unless you're actually doing a Windows native build instead of a Cygwin/MobaXterm build.
Regards - Eliot