[M3devel] elegosoft.com working?

[Daniel Alejandro Benavides D.]

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