((( [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 [docs] [package home page]
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 2 9)))
Package description:
Provides the Dracula language level for ACL2 emulation.
Downloads this week: 0
Total downloads: 2575
Tickets:7
Open tickets:6
Primary files:
language/dracula.scm
NameContract
(all-from dracula-core.scm)—
(all-from defstructure.scm)—
(all-from deflist.scm)—
(all-from (file "primitive-procedures/acl2-prims.scm"))—
#%module-begin—
#%plain-module-begin—
#%top-interaction—
#%top—
#%app—
 Current version
PLaneT versionExternal versionSourceDLsDocsReq. PLTDate added
(2 9)—
25
[none]2008-05-15
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!)
 Open tickets
[All Tickets] [New Ticket]
Ticket IdOwnerReporterTypeVersion
182ccepnkfelixdefect
example from docs defines MDistributive module twice (and MDistributeLists not at all)
183ccepnkfelixdefect
dracula rename export example from reference docs does not work
184ccepnkfelixdefect
modular acl2 unresolved import problem, useless error message
186ccepnkfelixdefect
Dracula errors on (just) + or - at REPL
181ccepnkfelixdefect
example from docs declares IDistributeLists as a module
185ccepnkfelixdefect
Modular ACL2 reacts poorly to mixing of "code" and exports

 Old versions
PLaneT versionExternal versionSourceDLsDocsReq. PLTDate added
(2 8)—
4
[none]2008-05-15
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]2008-05-15
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]2008-05-14
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
3712008-02-21
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
3712007-11-12
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]2007-11-12
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]2007-11-11
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]2007-10-29
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
371.32007-10-29
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]2007-10-17
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]2007-09-19
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]2007-09-13
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]2007-09-13
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]2007-09-13
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]2007-09-07
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]2007-09-06
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]2007-08-25
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
3702007-08-06
To load: (require (planet "language/dracula.scm" ("cce" "dracula.plt" 1 (= 0))))
Available in repositories: 3xx
1.0: First PLaneT release of Dracula.
 Packages in other repositories

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

PLaneT versionExternal versionSourceDLsDocsReq. PLTDate added
(8 25)—
45
5.922014-02-24
To load: (require (planet "main.rkt" ("cce" "dracula.plt" 8 (= 25))))
Available in repositories: 4.x
8.25: updated modular acl2 file metadata
(8 24)—
2
5.922014-02-24
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
4.2.52012-07-25
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
4.2.52011-11-28
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
4.2.52011-10-25
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
4.2.52011-09-02
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
4.2.52011-04-21
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
4.2.22011-02-04
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
4.2.22011-02-03
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
4.2.22010-11-29
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
4.2.22010-11-02
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
4.2.22010-10-07
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
4.2.22010-10-05
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
4.2.22010-08-18
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
4.2.22010-05-28
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
4.2.22010-03-30
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
4.2.22010-03-22
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
4.2.22010-03-16
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
4.2.22009-12-09
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
4.2.22009-11-17
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
4.0.12009-11-16
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.12009-09-30
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.12009-08-28
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.12009-03-10
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.12009-02-12
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.12009-02-04
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.12009-01-17
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.12009-01-17
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
4.0.12008-10-24
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
4.0.12008-08-28
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
4.0.12008-08-27
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
4.0.12008-08-25
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.12008-09-12
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]2008-06-23
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]2008-06-09
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.