Hi Chun
Yes I know that and I did call it but for some reason this doesn't work.
Will tell you what did work like a charm is what you originally suggested -
use Poly ML 5.6 and Kananaskis 11.
Couldn't get either the Git clone or the Kananaskis one to work with Poly
ML 5.7.
Ashish
--
*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 23 May 2018 at 11:44, Chun Tian <binghe.l...@gmail.com> wrote:
> `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
>
>
> ------------------------------------------------------------
> ------------------
> 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
