Windows ACL2 interrupt/shutdown, defrandom, minor fixes

calebegg / proof-pad-classic

An IDE for ACL2

http://proofpad.org

GNU General Public License v3.0

21 stars 4 forks source link

Windows ACL2 interrupt/shutdown, defrandom, minor fixes #11

Closed PeterReid closed 12 years ago

PeterReid commented 12 years ago

I haven't sent a pull request in a while, so this is kind of an assortment of things.

The ACL2 process on Windows can be interrupted
There are implementations for all the doublecheck random primitives (excluding the higher-order ones random-list-of and random-sexp-of). This uses the passing-in-random-seed method of getting randomness.
An invalid book path won't cause a crash
Functions named def* will indent like defuns (this was giving me problems with defrandoms)
The book viewer scrolls when the books don't fit in the window

PeterReid commented 12 years ago

I added a nice way to hide local function/theorem definitions and applied it to defrandom. The internals of defrandom now have names like DEFRANDOM%WHATEVER, but they show up in the source as the slightly cleaner %WHATEVER.

PeterReid commented 12 years ago

I merged with the latest of your things. It was a mess, since that was my first non-trivial merge, but I think everything is intact.

Do you think the ctrlc-windows binary should be included, or should we expect people to build that from source?

calebegg commented 12 years ago

The namespacing looks awesome. Thanks!

Sorry about that! I should have waited to make those changes until after I'd merged this.

I don't feel strongly about the binary, I guess. My Windows VM is in a non-operational state currently, so I couldn't build it myself, but I also wouldn't have any use for it. What do you think?

PeterReid commented 12 years ago

I think it might as well be there... it is just one less step to get going from source.