<div dir="ltr">I've pushed the changes; syntax/modcode now exports get-module-path, which returns the path of the most up-to-date file for a module, along with a symbol indicating whether that is a source file, bytecode file, or native library. It also exports get-metadata-path, which constructs derived path names based on PLTCOMPILEDROOTS and similar settings. Thanks to Matthew for reviewing the diff.<br> <div class="gmail_extra"><br clear="all"><div>Carl Eastlund</div> <br><br><div class="gmail_quote">On Mon, Jun 10, 2013 at 12:38 AM, Carl Eastlund <span dir="ltr"><<a href="mailto:cce@ccs.neu.edu" target="_blank">cce@ccs.neu.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> <div dir="ltr">It looks like get-module-code from syntax/modcode does what I want internally. I've submitted a pull request on github in which I've split out the two extra functions I need using the functionality that exists. I "modernized" the Racket style in that file before making the changes -- turning let into define and so forth. That makes this a fairly big change, line-by-line; sorry about that, I know it makes reading the diff tougher, but it made it easier to figure out what I was working with in the file.<span class="HOEnZb"><font color="#888888"><br> </font></span><div><div class="gmail_extra"><span class="HOEnZb"><font color="#888888"><br clear="all"><div>Carl Eastlund</div></font></span><div><div class="h5"> <br><div class="gmail_quote">On Sun, Jun 9, 2013 at 10:29 AM, Carl Eastlund <span dir="ltr"><<a href="mailto:cce@ccs.neu.edu" target="_blank">cce@ccs.neu.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> <div dir="ltr"><div><div><div>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.<br> <br></div>(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?<br> <br></div>(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?<br> <br></div>I think that's all I would need to get started. Any help would be appreciated, thanks.<span><font color="#888888"><br><div><div><div><div><br clear="all"><div>Carl Eastlund</div> </div></div></div></div></font></span></div> </blockquote></div><br></div></div></div></div></div> </blockquote></div><br></div></div>