[M3devel] elegosoft.com working?

Thu Jan 6 14:28:18 CET 2011

Hi all:
yes, but maybe when if we got around an optimizing compiler we would need the verification condition generator to use the theorem prover, so the same deal again, and if so we would need also build machines dedicated also to that, I mean what is the point of having them to keeping idle while something in contrast would highly optimized it instead. I bet even the compiler is also to have optimization by it self, I guess everything would need to and so the optimization framework would need to run the theorem prover to work in each build. Even the Simplify, so we must keep and eye on it too meanwhile.

Thanks in advance  

--- El jue, 6/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: jueves, 6 de enero, 2011 06:56
> 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
> 
> 