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-the-ar-u-option
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
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
