Hi Chun
You may have a point, not sure about Poly ML woes...I was able to move a
bit further by cloning the latest HOL distro.
I get the configuration done now but as soon as I start the build I get a
Subscript error.
[adarbari@localhost HOL]$ bin/build
*** Using kernel spec --stdknl from earlier build command;
use one of --expk, --stdknl, --otknl to override
Cleaning out /home/adarbari/HOL/sigobj
/home/adarbari/HOL/sigobj cleaned
Building directory tools/set_mtime [22 May, 22:24:34]
Holmake failed with exception: Subscript
Build failed in directory /home/adarbari/HOL/tools/set_mtime (exited with
code 1)
[adarbari@localhost HOL]$
*Detailed log:*
[adarbari@localhost HOL]$ poly < tools-poly/smart-configure.sml
Poly/ML 5.7.1 Release
HOL smart configuration.
Determining configuration parameters: holdir OS poly polymllibdir
OS: linux
poly: /usr/local/bin/poly
polyc: /usr/local/bin/polyc
polymllibdir: /usr/local/lib
holdir: /home/adarbari/HOL
DOT_PATH: NONE
MLTON: NONE
Configuration will begin with above values. If they are wrong
press Control-C.
Will continue in 1 seconds.
Loading system specific functions
Compiling system specific functions (sml)
Beginning configuration.
Removing old quotation filter from bin/
Making mllex
Making mlyacc
Number of states = 95
Number of distinct rows = 47
Approx. memory size of trans. table = 6063 bytes
Making Holmake
Number of states = 1020
Number of distinct rows = 847
Approx. memory size of trans. table = 1734656 bytes
Making unquote.
Making holdeptool
Making build
Making heapname
Making buildheap
Making genscriptdep
Making hol-mode.el (for Emacs/XEmacs)
Making tools/vim/*
Generating bin/hol.
Finished configuration!
[adarbari@localhost HOL]$ bin/build
*** Using kernel spec --stdknl from earlier build command;
use one of --expk, --stdknl, --otknl to override
Cleaning out /home/adarbari/HOL/sigobj
/home/adarbari/HOL/sigobj cleaned
Building directory tools/set_mtime [22 May, 22:24:34]
Holmake failed with exception: Subscript
Build failed in directory /home/adarbari/HOL/tools/set_mtime (exited with
code 1)
--
*Dr Ashish Darbari, FBCS, FIETE, DPhil (Oxon)Founder & CEO+44 207 096
0465ashish.darb...@axiomise.com <ashish.darb...@axiomise.com>Axiomise Ltd.
Company No: 1101612871-75 Shelton StreetWC2H 9JQ*
*London, UK*
On 22 May 2018 at 21:07, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
> Hi,
>
> I think you should use Poly/ML 5.6 to build Kananaskis 11. (and Poly/ML
> 5.6 or5.7 to build latest HOL on GitHub)
>
> Regards,
>
> Chun
>
> Ashish Darbari wrote:
> > I'm running into this problem on Cent OS 7. No issues reported with
> > Poly ML installation (installation from sources).
> >
> > When running either smart-configure or tweaking by hand the
> > configure.sml file I get Static Errors.
> >
> > Any idea how to fix this?
> >
> >
> > Ashish
> >
> > [adarbari@localhost hol-kananaskis-11]$ poly
> > <tools-poly/smart-configure.sml
> > Poly/ML 5.7.1 Release
> >
> > HOL smart configuration.
> >
> > Determining configuration parameters: holdir OS poly polymllibdir
> > OS: linux
> > poly: /usr/local/bin/poly
> > polyc: /usr/local/bin/polyc
> > polymllibdir: /usr/local/lib
> > holdir: /home/adarbari/hol-kananaskis-11
> > DOT_PATH: /usr/bin/dot
> >
> > Configuration will begin with above values. If they are wrong
> > press Control-C.
> >
> > Will continue in 1 seconds.
> >
> > Loading system specific functions
> > /home/adarbari/hol-kananaskis-11/tools-poly/configure.sml:283: error:
> > Type error in function application.
> > Function: > : Position.int * Position.int -> bool
> > Argument: (OS.FileSys.fileSize uifile, size uifile_content) :
> > Position.int * int
> > Reason:
> > Can't unify Position.int (*In Basis*) with int (*In Basis*)
> > (Different type constructors)
> > Found near
> > Time.> (modTime sigfile, modTime uifile)
> > orelse
> > OS.FileSys.fileSize uifile > size uifile_content
> > Static Errors
> >
> >
> >
> >
> > ------------------------------------------------------------
> ------------------
> > 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
>
>
> ------------------------------------------------------------
> ------------------
> 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
>
------------------------------------------------------------------------------
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
