<div dir="ltr"><div><div><div>I&#39;m trying to make a &quot;raco make&quot;-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&#39;t know how to get at, in making this process work.<br>

<br></div>(1) I don&#39;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&#39;s source code, but I assume that&#39;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&#39;s source file name the same way as compilation does, except instead of &lt;SOURCE&gt;_rkt.zo I want to create &lt;SOURCE&gt;_rkt.lisp or some such.  Is _this_ functionality available somewhere?<br>

<br></div>I think that&#39;s all I would need to get started.  Any help would be appreciated, thanks.<br><div><div><div><div><br clear="all"><div>Carl Eastlund</div>
</div></div></div></div></div>