calebegg/try-acl2

A website and evaluation service so that visitors can try ACL2 in their browser without any plugins or installation.

try-acl2's Issues

Forward/back arrows jump vertically

If you want to page through the tutorial, you have to keep adjusting where you're pointing the mouse, because the arrows are at the bottom of the page of text. Moving the arrows to the right of the title line would give them a fixed place, making it much easier to rapidly move through the tutorial.

Doesn't work in Internet Explorer 9

When I enter (+ 1 2) and press Enter in IE 9, nothing happens. 3 is not shown.

zp: Initial desc does not match REPL behavior

The factorial example says that (zp n) is t when n is not a natural number. The first thing I tried then was to execute (zp -1), only to get an error due to a violated guard. The next page of the tutorial mentions guards, but does not explain that they will cause the toplevel execution of (zp n) to fail when n is not a natural number.

All caps on iPhone.

http://stackoverflow.com/questions/3416867/how-can-i-disable-the-spell-checker-on-text-inputs-on-the-iphone

RFE: Clickable lesson TOC

I would like to be able to see where I am relative to all lessons and what the general plan of the lessons are at a glance. Having an idea where lessons are going helps integrate what I'm learning into the overall picture.

I imagine a display something like:

*** Lesson 1. Lisp (3/8)**
Lesson 2. Functions (4)
Lesson 3. Theorems (2)

Where:

• bold+star indicates the current lesson
• the number of steps in each lesson follows the title in parentheses
• the current lesson also reports the current step; the above would indicate the viewer is on step 3 of 8 steps in lesson 1.

(set-guard-checking nil) breaks the output (shows prompt char instead)

set-prover-step-limit

http://www.cs.utexas.edu/~moore/acl2/current/SET-PROVER-STEP-LIMIT.html

Floating point numbers hang/don't work.

The process seems to hang when I try to apply np to a floating point value. (np -1) is rejected immediately by the guard, but (np -1.0) or any other float just sits there, processing forever, till I reload the page.

properly indent code when you press <enter> mid-term

advance through tutorial when you type the right things.

Scroll jumps around while typing

Once the text area starts to scroll:

• Inserting a character jumps to the bottom then nearly to the top.
• Deleting a character jumps to the bottom and stays there.
• Arrowing through history jumps to the bottom and stays there.

This affects Firefox 10.0a2 (Aurora channel) under OS X 10.7.2. The custom scrollbar also does not appear in that browser.

Safari version 5.1.1 (7534.51.22) does not show these problems. It's possible they'll go away by the time FireFox 10.0 becomes beta or release, but it's something to keep an eye on.

Experiment with 40-col wrap on small widths

Activity indicator appears at top of scrollview rather than bottom

When the remote process is hung, the activity indicator appears in the top-right corner of the scrollview rather than the bottom-right, where the viewers focus is after inputting the command. This caused me to hit enter a few times before deciding things were well and hung; only when I hit backspace did focus for some reason jump to the top of the scrollview, where I could see the activity indicator.

Mention that clicking on typewriter text will copy it to REPL

I did not discover this till I went to copy-paste while writing issues. It's not obvious that the code is clickable; the lighter green background just seemed a way to visually distinguish code blocks.

It might also be appropriate to have it both copy and immediately execute, though some text will just give an error, like (zp n), which does not bind n.

(factorial (list 1 2 3)) does not return 1

The tutorial says:

You'll notice that (factorial (list 1 2 3)) returns 1, an inapplicable answer. This is a little messy, but fine.

Actually, executing that line of code gives an error:

> (factorial (list 1 2 3))
ACL2 Error in TOP-LEVEL:  The guard for the function call (ZP X), which 
is (AND (INTEGERP X) (<= 0 X)), is violated by the arguments in the
call (ZP '(1 2 3)).
See :DOC set-guard-checking for information about suppressing this
check with (set-guard-checking :none), as recommended for new users.
To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.

Tab completion

Diagnose horizontal scrollbar on iPhone.