Permalink
Browse files

Moved help to proofpad.org, moved icons

  • Loading branch information...
calebegg committed Dec 31, 2012
1 parent 8ff99b6 commit fbfb7d0e2159c9ecfa5d91e030fecb00f2097b5e
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
View
@@ -1,47 +0,0 @@
-import os
-import shutil
-
-from markdown import markdown
-from django.template.loader import render_to_string
-from django.template import Context, Template
-import django.conf
-
-ROOT = os.path.abspath(os.path.dirname(__file__))
-OSES = ['mac', 'win', 'linux']
-
-def main():
- django.conf.settings.configure(
- TEMPLATE_DIRS=[os.path.join(ROOT, 'templates')])
- for os_name in OSES:
- dirname = os_name
- path = os.path.join(ROOT, dirname)
- try:
- shutil.rmtree(os.path.join(ROOT, dirname))
- except OSError:
- pass
- os.makedirs(path)
- for fn in os.listdir(os.path.join(ROOT, 'templates')):
- if fn in OSES or fn.startswith('.'):
- continue
- elif fn.endswith('.md'):
- newfn = fn[:-3] + '.html'
- with open(os.path.join(ROOT, 'templates', fn), 'r') as f:
- source = markdown(f.read())
- with open(os.path.join(path, newfn), 'w') as f:
- t = Template(source)
- f.write('<link href="style.css" rel="stylesheet" />')
- f.write(t.render(Context({'os': os_name,
- 'is_mac': os_name == 'mac',
- 'is_win': os_name == 'win',
- 'is_linux': os_name == 'linux'})))
- elif fn.endswith('.html'):
- with open(os.path.join(path, fn), 'w') as f:
- f.write(render_to_string(fn, {'os': os_name,
- 'is_mac': os_name == 'mac',
- 'is_win': os_name == 'win',
- 'is_linux': os_name == 'linux'}))
- else:
- shutil.copy(os.path.join(ROOT, 'templates', fn), path)
-
-if __name__ == '__main__':
- main()
View
Binary file not shown.
View
Binary file not shown.
@@ -1,8 +0,0 @@
-<html>
- <head>
- <title>Proof Pad help</title>
- </head>
- <body>
- {{ os }}
- </body>
-</html>
@@ -1,44 +0,0 @@
-Random generators
-=================
-
-`(random-between low high)` -- Generates a random number uniformly chosen between `low` and `high`, inclusive.
-
-`(random-natural)` -- Generates a random natural number (above zero).
-
-`(random-positive)` -- Generates a random positive number (above one).
-
-`(random-integer)` -- Generates a random integer.
-
-`(random-rational)` -- Generates a random rational number (by dividing two random integers)
-
-`(random-complex)` -- Generates a random complex number (using two random rationals)
-
-`(random-number)` -- Randomly generates either an integer, a rational, or a complex number.
-
-`(random-data-size)` -- Generates a random natural number, but favors smaller numbers. Appropriate if this value is going to determine the amount of data in a structure.
-
-`(random-natural-list)` -- Generates a list of `(random-natural)` values, using a length determined by `(random-data-size)`.
-
-`(random-natural-list-of-length ln)` -- Generates a list of `(random-natural)` values of a specified length. `ln` must be either a fixed natural number (such as 10) or a variable. So, for instance, `(random-natural-list-of-length (random-natural))` will give an error. Instead, generate the length separately: `(n :value (random-natural) xs :value (random-natural-list-of-length n))`
-
-`(random-integer-list)` and `(random-integer-list-of-length ln)` -- similar to above
-
-`(random-digit-list)` and `(random-digit-list-of-length ln)` -- random lists of numbers between 0 and 9
-
-`(random-between-list low high)` and `(random-between-list-of-length low high ln)` -- similar to above; generates values between `low` and `high` inclusive (using `(random-between low high)`).
-
-`(random-increasing-list)` -- A list of values that strictly go up (a sorted list).
-
-**Note:** The below `random-list-of` versions of the above functions are included in Proof Pad for compatibility with DrACuLa; They don't add any functionality over the above forms. Additionally, unlike in DrACuLa, the parameters to `random-list-of` must match one of the below templates, or they won't work. I recommend that you use the above generators instead.
-
-`(random-list-of (random-natural))` -- Alternate syntax for `(random-natural-list)`
-
-`(random-list-of (random-natural) :size ln)` -- Alternate syntax for `(random-natural-list-of-length ln)`
-
-`(random-list-of (random-integer))` -- Alternate syntax for `(random-integer-list)`
-
-`(random-list-of (random-integer) :size ln)` -- Alternate syntax for `(random-integer-list-of-length ln)`
-
-`(random-list-of (random-between low high))` -- Alternate syntax for `(random-between-list low high)`
-
-`(random-list-of (random-between low high) :size ln)` -- Alternate syntax for `(random-between-list-of-length low high ln)`
No changes.
@@ -1,95 +0,0 @@
-<!doctype html>
-<html>
- <head>
- <title>Proof Pad help for {{ os }}</title>
- <link href="style.css" rel="stylesheet" />
- </head>
- <body>
- <h1>Introduction to Proof Pad</h1>
- <img src="../media/intro-{{ os }}.png" />
- <h2>The REPL</h2>
- <p>The REPL, or "Read-Eval-Print loop", is located in the bottom half
- of the main Proof Pad window. Essentially, the REPL will execute any
- code you type in the text field on bottom (the "prompt") and show the
- result in the log above.
- <p>Try typing some math into the REPL now:
- <pre><code>(+ 1 2)</code></pre>
- If ACL2 is functioning correctly, you should get
- <pre><code>3</code></pre>
- back. (If you don't, see <a href="troubleshooting.html">the
- troubleshooting page.</a>)
- <p>There are a couple of things to note at this point. First, the '3'
- has a checkmark with a green background next to it. This means that the
- function call executed without errors. A red 'x' means that there was an
- error, and a '&lt;' sign means that the message is informational (not
- in direct response to something you did).</p>
- <p>The REPL is a good place to test the functions you write in the
- definitions area, or just to get a sense of how to use a certain
- function or feature.</p>
- <h2>The definitions area</h2>
- <p>The definitions area is where you write your functions, theorems, and
- other state-altering expressions. Here's a definition for 'sum' that you
- can either retype or copy and paste:
- <pre><code>(defun sum (xs)
- (if (endp xs)
- 0
- (+ (first xs)
- (sum (rest xs)))))</code></pre>
- <p>When you type or paste this into the definitions area, you might
- notice that the background color of the proof bar goes from white to
- grey to light green, and a checkmark appears. This simply means that the
- code was executed by ACL2 without any problems. We'll talk more about
- the proof bar in the <a href="#proofbar">next section</a>
- <p>Definitions occur in an ordered way in the file; if you want to use
- the function "foo" within the function "bar", you must put the
- definition of "foo" above the definition of "bar". This has to do with
- how ACL2 processes events; the ACL2 "world" must be logically consistent
- after each and every event, so if you used "foo" before defining it,
- ACL2 might be accepting something that won't actually work.
- <h2 id="proofbar">Proof bar</h2>
- <p>The proof bar is the (normally white) bar to the left of the
- definitions panel that allows you to view and manipulate the status of
- ACL2 with respect to your code.
- <p>By default, Proof Pad is passing all of your functions, theorems,
- tests, etc to ACL2 automatically. This automatic admission occurs in
- <tt>:program</tt> mode<sup>1</sup>, an ACL2 mode where ACL2 doesn't
- worry as much about logic. The intent of this is to let you test your
- functions in the REPL, even if they aren't carefully written enough in
- the way ACL2 expects to be used in :logic mode.
- <p>If the automatic admission succeeds, the proof bar turns light green
- next to the admitted code. If it fails, it instead turns red, an 'x' is
- shown, and the details pane opens up to show you the error message you
- received.
- <p>You will probably want to admit these functions to ACL2's
- <tt>:logic</tt> mode (a requirement if you want to prove theorems). To
- do this, click on the proof bar next to the function you want to admit.
- As you hover over the proof bar, it will show you a preview of what's
- going to be done; in particular, if you want to admit an expression, you
- have to first admit all the expressions above it. The proof bar handles
- this for you.
- <p>Once you've admitted some code to the ACL2 logic (which can take
- some time for complex functions or theorems), the proof bar turns green
- next to the form or forms that were admitted. If ACL2 encounters an
- error, a red 'x' is shown and the error pane opens to show you the
- response that Proof Pad got from ACL2. If the proof or admission was
- successful, the error pane won't open up by default. If you're curious
- about what the ACL2 output was, you can click the '&gt;' sign to the
- right of the form you admitted (though you rarely care about that if the
- proof succeeds).
- <p>Try admitting your <tt>sum</tt> function from before.</p>
- <p>Admitted code becomes read-only in Proof Pad, since editing it
- requires re-admitting it to ACL2. To un-admit some code (and thus make
- it editable), just click on the proof bar again next to the expression
- you want to edit. Proof Pad will roll back ACL2 to the function you want
- to edit. You can make your edits and then re-admit.
- <div class="footnotes">
- <ol>
- <li>You can read more about ACL2's two modes <a
- href="http://www.cs.utexas.edu/~moore/acl2/current/DEFUN-MODE.html">here</a>,
- though this is strictly optional reading; you don't need to have
- an intimate understanding of this for Proof Pad, since it
- abstracts these parts away for you.
- </ol>
- </div>
- </body>
-</html>
View
@@ -1,18 +0,0 @@
-body {
- width: 50%;
- min-width: 700px;
- max-width: 1000px;
- margin: 15px auto;
- font-family: sans-serif;
-}
-pre code {
- display: block;
- padding: 5px;
- border-left: solid #ccc 1px;
- background: #eee;
- margin: 10px 20px;
-}
-.footnotes {
- border-top: solid black 1px;
- font-size: smaller;
-}
@@ -1,166 +0,0 @@
-Tutorial: reverse of reverse
-============================
-
-Step 1: Define reverse
-----------------------
-
-`(reverse xs)` is a built-in function that takes a list and returns a list with
-all of the elements in the opposite order. We'll be defining another version of
-it called `rev`.
-
-In order to define a recursive function in ACL2, we need to think about what it
-would return in a couple of different cases. The first case is when the
-argument, `xs`, is empty (or `nil`). The reverse of an empty list is just an
-empty list:
-
- (rev nil) = nil
-
-Now, what if `xs` is not empty? If it's not empty, we can break it up into its
-first element and the rest of the list, using `(first xs)` and `(rest xs)`,
-respectively. We want to take these parts and assemble a new, reversed list. We
-can just use `(rev (rest xs))` to reverse the rest of the list, but what do we
-do with `(first xs)`?
-
-Consider an example: `(rev (list 1 2 3 4 5))`. After we split it up into two
-parts, `1` and `(list 2 3 4 5)`, we can reverse the list part to get `(list 5 4
-3 2)`. And what we want for the whole list is `(list 5 4 3 2 1)`. So we need to
-put `1` at the end of the reversed list.
-
- (rev xs) = (put-at-end (first xs) (rev (rest xs)))
-
-For `(put-at-end x xs)`, we can use `(append)`:
-
- (defun put-at-end (x xs)
- (append xs (list x)))
-
-Putting it all together, we get:
-
- (defun rev (xs)
- (if (endp xs) ; Test if xs is empty
- nil
- (put-at-end (first xs)
- (rev (rest xs)))))
-
-Step 2: Test reverse
---------------------
-
-Now that we have a good working definition for reverse, we need to test it to
-see that it works.
-
-The quickest way to test a function you've defined is with the REPL. The REPL is
-the part of Proof Pad below the definitions area. After you've typed the
-definitions for `put-at-end` and `rev` into the main definitions area, type
-`(rev (list 1 2 3 4 5))` into the text field at the very bottom of Proof Pad,
-and click "Run" (or press "Enter"). You instantly see the result, which is `(5 4
-3 2 1)`.
-
-We can automate this process to make sure that `rev` continues to match our
-expectations, even if we change or rewrite it. The simplest automatic test
-provided by Proof Pad is `check-expect`. To use it, first include the "testing"
-book:
-
- (include-book "testing" :dir :teachpacks)
-
-Now write a test like this:
-
- (check-expect (rev (list 1 2 3 4 5)) (list 5 4 3 2 1))
-
-`check-expect` will automatically run the test and show a green bar to the left
-when it passes. A test passes when the two arguments to `check-expect` evaluate
-to the same thing (in this case, the list `(5 4 3 2 1)`).
-
-We could write some more check-expect style tests, but they can only get us so
-far. It would be even better if we could write a test that will check several
-types of lists to see that our function does what we want. To do this, we need
-to write a property-style test. First, include the "doublecheck" book
-(DoubleCheck is the name of the testing library):
-
- (include-book "doublecheck" :dir :teachpacks)
-
-A doublecheck test has three parts: a name, a set of data generators, and a
-body. The body is evaluated several times with different, randomly generated
-data, and if it evaluates to `t` (which is Lisp's version of `true`), then the
-test passes. If a single case fails, the test fails.
-
-One property we can test with DoubleCheck is that reversing a list twice gives
-you the same list you started with. I'll start by showing the test, then talk
-about the parts:
-
- (defproperty rev-rev-test
- (xs :value (random-integer-list))
- (equal (rev (rev xs)) xs))
-
-The name of the test is `rev-rev-test`. The name isn't important, except that
-each one has to be unique. This test has one generator. It generates values
-called `xs`, using the `(random-integer-list)` generator. You can see what kinds
-of values this generator returns by typing it in the REPL.
-
-Finally, we have the body: we want to show that `(rev (rev xs))` is equal to
-just `xs`.
-
-To run the test, just paste it into the definitions area. It will run, and if it
-passes, a green bar will appear to the left of the test.
-
-Try changing the `nil` in the definition of `rev` above to something else, like
-`1`. You can see that this makes the test fail. When a test fails, it shows you
-which cases it failed on. In this case, it fails all cases, but it might help
-you to diagnose the problem if only some of the cases fail too. When a test
-fails, it's often a good idea to go back to the REPL and try some of the failed
-values to see what you get.
-
-Step 3. Proving `rev-rev`
--------------------------
-
-DoubleCheck properties are nice, but they aren't perfect. They only test the
-types of values that you generate, and you might have a bug that impacts only a
-small subset of cases, which means the generated test cases are unlikely to
-expose the bug.
-
-To strengthen our properties, we can run them through ACL2's theorem prover to
-try to prove that it holds for all input values, not just the randomly selected
-ones that DoubleCheck uses.
-
-In this case, our test as written will fail. The reason for the failure is that
-it doesn't quite hold for any value of `xs`. In particular, to ACL2's logic,
-`(rev 1)` = `nil`. If you try to run `(rev 1)` in the REPL, you'll get a guard
-error. Guards are restrictions on what values a function will take; in this
-case, `(endp xs)` expects a list, and we gave it a number. However, ACL2's
-internal logic will run the theorem just fine, with `(endp xs)` returning `t`
-when `xs` is 1, making `(rev 1)` return `nil`.
-
-In order to correct this, we need to add a hypothesis to our property:
-
- (defproperty rev-rev
- (xs :value (random-integer-list)
- :where (true-listp xs))
- (equal (rev (rev xs)) xs))
-
-This way, ACL2 will know to only concern itself with values that satisfy
-`true-listp` -- values that are lists.
-
-With this correction in place, you can run the property through ACL2's logic by
-clicking on the green bar to the left of it. If everything has been entered
-correctly, ACL2 will succeed, and the bar will turn dark green (with a
-checkmark), indicating that the property has been proven correct.
-
-The whole file so far is:
-
- (include-book "testing" :dir :teachpacks)
- (include-book "doublecheck" :dir :teachpacks)
-
- (defun put-at-end (x xs)
- (append xs (list x)))
-
- (defun rev (xs)
- (if (endp xs) ; Test if xs is empty
- nil
- (put-at-end (first xs)
- (rev (rest xs)))))
-
- (check-expect (rev (list 1 2 3 4 5))
- (list 5 4 3 2 1))
-
- (defproperty rev-rev
- (xs :value (random-integer-list)
- :where (true-listp xs))
- (equal (rev (rev xs)) xs))
@@ -1,9 +0,0 @@
-
-<html>
- <head>
- <title>Tutorial</title>
- </head>
- <body>
- asdf {{ os }}
- </body>
-</html>

0 comments on commit fbfb7d0

Please sign in to comment.