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 ------------------------------------------------------------------------------ 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
