On Wed, Oct 16, 2013 at 7:38 PM, Andrea <ag...@leicester.ac.uk> wrote:
> Hi,
>
> @Ramana: thank you very much! The solution you proposed worked pretty well.
> Just now I got the message:
>
> Hol built successfully.
>
Great!
>
> @Vincent: thank you the same. Probably this solved also your problem,
> doesn't it?
>
> By the way, is there also an IRC channel for Hol?
>
Not that I'm aware of. However, I am currently in #hol on freenode, and
attempting to find its current owner (last seen 10 years ago).
So, anyone on list who's interested, feel free to ask questions there.
If we can't get ownership of that channel, ##hol is available.
> Thanks again,
>
> Andrea
>
>
> On 16/10/13 18:54, Ramana Kumar wrote:
>
> Another option would be to use an older version of Poly/ML, e.g. 5.5.
> There was some discussion about this issue on the Poly/ML mailing list,
> around this thread:
> http://lists.inf.ed.ac.uk/pipermail/polyml/2013-September/001344.html
>
>
> On Wed, Oct 16, 2013 at 6:49 PM, Ramana Kumar <ram...@member.fsf.org>wrote:
>
>> Hi Vincent,
>>
>> I strongly advise against this solution. Moscow ML is much slower than
>> Poly/ML, and some features of HOL4 don't work with it (e.g. heaps).
>> However, with a language defined by a standard we would always hope to be
>> implementation-agnostic :)
>>
>> Cheers,
>> Ramana
>>
>>
>> On Wed, Oct 16, 2013 at 6:44 PM, Vincent Aravantinos <
>> vincent.aravanti...@gmail.com> wrote:
>>
>>> Hi Andrea, I had the same problem recently and "solved" it by using
>>> Moscow ML instead of Poly ML.
>>>
>>> V.
>>>
>>> Le 16/10/2013 19:02, Andrea a écrit :
>>> > Hello everyone,
>>> >
>>> > I am a PhD student who is going to work hardly with HOL for the next
>>> > three years.
>>> > Hope you will be patient with me, since I am totally new to it and,
>>> > eventually, I will ask a lot about it!
>>> >
>>> > Here the first question:
>>> > I am trying to install it on my pc, but I am getting this error:
>>> >
>>> > Loading system specific functions
>>> > Compiling system specific functions (sig sml)
>>> > Beginning configuration.
>>> > Making tools/mllex/mllex.exe.
>>> > Poly/ML 5.5.1 Release
>>> > Failed to build mllex.
>>> >
>>> > My environment is linux ubuntu 13.04 64bit and the steps I have
>>> > performed are the following:
>>> >
>>> > 1) installed Poly/ML 5.5.1
>>> > as it appears in the HOL auto-setting of configuration
>>> parameter,
>>> > poly is in /usr/local/bin/poly and
>>> > polymllibdir is in /usr/local/lib
>>> > 2) run the command
>>> > $ poly < tools/smart-configure.sml
>>> >
>>> > but at this point I got the error.
>>> > More in particular a long list of undefined references. Here the final
>>> > bit of it:
>>> >
>>> >
>>> sharedata.cpp:(.text._ZN18ProcessAddToVectorD0Ev[_ZN18ProcessAddToVectorD0Ev]+0x20):
>>> > undefined reference to `operator delete(void*)'
>>> >
>>> /usr/local/lib/libpolyml.a(sharedata.o):(.rodata._ZTI19ProcessFixupAddress[_ZTI19ProcessFixupAddress]+0x0):
>>> > undefined reference to `vtable for __cxxabiv1::__si_class_type_info'
>>> >
>>> /usr/local/lib/libpolyml.a(sharedata.o):(.rodata._ZTI18ProcessAddToVector[_ZTI18ProcessAddToVector]+0x0):
>>> > undefined reference to `vtable for __cxxabiv1::__si_class_type_info'
>>> >
>>> /usr/local/lib/libpolyml.a(sharedata.o):(.rodata._ZTI12ShareRequest[_ZTI12ShareRequest]+0x0):
>>> > undefined reference to `vtable for __cxxabiv1::__si_class_type_info'
>>> > /usr/local/lib/libpolyml.a(sharedata.o):(.eh_frame+0x3f7): undefined
>>> > reference to `__gxx_personality_v0'
>>> > /usr/local/lib/libpolyml.a(elfexport.o): In function
>>> > `ELFExport::exportStore()':
>>> > elfexport.cpp:(.text+0x235): undefined reference to `operator
>>> > new[](unsigned long)'
>>> > elfexport.cpp:(.text+0xdf5): undefined reference to `operator
>>> > delete[](void*)'
>>> >
>>> /usr/local/lib/libpolyml.a(elfexport.o):(.rodata._ZTI9ELFExport[_ZTI9ELFExport]+0x0):
>>> > undefined reference to `vtable for __cxxabiv1::__vmi_class_type_info'
>>> > /usr/local/lib/libpolyml.a(elfexport.o):(.eh_frame+0x6f): undefined
>>> > reference to `__gxx_personality_v0'
>>> > collect2: error: ld returned 1 exit status
>>> > Failed to build mllex.
>>> >
>>> > Hope you can help me, I look forward to try it!
>>> > Have a nice day,
>>> >
>>> > Andrea
>>> >
>>> > P.S: I have made a mess and I have sent the message with my personal
>>> > mail first, Sorry to the moderators :P
>>> >
>>> >
>>> ------------------------------------------------------------------------------
>>> > October Webinars: Code for Performance
>>> > Free Intel webinars can help you accelerate application performance.
>>> > Explore tips for MPI, OpenMP, advanced profiling, and more. Get the
>>> most from
>>> > the latest Intel processors and coprocessors. See abstracts and
>>> register >
>>> >
>>> http://pubads.g.doubleclick.net/gampad/clk?id=60135031&iu=/4140/ostg.clktrk
>>> > _______________________________________________
>>> > hol-info mailing list
>>> > hol-info@lists.sourceforge.net
>>> > https://lists.sourceforge.net/lists/listinfo/hol-info
>>>
>>>
>>> --
>>> Vincent Aravantinos, PhD
>>> Analysis and Design of Dependable Systems
>>> fortiss GmbH <www.fortiss.org/en>
>>> Guerickestrasse 25 | 80805 Munich | Germany
>>>
>>>
>>>
>>> ------------------------------------------------------------------------------
>>> October Webinars: Code for Performance
>>> Free Intel webinars can help you accelerate application performance.
>>> Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most
>>> from
>>> the latest Intel processors and coprocessors. See abstracts and register
>>> >
>>>
>>> http://pubads.g.doubleclick.net/gampad/clk?id=60135031&iu=/4140/ostg.clktrk
>>> _______________________________________________
>>> hol-info mailing list
>>> hol-info@lists.sourceforge.net
>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>>
>>
>>
>
>
>
> ------------------------------------------------------------------------------
> October Webinars: Code for Performance
> Free Intel webinars can help you accelerate application performance.
> Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most
> from
> the latest Intel processors and coprocessors. See abstracts and register >
> http://pubads.g.doubleclick.net/gampad/clk?id=60135031&iu=/4140/ostg.clktrk
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
October Webinars: Code for Performance
Free Intel webinars can help you accelerate application performance.
Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from
the latest Intel processors and coprocessors. See abstracts and register >
http://pubads.g.doubleclick.net/gampad/clk?id=60135031&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
