[M3devel] elegosoft.com working?

Thu Jan 6 12:56:16 CET 2011

Let's worry about ESC integration when we get access to it.
Anyway, I wouldn't run such checks in every build, but perform it
on a certain machine e.g. once a day.

Olaf

Quoting "Daniel Alejandro Benavides D." <dabenavidesd at yahoo.es>:

> Hi all:
> I recall now that the current rend is run this theorem provers   
> distributedly, rather than standalone, so we might given that we   
> have already this in our hands the Simplify theorem prover, for a   
> network instance, not sure if the I/O will be affected in that case,  
>  perhaps the most important thing is to verify full integrity of   
> transfers. See about that issue:
> http://nexus.realtimepublishers.com/ttgmft.php
> (is a work in progress so if interested keep and eye on it, you can   
> register if you want)
> Given that simplify is not written object oriented, perhaps that   
> must be thought to be like that. The thing is given it takes more   
> than double times the time of the compile build process we might   
> (the Greg nelson comment at 53:00 on the linked video) is it is a   
> kind of slow process or of high length but ok to be run on nights.   
> Perhaps given that the compiler building could take 2x a compiler   
> build and the theorem proving 5x times that, which is we can run it   
> each 5 runs in terms of the of two builds, i.e m3tk included. The   
> thing is, if the source has not changed that is would be the case in  
>  some runs it could be in terms of less runs, so we can check in at   
> least each 5 building tasks runs (of all platforms, i.e 5 parallel   
> building tasks), I guess this tasks are programmed in some way, I   
> don't recall where are the policies of this written, if someone can   
> tell that for me or point me that, thanks in advance
>
>
> --- El mié, 5/1/11, Daniel Alejandro Benavides D.   
> <dabenavidesd at yahoo.es> escribió:
>
>> De: Daniel Alejandro Benavides D. <dabenavidesd at yahoo.es>
>> Asunto: Re: [M3devel] elegosoft.com working?
>> Para: "Olaf Wagner" <wagner at elegosoft.com>
>> CC: m3devel at elegosoft.com
>> Fecha: miércoles, 5 de enero, 2011 11:28
>> Hi all:
>> yes, I think we should get access to building with cm3 at
>> least, not sure if the sources according to the latest news
>> on that.
>> In the other hand whether we get this I hope sooner or
>> later, I think it would be a m3quake directive like "esc()"
>> to activate it from inside the building task process, so it
>> can be integrated on the same building machine or another
>> will need to have access to the same CM3 build and source
>> repository and check it on the way, the only thing here, is
>> that ESC need to build M3 sources with m3tk and if so, it
>> will that aprox. by the same time cm3 compiler building
>> software ends that ESC will feed itself with cm3 M3Build
>> .M3IMPTAB import table not generated file now times for
>> external compilers. I'm not sure anyway if that's the order
>> of ESC input anyway, or will need first the .M3IMPPTAB back
>> again perhaps will need to upgrade down or make a better
>> independent procedure to expose this for it, see Revision
>> 1.24:
>> http://dcvs.elegosoft.com/cgi-bin/cvsweb.cgi/cm3/m3-sys/cm3/src/M3Build.m3?annotate=1.24
>> if that's the case we would need to wait anyway for cm3
>> builds or call it from the IMPORTS to get it. Please if one
>> can check that if it's need it and I will likely to see that
>> too. I also think this would be a nice way of making a
>> dependence analyzer (if so perhaps I think is better doing
>> it with m3tk, what do you think? Besides its worth for Obliq
>> and others too like cm3ide, etc)  program for our and
>> other clients too information IMHO.
>> Thanks in advance
>>
>> P.D: according to Dr Greg Nelson the compiler is usually
>> 10x times faster than the ESC process (not sure for the
>> ESC/Java or the ESC/Moddula3), but this is mostly because of
>> the Simplify theorem prover checking see:
>> http://www.uwtv.org/programs/displayevent.aspx?rID=2761
>> Also for simplify see:
>> http://portal.acm.org/citation.cfm?id=1066100.1066102&preflayout=flat
>> whican can be downlaoded report from here:
>> http://www.hpl.hp.com/techreports/2003/HPL-2003-148.html
>> and benchmarks from here:
>> http://goedel.cs.uiowa.edu/smtlib/benchmarks/pending/simplify_benchmarks.tar.gz
>>
>>
>> --- El mié, 5/1/11, Olaf Wagner <wagner at elegosoft.com>
>> escribió:
>>
>> > De: Olaf Wagner <wagner at elegosoft.com>
>> > Asunto: Re: [M3devel] elegosoft.com working?
>> > Para: "Daniel Alejandro Benavides D." <dabenavidesd at yahoo.es>
>> > CC: m3devel at elegosoft.com
>> > Fecha: miércoles, 5 de enero, 2011 04:04
>> > Quoting "Daniel Alejandro Benavides
>> > D." <dabenavidesd at yahoo.es>:
>> >
>> > > Hi all:
>> > > thanks for the info, some time after it went on
>> again
>> > working, but  still if there is some escalation
>> issue
>> > because of the compiler  checks specially with
>> the
>> > computation time, like ESC and so, perhaps  like
>> in
>> > night builds, what would be the machine needs for that
>>
>> > process and the results to allow?
>> > > Based on some experience like in compilers we
>> would
>> > have access to  the checks in more or less time
>> if so I
>> > guess we would need  optimization anyway at
>> source
>> > level and execution level. Meanwhile  more checks
>> will
>> > likely to be introduced, so it would a balance
>> of  both
>> > needs.
>> > > Thanks in advance
>> >
>> > I'm not sure if I understand correctly what you're
>> aiming
>> > at, but
>> > I guess you worry that we need to introduce more
>> > checks/tests like
>> > ESC. Apart from my estimation that we won't get access
>> to
>> > the ESC M3
>> > sources, CPU time would not be a bottleneck, as (a)
>> the
>> > bottleneck on
>> > birch is the I/O system and (b) we could easily
>> delegate
>> > such a task
>> > to another server via Hudson. Anyway, once the web
>> service
>> > has been
>> > moved to another machine there shouldn't be any more
>> > problems with
>> > our use of birch.
>> >
>> > Olaf
>> > --Olaf Wagner -- elego Software Solutions GmbH
>> >
>> >    Gustav-Meyer-Allee 25 / Gebäude 12,
>> 13355
>> > Berlin, Germany
>> > phone: +49 30 23 45 86 96  mobile: +49 177 2345
>> > 869  fax: +49 30 23 45 86 95
>> >    http://www.elegosoft.com |
>> > Geschäftsführer: Olaf Wagner | Sitz: Berlin
>> > Handelregister: Amtsgericht Charlottenburg HRB 77719
>> |
>> > USt-IdNr: DE163214194
>> >
>> >
>>
>>
>>
>>
>
>
>
>

-- 
Olaf Wagner -- elego Software Solutions GmbH
                Gustav-Meyer-Allee 25 / Gebäude 12, 13355 Berlin, Germany
phone: +49 30 23 45 86 96  mobile: +49 177 2345 869  fax: +49 30 23 45 86 95
    http://www.elegosoft.com | Geschäftsführer: Olaf Wagner | Sitz: Berlin
Handelregister: Amtsgericht Charlottenburg HRB 77719 | USt-IdNr: DE163214194