[M3devel] MODULEs in .M3IMPTAB

Mika Nystrom mika at async.caltech.edu
Sun Mar 6 05:24:37 CET 2011

Let me be perfectly clear.

m3tk processes interfaces just fine.

m3tk at the moment doesn't know where to find implementations (MODULEs).

One can tell m3tk where to find them with a command-line switch specifying
a list of directories.  But that's not right, because only cm3 (the
compiler driver) knows which source files have been processed to build
which implementation.

I think my argument suggests the .m3s should be emitted to .M3IMPTAB together
with the .i3s (and .igs oh and also .mgs)


"Daniel Alejandro Benavides D." writes:
>Hi all:
>yes, I think I did mention it in a past message because about the ESC, it n=
>eedes as it m3tk too, I didn't know it was a requirement of m3tk though. Bu=
>t because is just a module dependency analyzer I thought we could just crea=
>te one in m3tk, sort of a chicken and egg problem it seems now. OK, I with =
>an older cm3 we could use it to build it in a setting and then supply itsel=
>f in m3tk, if that's the way to go, therefore I think this is really needed=
> for ESC release.
>Another thing if you allow me is about again the ESC itself, I think that o=
>ne of the ways we could improve some of the ESC checks is to reuse some sor=
>t automatic program debugger I already mentioned about Juno which language =
>has a subset of Simplify language so we could try to postprocess further er=
>rors to guarantee they are so and the more important it could be possible t=
>o think in analyzing checks for soundness so we may try to put closer Simpl=
>if0y to its (in results terms) goal of finding more errors it can catch. Th=
>at said I would go for double checked proofs so me can arguably guarantee t=
>hey are sound proved theoretically and passing through it Simplify again, a=
>ll of this without modification to ESC per se. This is traditional approach=
> for debuggers, so its not a new idea again, just that we need to be smarte=
>r in certain way to catch with the less computation effort the most bugs we=
> can. Another thing I was thinking was to integrate this proofs in
> regular builds so for example a given all program proofs modified by the d=
>ebugger should be presented as warnings of error and something that must be=
> checked closely (supervised).
>Ok, let mw now your thoughts on this points, thanks in advance
>--- El s=E1b, 5/3/11, Mika Nystrom <mika at async.caltech.edu> escribi=F3:
>> De: Mika Nystrom <mika at async.caltech.edu>
>> Asunto: Re: [M3devel] MODULEs in .M3IMPTAB
>> Para: "Tony Hosking" <hosking at cs.purdue.edu>
>> CC: m3devel at elegosoft.com
>> Fecha: s=E1bado, 5 de marzo, 2011 17:53
>> Tony, are you sure?  There don't seem to be any tools
>> in CM3 that process
>> implementations with m3tk, or have I been looking in the
>> wrong places?
>> stubgen doesn't, I don't think stablegen does, and m3pp and
>> m3tohtml
>> don't even use m3tk.  Also it doesn't seem to work on
>> PM3-1.13.2.  Hmmmmm....
>>      Mika
>> Tony Hosking writes:
>> >It used to work... :-(
>> >
>> >On Mar 5, 2011, at 3:06 PM, Mika Nystrom wrote:
>> >
>> >> Hi again m3devel,
>> >>=20
>> >> Can anyone think of a reason that cm3 should *not*
>> emit information
>> >> about MODULEs that it compiles to .M3IMPTAB?=20
>> (It doesn't, today,
>> >> which means that m3tk-based tools can't find
>> implementations, only
>> >> interfaces.)
>> >>=20
>> >>    Mika
>> =0A=0A=0A      

More information about the M3devel mailing list