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 <c...@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 >
_________________________ Racket Developers list: http://lists.racket-lang.org/dev
