[racket-dev] Racket build dependencies

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.

Carl Eastlund


On Mon, Jun 10, 2013 at 12:38 AM, Carl Eastlund <cce at ccs.neu.edu> wrote:

> 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.
>
> Carl Eastlund
>
> On Sun, Jun 9, 2013 at 10:29 AM, Carl Eastlund <cce at ccs.neu.edu> wrote:
>
>> 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/20130614/b42ec742/attachment.html>