Short, short version: I will be working on a new Dracula implementation; see <a href="https://github.com/carl-eastlund/dracula">https://github.com/carl-eastlund/dracula</a> (currently just a bare Racket fork).<br><br>====<br>

<br>Short version: While the &quot;new Dracula&quot; is still spiritually &quot;ACL2 via Racket&quot;, the new one will be very different from the old.  It will be much more Rackety, have full use of Racket macros and modules, and have a much improved component system based very closely on ML functors.  It will also be distributed as a regular collection rather than as a planet package.  Along with Dracula development, I will &quot;spin off&quot; some of my support libraries as new collections (or parts of existing ones).<br>

<br>====<br><br>TL;DR:<br><br>The implementation of my thesis is &quot;almost ready for prime-time&quot;.  I want to push it out to the world soon.  I have not found Planet to be an ideal platform for an internal PLT developer trying to keep up with the development branch; I need to update my code far too often, and yet for clients I have to maintain compatibility with the released version.  I could probably resolve that if I wanted to maintain &quot;stable&quot; and &quot;release&quot; branches of my own project; I do not.  Our organization has a whole development and release infrastructure built around our core repository, and it has not been beneficial for me to work outside that for so long.<br>

<br>In the meantime, my private Dracula development has built up a number of support libraries.  Some of them are superfluous and should just basically be &quot;inlined&quot; into the implementation, but some are also near-ready for release in their own right.  The top candidates are my debugging library, which is in the spirit of unstable/debug but significantly improved, and my pretty-printer which has a number of advantages over racket/pretty.  I have found both of these to be immensely useful in debugging programs with little errors buried under huge amounts of data.  I don&#39;t know if the unstable collection will be part of the life cycle for these collections; I&#39;ve yet to pin down the best way to use unstable so it doesn&#39;t just turn into a code graveyard.  Probably these collections are better candidates than some of my previous attempts, in that I am actively developing them for a specific purpose and intend to push them out as stable collections before long.  In previous cases, I was just putting stuff &quot;out there&quot; and &quot;seeing what happens&quot;.<br>

<br>The old Dracula was a Racket model of ACL2: taking ACL2 programs, and simulating them in DrRacket so we could get the world teachpack and syntax checking.  The new Racket is an ACL2 model of Racket, designed to be much more along the lines of taking first- (and possibly second-)order Racket programs and certifying ACL2 models of them.  I don&#39;t know how precise that will be; the new ML-like components don&#39;t look much like anything we have natively in Racket.<br>

<br>Anyway, the repository is up on Github, linked above.  Right now it&#39;s just a copy of plt/racket, but I&#39;ll be gradually pulling pieces of my private Dracula repo (which for various reasons I prefer to refactor into the Racket fork piecemeal rather than copy wholesale).<br clear="all">

<br clear="all">Carl Eastlund<br>
<br>