Hi Makarius,
Yeah, this is why I never succeeded in building PolyML on Windows in Cygwin
or MinGW. When the building process stopped at some assembly code files, I
thought they're for Microsoft compilers only. I don't believe PolyML
depends on any deep GCC feature which is only available in old versions,
because PolyML builds correctly on Linux and Mac using whatever versions of
GCC. PolyML maintainers may be interested enough to fix the building
issues, if both HOL-4 and Isabelle want to have Windows versions based on
easily build-able PolyML.
And thank you very much for pointing out the hidden Mercurial repository of
Isabelle [1] ^_^ Now I can see how "active" it is for a "not dying" theorem
prover: stable 10-20 code commits on everyday basis, and new theories keep
going into core Isabelle libraries.
Regards,
Chun Tian
[1] hg clone http://isabelle.in.tum.de/repos/isabelle/
On 18 January 2017 at 11:54, Makarius <wenz...@in.tum.de> wrote:
> On 17/01/17 15:24, Chun Tian (binghe) wrote:
> > Sorry, I re-checked my Isabelle environment and found that the PolyML in
> > Isabelle is actually built by GCC (mingw versions), so my statement
> > about "PolyML cannot be built in ..." was completely wrong. The rest
> > ideas should still hold.
>
> It is indeed built with MinGW, but that is very difficult to do. See
> http://isabelle.in.tum.de/repos/isabelle/raw-file/
> Isabelle2016-1/Admin/polyml/INSTALL-MinGW
> which is just a reminder for me for the precise versions need to be
> used. Otherwise it won't work.
>
> Maybe we can open a discussion on the Poly/ML mailing list, if this
> rather old version of gcc on MinGW is still needed, or if things can be
> updated and simplified.
>
>
> Concerning system structures in ML, see also:
>
> http://isabelle.in.tum.de/repos/isabelle/raw-file/
> Isabelle2016-1/src/Pure/ML/ml_system.ML
>
> http://isabelle.in.tum.de/repos/isabelle/raw-file/Isabelle2016-1/src/Pure/
> System/bash.ML
>
> Here the bash.exe is the one from Cygwin -- that is required for add-on
> tools of Isabelle.
>
>
> Makarius
>
>
--
---
Chun Tian (binghe)
University of Bologna (Italy)
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, SlashDot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
