Subscript is the standard exception raised if you attempt to do things like
List.nth([1,2,3], 3)
or
String.sub("foo bar", 9)
I guess that Holmake is trying to do one of the above sorts of things.
What happens if you move the Holmakefile in tools/set_mtime out of the way and
call
Holmake --poly_not_hol --no_sigobj --qof
in that directory?
Michael
On 23/5/18, 07:53, "Chun Tian" <binghe.l...@gmail.com> wrote:
I’m not 100% sure, but the keyword “Subscript” seems related to X11
bindings. I guess you must have enabled X11 when building Poly/ML. If so, you
can try to rebuild Poly/ML without X11 and try to build latest HOL again. Hope
this helps,
—Chun
> Il giorno 22 mag 2018, alle ore 22:51, Ashish Darbari
<ashish.darb...@gmail.com> ha scritto:
>
> 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 0465
> ashish.darb...@axiomise.com
> Axiomise Ltd. Company No: 11016128
> 71-75 Shelton Street
> WC2H 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
