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
