[Omake] Could metaprl be used to create omake?

[Aleksey Nogin]

On 02.09.2007 11:30, Larry Evans wrote:

> I'm assuming that in that a side effect of the proof is
> a program (i.e. omake) which satisfies the specification.
> Is that assumption correct?  If so, then why wouldn't
> it be good to use metaprl to create omake?

Larry,

Thanks for this insightful question!

Speaking from a specification point of view, OMake has three major parts:
  - Discovering the environment it's in (which source files exist, etc)
  - Computing the build specification (the dependency graph with commands)
  - Executing the build specification

If would have been possible to specify the second part in MetaPRL 
(basically, this would mean providing the complete formal semantics of 
the OMake programming language), however:
  - Executing OMake programs based on the formal specifications would 
have been very slow (while extracting programs from constructive proofs 
is a built-in capability of MetaPRL, writing constructive proofs that 
would yield _efficient_ programs is an open research problem).
  - Without the other two components, we could only execute "pure" OMake 
programs that do not interact with the environment in any way and we 
would have no way to execute the build specification such an OMake 
program would create, so this would not be very practical.

Note that the third component of OMake mostly contains large amounts of 
fairly messy code that is designed to provide a uniform interface under 
Linux and Windows, making it possible to implement a cross-platform 
shell language, complete with background processes, redirects, pipes, 
etc. If would be pretty much impossible to give a formal specification 
for that code (that is, unless somebody creates a formal specification 
of POSIX, Linux, and Windows APIs first)...

In the long run, having a formal specification of the OMake language 
would definitely be nice (and we are hoping to do it some day). However, 
this is something that would not probably be worth spending too much 
time on just yet, as the language is still evolving fairly rapidly.

I do not think anybody would ever care to do a formal specification of 
the whole OMake, though.

Aleksey