((( [logo]Racket )))Need Help?
AboutDownloadDocumentationPLaneTCommunityLearning
PLaneT > cce > dracula.plt
View packages:  [4.x] | 3xx
[contribute a package / log in]
Package dracula.plt contributed by cce  [package home page]
To load: (require (planet cce/dracula:8:25))
Old style:(require (planet "main.rkt" ("cce" "dracula.plt" 8 25)))
Min Racket version: 5.92
Package description:
Provides the Dracula language level for ACL2 emulation.
Downloads this week: 0
Total downloads: 2575
Tickets:0
Open tickets:0
Primary files:
main.rkt
[no interface available]
 Current version
PLaneT versionExternal versionSourceDLsDocsReq. PLTDate added
(8 25)—
45
[none]
5.92Tuesday, February 25th, 2014
To load: (require (planet cce/dracula:8:25))
Available in repositories: 4.x
8.25: updated modular acl2 file metadata
No Tickets Currently open for this Package [New Ticket]

 Old versions
PLaneT versionExternal versionSourceDLsDocsReq. PLTDate added
(8 24)—
2
[none]
5.92Monday, February 24th, 2014
To load: (require (planet "main.rkt" ("cce" "dracula.plt" 8 (= 24))))
Available in repositories: 4.x
8.24: updated to share code with package release
(8 23)—
333
[none]
4.2.5Wednesday, July 25th, 2012
To load: (require (planet "lang/dracula.rkt" ("cce" "dracula.plt" 8 (= 23))))
Available in repositories: 4.x
8.23: Compatibility with Racket 5.3.
(8 22)—
78
[none]
4.2.5Monday, November 28th, 2011
To load: (require (planet "lang/dracula.rkt" ("cce" "dracula.plt" 8 (= 22))))
Available in repositories: 4.x
8.22: Compatibility with Racket 5.2.0.4.
(8 21)—
13
[none]
4.2.5Tuesday, October 25th, 2011
To load: (require (planet "lang/dracula.rkt" ("cce" "dracula.plt" 8 (= 21))))
Available in repositories: 4.x
8.21: Documented link and restrict forms in Modular ACL2. Also updated the location of Dracula documentation on the Help Desk front page.
(8 20)—
66
[none]
4.2.5Friday, September 2nd, 2011
To load: (require (planet "lang/dracula.rkt" ("cce" "dracula.plt" 8 (= 20))))
Available in repositories: 4.x
8.20: Improved Dracula error message when property preconditions fail.
(8 19)—
76
[none]
4.2.5Thursday, April 21st, 2011
To load: (require (planet "lang/dracula.rkt" ("cce" "dracula.plt" 8 (= 19))))
Available in repositories: 4.x
8.19: Updated for compatibility with Racket v5.1.1.
(8 18)—
88
[none]
4.2.2Friday, February 4th, 2011
To load: (require (planet "lang/dracula.rkt" ("cce" "dracula.plt" 8 (= 18))))
Available in repositories: 4.x
8.18: Updated for compatibility with Racket v5.1.
(8 17)—
2
[none]
4.2.2Thursday, February 3rd, 2011
To load: (require (planet "lang/dracula.rkt" ("cce" "dracula.plt" 8 (= 17))))
Available in repositories: 4.x
8.17:
  • Added import/export restriction for Modular ACL2 compound modules.
  • Made state variable available in world teachpack.
  • Fixed ordering of import, include-book, and export verification in Modular ACL2.
(8 16)—
191
[none]
4.2.2Tuesday, November 30th, 2010
To load: (require (planet "lang/dracula.ss" ("cce" "dracula.plt" 8 (= 16))))
Available in repositories: 4.x
8.16: Bug fix for anomalous Dracula/ACL2 interaction.
(8 15)—
48
[none]
4.2.2Wednesday, November 3rd, 2010
To load: (require (planet "lang/dracula.ss" ("cce" "dracula.plt" 8 (= 15))))
Available in repositories: 4.x
8.15: Performance improvements to Dracula GUI for long proofs.
(8 14)—
44
[none]
4.2.2Thursday, October 7th, 2010
To load: (require (planet "lang/dracula.ss" ("cce" "dracula.plt" 8 (= 14))))
Available in repositories: 4.x
8.14: Performance improvements to Dracula language levels.
(8 13)—
14
[none]
4.2.2Tuesday, October 5th, 2010
To load: (require (planet "lang/dracula.ss" ("cce" "dracula.plt" 8 (= 13))))
Available in repositories: 4.x
8.13: Redundant include-book now allowed.
(8 12)—
85
[none]
4.2.2Wednesday, August 18th, 2010
To load: (require (planet "lang/dracula.ss" ("cce" "dracula.plt" 8 (= 12))))
Available in repositories: 4.x
8.12: Made Dracula proof window smaller by default.
(8 11)—
33
[none]
4.2.2Friday, May 28th, 2010
To load: (require (planet "lang/dracula.ss" ("cce" "dracula.plt" 8 (= 11))))
Available in repositories: 4.x
8.11: Updated for compatibility with upcoming Racket release.
(8 10)—
42
[none]
4.2.2Wednesday, March 31st, 2010
To load: (require (planet "lang/dracula.ss" ("cce" "dracula.plt" 8 (= 10))))
Available in repositories: 4.x
8.10: Added intern, intern$, and intern-in-package-of-symbol.
(8 9)—
17
[none]
4.2.2Monday, March 22nd, 2010
To load: (require (planet "lang/dracula.ss" ("cce" "dracula.plt" 8 (= 9))))
Available in repositories: 4.x
8.9: Fixed various bug reports.
(8 8)—
15
[none]
4.2.2Tuesday, March 16th, 2010
To load: (require (planet "lang/dracula.ss" ("cce" "dracula.plt" 8 (= 8))))
Available in repositories: 4.x
8.8: Sped up compilation; improved backwards compatibility.
(8 7)—
61
[none]
4.2.2Wednesday, December 9th, 2009
To load: (require (planet "lang/dracula.ss" ("cce" "dracula.plt" 8 (= 7))))
Available in repositories: 4.x
8.7: Made GUI respond more gracefully to errors.
(8 6)—
47
[none]
4.2.2Tuesday, November 17th, 2009
To load: (require (planet "lang/dracula.ss" ("cce" "dracula.plt" 8 (= 6))))
Available in repositories: 4.x
8.6: Removed the need for check-properties in the doublecheck teachpack and generate-report in the testing teachpack.
(8 5)—
13
[none]
4.0.1Monday, November 16th, 2009
To load: (require (planet "lang/dracula.ss" ("cce" "dracula.plt" 8 (= 5))))
Available in repositories: 4.x
8.5: Fixed a bug with the scope of definitions, especially with teachpacks in Modular ACL2.
(8 4)—
30
[none]
4.0.1Wednesday, September 30th, 2009
To load: (require (planet "lang/dracula.ss" ("cce" "dracula.plt" 8 (= 4))))
Available in repositories: 4.x
8.4:Updated for compatibility with PLT Scheme 4.2.2.Also extended backwards compatibility to PLT Scheme 4.2.
(8 3)—
67
[none]
4.0.1Friday, August 28th, 2009
To load: (require (planet "lang/dracula.ss" ("cce" "dracula.plt" 8 (= 3))))
Available in repositories: 4.x
8.3: fixed a problem in the io-utilities teachpack with string-list->file.
(8 2)—
128
[none]
4.0.1Tuesday, March 10th, 2009
To load: (require (planet "lang/dracula.ss" ("cce" "dracula.plt" 8 (= 2))))
Available in repositories: 4.x
8.2: Removed a memory leak in ACL2 GUI; fixed broken links in online documentation.
(8 1)—
35
[none]
4.0.1Thursday, February 12th, 2009
To load: (require (planet "lang/dracula.ss" ("cce" "dracula.plt" 8 (= 1))))
Available in repositories: 4.x
8.1: Support for include-book inside modules, plus internal changes.
(8 0)—
44
[none]
4.0.1Wednesday, February 4th, 2009
To load: (require (planet "lang/dracula.ss" ("cce" "dracula.plt" 8 (= 0))))
Available in repositories: 4.x
8.0: Removed Dracula version number from metadata in Modular ACL2 files.
(7 1)—
89
[none]
4.0.1Saturday, January 17th, 2009
To load: (require (planet "lang/dracula.ss" ("cce" "dracula.plt" 7 (= 1))))
Available in repositories: 4.x
7.1: Updated version number in installation instructions.
(7 0)—
3
[none]
4.0.1Saturday, January 17th, 2009
To load: (require (planet "lang/dracula.ss" ("cce" "dracula.plt" 7 (= 0))))
Available in repositories: 4.x
7.0: Rewrote the Dracula GUI and Modular ACL2 language entirely.
(6 0)—
99
[none]
4.0.1Friday, October 24th, 2008
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 6 (= 0))))
Available in repositories: 4.x
6.0: Fixed typos preventing certification of some teachpacks.
(4 2)—
110
[none]
4.0.1Friday, August 29th, 2008
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 4 (= 2))))
Available in repositories: 4.x
4.2: Fixed a bug: files read by include-book now properly case insensitive.
(4 1)—
19
[none]
4.0.1Thursday, August 28th, 2008
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 4 (= 1))))
Available in repositories: 4.x
4.1: Changed DoubleCheck again. See documentation for new syntax.
(4 0)—
28
[none]
4.0.1Monday, August 25th, 2008
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 4 (= 0))))
Available in repositories: 4.x
4.0: Added Scribble documentation. Updated DoubleCheck.
(3 2)—
18
[none]
4.0.1Friday, September 12th, 2008
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 3 (= 2))))
Available in repositories: 4.x
3.2: Updated legacy Dracula version, fixed incompatibility with cce/scheme.plt.
(3 1)—
58
[none]
[none]Monday, June 23rd, 2008
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 3 (= 1))))
Available in repositories: 4.x
3.1: Ported Dracula to PLT v4.0.1. Still needs Scribble documentation.
(3 0)—
20
[none]
[none]Monday, June 9th, 2008
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 3 (= 0))))
Available in repositories: 4.x
3.0: Ported Dracula to PLT v4. Still needs Scribble documentation.
 Packages in other repositories

These packages are not available in the 4.x repository, but they are available for other versions of Racket.

PLaneT versionExternal versionSourceDLsDocsReq. PLTDate added
(2 9)—
25
[none]
[none]Thursday, May 15th, 2008
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 2 (= 9))))
Available in repositories: 3xx
2.9: Took hard-coded ACL2 path out of Modular ACL2 (big oops!)
(2 8)—
4
[none]
[none]Thursday, May 15th, 2008
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 2 (= 8))))
Available in repositories: 3xx
2.8: Updated version number (oops) and minimum FastTest version
(2 7)—
6
[none]
[none]Thursday, May 15th, 2008
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 2 (= 7))))
Available in repositories: 3xx
2.7: defproperty now generates test expressions to duplicate failures
(2 6)—
4
[none]
[none]Wednesday, May 14th, 2008
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 2 (= 6))))
Available in repositories: 3xx
2.6:
  • Updated and documented rand teachpack.
  • Expanded world teachpack to more of HTDP functions.
  • Added experimental demo of Modular ACL2 (work in progress)
(2 5)—
133
[none]
371Thursday, February 21st, 2008
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 2 (= 5))))
Available in repositories: 3xx
2.5:
  • Fixed audio teachpack so it will certify.
  • Fixed DoubleCheck tests and enabled GUI interface.
  • Restored self-quoting keywords (e.g. :NAME).
  • Updated prover interaction to detect prompt for ACL2(r).
(2 4)—
108
[none]
371Monday, November 12th, 2007
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 2 (= 4))))
Available in repositories: 3xx
  • 2.4: Correction to DoubleCheck documentation.
  • 2.3: Accidental duplicate of 2.2.
  • 2.2:
    • Added doublecheck teachpack.
    • Added remove-eq and remove-equal.
    • Added documentation for teachpacks.
    • Exported horner and map-chrs->str from io-utilities teachpack.
    • Exported drop-thru from list-utilities teachpack.
    • Updated Undo to work better with teachpacks.
    • Added error dialog for Create Executable.
(2 3)—
5
[none]
[none]Monday, November 12th, 2007
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 2 (= 3))))
Available in repositories: 3xx
2.2:
  • Added doublecheck teachpack.
  • Added remove-eq and remove-equal.
  • Added documentation for teachpacks.
  • Exported horner and map-chrs->str from io-utilities teachpack.
  • Exported drop-thru from list-utilities teachpack.
  • Updated Undo to work better with teachpacks.
  • Added error dialog for Create Executable.
(2 2)—
9
[none]
[none]Sunday, November 11th, 2007
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 2 (= 2))))
Available in repositories: 3xx
2.2:
  • Added doublecheck teachpack.
  • Added remove-eq and remove-equal.
  • Added documentation for teachpacks.
  • Exported horner and map-chrs->str from io-utilities teachpack.
  • Exported drop-thru from list-utilities teachpack.
  • Updated Undo to work better with teachpacks.
  • Added error dialog for Create Executable.
(2 1)—
17
[none]
[none]Monday, October 29th, 2007
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 2 (= 1))))
Available in repositories: 3xx
  • 2.1: Compatibility fix with released DrScheme versions. Still possibly unstable.
  • 2.0: Performance improvements. Possibly unstable, revert to 1.8 if buggy.
(2 0)—
0
[none]
371.3Monday, October 29th, 2007
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 2 (= 0))))
Available in repositories: 3xx
2.0: Performance improvements. Possibly unstable, revert to 1.8 if buggy.
(1 8)—
55
[none]
[none]Wednesday, October 17th, 2007
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 1 (= 8))))
Available in repositories: 3xx
  • 1.8: Internal infrastructure changes, more language level GUI fixes.
  • 1.7: Updated doc.txt and added image-height to world teachpack.
  • 1.6: Fixed string-list->file function from io-utilities teachpack.
  • 1.5: Exported loc function from io-utilities teachpack.
  • 1.4: Improvements to book certification (feedback, Windows compatibility).
  • 1.3: Added remove1, remove1-eq, and remove1-equal.
  • 1.2: Fixed bug preventing DrScheme GUI updates when switching languages.
  • 1.1: Improved support for Lisp distributions (SBCL, CLisp).
  • 1.0: First PLaneT release of Dracula.
(1 7)—
53
[none]
[none]Wednesday, September 19th, 2007
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 1 (= 7))))
Available in repositories: 3xx
  • 1.7: Updated doc.txt and added image-height to world teachpack.
  • 1.6: Fixed string-list->file function from io-utilities teachpack.
  • 1.5: Exported loc function from io-utilities teachpack.
  • 1.4: Improvements to book certification (feedback, Windows compatibility).
  • 1.3: Added remove1, remove1-eq, and remove1-equal.
  • 1.2: Fixed bug preventing DrScheme GUI updates when switching languages.
  • 1.1: Improved support for Lisp distributions (SBCL, CLisp).
  • 1.0: First PLaneT release of Dracula.
(1 6)—
8
[none]
[none]Thursday, September 13th, 2007
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 1 (= 6))))
Available in repositories: 3xx
  • 1.6: Fixed string-list->file function from io-utilities teachpack.
  • 1.5: Exported loc function from io-utilities teachpack.
  • 1.4: Improvements to book certification (feedback, Windows compatibility).
  • 1.3: Added remove1, remove1-eq, and remove1-equal.
  • 1.2: Fixed bug preventing DrScheme GUI updates when switching languages.
  • 1.1: Improved support for Lisp distributions (SBCL, CLisp).
  • 1.0: First PLaneT release of Dracula.
(1 5)—
2
[none]
[none]Thursday, September 13th, 2007
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 1 (= 5))))
Available in repositories: 3xx
  • 1.5: Exported loc function from io-utilities teachpack.
  • 1.4: Improvements to book certification (feedback, Windows compatibility).
  • 1.3: Added remove1, remove1-eq, and remove1-equal.
  • 1.2: Fixed bug preventing DrScheme GUI updates when switching languages.
  • 1.1: Improved support for Lisp distributions (SBCL, CLisp).
  • 1.0: First PLaneT release of Dracula.
(1 4)—
2
[none]
[none]Thursday, September 13th, 2007
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 1 (= 4))))
Available in repositories: 3xx
  • 1.4: Improvements to book certification (feedback, Windows compatibility).
  • 1.3: Added remove1, remove1-eq, and remove1-equal.
  • 1.2: Fixed bug preventing DrScheme GUI updates when switching languages.
  • 1.1: Improved support for Lisp distributions (SBCL, CLisp).
  • 1.0: First PLaneT release of Dracula.
(1 3)—
10
[none]
[none]Friday, September 7th, 2007
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 1 (= 3))))
Available in repositories: 3xx
  • 1.3: Added remove1, remove1-eq, and remove1-equal.
  • 1.2: Fixed bug preventing DrScheme GUI updates when switching languages.
  • 1.1: Improved support for Lisp distributions (SBCL, CLisp).
  • 1.0: First PLaneT release of Dracula.
(1 2)—
2
[none]
[none]Thursday, September 6th, 2007
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 1 (= 2))))
Available in repositories: 3xx
  • 1.2: Fixed bug preventing DrScheme GUI updates when switching languages.
  • 1.1: Improved support for Lisp distributions (SBCL, CLisp).
  • 1.0: First PLaneT release of Dracula.
(1 1)—
44
[none]
[none]Saturday, August 25th, 2007
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 1 (= 1))))
Available in repositories: 3xx
1.0: First PLaneT release of Dracula.
1.1: Improved support for Lisp distributions (SBCL, CLisp).
(1 0)—
27
[none]
370Monday, August 6th, 2007
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 1 (= 0))))
Available in repositories: 3xx
1.0: First PLaneT release of Dracula.