[racket-dev] Racket build dependencies

I'm trying to make a "raco make"-like command for ACL2 certification of
Dracula programs.  Given a Racket program written using the Dracula
language, the command extracts a proof obligation, saves it as a .lisp
file, and runs ACL2 on it.  There are a couple pieces of the Racket build
system that I don't know how to get at, in making this process work.

(1) I don't want to recreate the proof obligation files if they are
up-to-date.  For this I need to get the name of the compiled .zo file for a
module for comparison.  Is this functionality available somewhere?  I might
also need the path of the module's source code, but I assume that's what
resolved-module-path-name gives me.  Right?

(2) I want to respect settings like PLTCOMPILEDROOTS when deciding where to
save the proof obligation file.  Basically I want to mangle the module's
source file name the same way as compilation does, except instead of
<SOURCE>_rkt.zo I want to create <SOURCE>_rkt.lisp or some such.  Is _this_
functionality available somewhere?

I think that's all I would need to get started.  Any help would be
appreciated, thanks.

Carl Eastlund
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/dev/archive/attachments/20130609/9393a082/attachment.html>