`Holmake` command is in the “bin/“ directory of your HOL directory (/home/adarbari/hol-kananaskis-11) after the initial build step. You should call it with its full or relative path.
> Il giorno 23 mag 2018, alle ore 10:04, Ashish Darbari
> <ashish.darb...@gmail.com> ha scritto:
>
> Hi Michael
>
> This is what I see when I run Holmake from within the tools/set_mtime
> directory
>
> [adarbari@localhost HOL]$ Holmake --poly_not_hol --no_sigobj --qof
> bash: Holmake: command not found...
>
> I do see Holmakefile executable in that directory.
>
> Ashish
>
>
> --
>
> 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 23:58, <michael.norr...@data61.csiro.au> wrote:
> 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
>
> ------------------------------------------------------------------------------
> 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
signature.asc
Description: Message signed with OpenPGP
------------------------------------------------------------------------------ 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
