[M3devel] About CM3_IDE_UsersGuide format if so

Wed Mar 30 02:21:44 CEST 2011

Hi all:
thanks for your message, and it's Ok, indeed I'm very sorry about that; now the idea behind is that we can invoke "m3build" process (aka cm3) to ESC via esc() quake directive and so subsequently it will call Simplify theorem prover as many times as needed.
As Simplify is able to display its output via ESC command line input parameter and then call the output of it and postprocessed it in ESC to show a source code line number error, e.g array index out of bounds line number xyz, nil deref attempt, unchecked exception, deadlock, etc, so we can get a line number from it and then pass it trough cm3ide to its web output (if Verification Condition VC is correctly generated in ESC that is, Simplify's input and if implied results are positive for source code "errors" at least by its conservatism or formal proof, as also it might be silent in absence of errors either by possible insufficient or too much rigorousness in VCs or if not pass it back to ESC if so to get an error message because of theorem proof is not true or if it doesn't find it, again conservatively speaking), we surely may get this passed through from ESC back to cm3ide to show a similar message hyperlink and "error" line number.
Now in behalf of us we don't have any time to waste we could continue our duties and get a editor call or a twit a message with line and error and enter or twit back the intended solution if so in that line whenever that happens.
As the the Simplify output has html output support for VC falsity, etc, and ESC I still wonder how it will communicate its results, we could adjust that for us in the cm3ide to make that display for us too and show its line number and warning message. Perhaps another cm3ide object method might do that as well, as this "errors" are not fatal, still, it can be shown as warnings (as they really are), then does CM3IDE warning messages come too in same way cm3 errors are shown? If so perhaps this is the way to go. We could select whether to stop compilation process if so if there are selected warnings to do so or if it's asked to continue to do so and don't halt until another instruction is given or it finishes its process. 
As ESC is concerned it would take same time parsing and compiling as cm3 but then another equivalent or more time to check it in VCs theorem proving   meanwhile it might be useful to have that view or display, if for instance it is not happy or unable to prove a given formula to display its VC, in case of false alarm say, or if they are successful steps as they are PROCEDURE by PROCEDURE as ESC goes along each MODULE, so in the end it would take slower time to compile and then recompile it if so as any given module might have a failed proof in a procedure before it checks everything of it. 
Main issue here is that parse trees are different so we can't share their time to type check (assuming we both want to compile and statically check), at least as Verification condition generation is concerned, besides dependency order is determined by cm3 driver and I don't know how it might be get it by m3tk independently if so, so it will for now wait for its type checking and then redo type inference and so and continue to proof so best case scenario both systems will have that to do same type checking and inference to produce a parse tree that will give us a proof that must be verified and if it doesn't satisfy its condition return as an ESC "error" or warning, or finish without complaints if it really does.   
Thanks in advance

--- El mar, 29/3/11, Coleburn, Randy <rcolebur at SCIRES.COM> escribió:

> De: Coleburn, Randy <rcolebur at SCIRES.COM>
> Asunto: RE: [M3devel] About CM3_IDE_UsersGuide format if so
> Para: "Daniel Alejandro Benavides D." <dabenavidesd at yahoo.es>, "m3devel at elegosoft.com" <m3devel at elegosoft.com>
> Fecha: martes, 29 de marzo, 2011 16:26
> Daniel:
> 
> I'm sorry, but I'm not sure I follow your entire train of
> thought.
> 
> If you use CM3IDE to invoke the CM3 builder, any errors
> during the compilation/build process will be displayed in
> the browser with a hyperlink to invoke your editor and jump
> to the line identified as the source of the problem.
> 
> The CM3IDE configuration page allows you to specify the
> editor to be invoked, among other options.
> 
> Regards,
> Randy Coleburn
> 
> -----Original Message-----
> From: Daniel Alejandro Benavides D. [mailto:dabenavidesd at yahoo.es]
> 
> Sent: Tuesday, March 29, 2011 4:37 PM
> To: m3devel at elegosoft.com;
> Coleburn, Randy
> Subject: RE: [M3devel] About CM3_IDE_UsersGuide format if
> so
> 
> Hi all:
> yes, thanks for the info, would be nice to see some level
> of integration between the ESC and Modula-3 in cm3ide as I
> said it shall be pretty easy to deploy network management
> display of test sessions with the cm3ide tool with Simplify
> too, so is nice to have documentation on it about that. I
> guess it would be possible to handle that too in any format,
> if hosts are kind enough for that, as our hosts allows us to
> do so, if I am right. Also a good and nice option is for
> Mobile sessions, to keep an eye on each task, for instance I
> know you can use some editor for showing error messages, I
> guess one would be able to reproduce that behavior with ESC
> errors right, i.e cm3 errors displays line an hyperlinks a
> editor on line. Thus for instance you can get a report on
> error messages from the web server and so display a line in
> the code directly to modify it and run again, I believe.
> This is something really useful if we have such an
> automation of tasks one could think in programming or
> getting the marked line via twits for instance :) if such
> agreement is allowed too.
> Thanks in advance
> 
> 
> --- El mar, 29/3/11, Coleburn, Randy <rcolebur at SCIRES.COM>
> escribió:
> 
> > De: Coleburn, Randy <rcolebur at SCIRES.COM>
> > Asunto: RE: [M3devel] About CM3_IDE_UsersGuide format
> if so
> > Para: "Daniel Alejandro Benavides D." <dabenavidesd at yahoo.es>,
> "m3devel at elegosoft.com"
> <m3devel at elegosoft.com>
> > Fecha: martes, 29 de marzo, 2011 14:40
> > Daniel:
> > 
> > I am ok with you or anyone else providing the user
> guide in
> > additional formats.
> > I simply provided it in the formats readily available
> to me
> > at the time.
> > 
> > Regards,
> > Randy Coleburn
> > 
> > -----Original Message-----
> > From: Daniel Alejandro Benavides D. [mailto:dabenavidesd at yahoo.es]
> > 
> > Sent: Monday, March 28, 2011 7:57 PM
> > To: m3devel at elegosoft.com
> > Subject: [M3devel] About CM3_IDE_UsersGuide format if
> so
> > 
> > Hi all:
> > I wanted to know whether you agree on reformat the
> > CM3_IDE_UserGuide doc file into a standard linear one,
> like
> > of the doc tools used in cm3 and pm3 repository are
> based on
> > either tex, html (and back and forth see belo ) or
> even
> > gnuinfo files, although there some small ones of mtex
> that I
> > don't know much about and also the noweb files
> (literate
> > programming like native burs backend is coded or ldb,
> where
> > still is to be seeing whether generic files are post
> > processed as expected by cm3) that are also plain
> text
> > files.
> > I was thinking in make some docs more widely
> available
> > specifically some improvement over Net Object
> collector
> > information, since there are two formal proofs of that
> I
> > believe one is current there (Birrell's collection
> scheme)
> > and "new" one distributed cyclic garbage collection.
> > This would allows us to alter proof them by formal
> and
> > automatic mechanical checking and such gain some more
> > interest in the platform and its collection
> algorithms:
> > http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-RR-116.pdf

> 
> > 
> > And subsequent work:
> > http://kar.kent.ac.uk/21327/

> 
> > 
> > http://www.cs.kent.ac.uk/pubs/1998/926/index.html

> 
> > 
> > and last but not least:
> > http://www.cs.kent.ac.uk/pubs/2003/1650/

> 
> > 
> > With mechanism such as of the pm3 sgml-obliq it could
> be
> > shown to convert from ps (with see
> > doi:10.1109/ICDAR.1997.619868 [1]) to html to tex and
> so on
> > keep improving the situation with respect of lack of
> > annotation information with the current papers, as of
> > anybody who wants to write informally knowledge about
> it let
> > him do it freely.
> > 
> > Well, just in case you don't mind I will try to add
> extra
> > converted this docs to lyx, from where it could be
> later
> > compiled to tex or displayed directly in any other
> format if
> > so.
> > 
> > Thanks in advance
> > 
> > [1] B. Poirier and M. Dagenais, “An interactive
> system to
> > extract structured text from a geometrical
> > representation,” in Document Analysis and
> Recognition,
> > 1997., Proceedings of the Fourth International
> Conference
> > on, 1997, vol. 1, pp. 342-346 vol.1.
> > 
> 