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