Fixed some tactic docs; tests that print to stdout

scribblings/stdlib/tactics.scrbl

@@ -7,6 +7,14 @@ As Coq has shown, tactics have proven useful for doing complex proofs. In Cur, t
 built-in or provided by the language. However, any user can use meta-programming to add tactics to
 Cur. A tactic system ships in the standard library, written entirely in user-land code.
 
+@(require racket/sandbox scribble/eval)
+@(define curnel-eval
+   (parameterize ([sandbox-output 'string]
+                  [sandbox-error-output 'string]
+                  [sandbox-eval-limits #f]
+                  [sandbox-memory-limit #f])
+     (make-module-evaluator "#lang cur (require cur/stdlib/tactics/base)  (require cur/stdlib/tactics/standard) (require cur/stdlib/bool) (require cur/stdlib/nat)")))
+
 @section{Proof State and Defining Tactics}
 @defmodule[cur/stdlib/tactics/base]
 
@@ -17,11 +25,9 @@ Defines a new @tech{tactic}, at @gtech{phase} 1. A @deftech{tactic} is a Racket
 number of arguments, plus the @tech{proof state}. The @tech{proof state} must be the final argument of
 the tactic.
 
-Examples:
+@examples[#:eval curnel-eval
-@racketblock[
 (define-tactic (do-nothing ps)
   ps)
-
 (define-tactic (switch-goal i ps)
   (struct-copy proof-state ps
     [current-goal i]))
@@ -150,16 +156,12 @@ saved anywhere, only checked against the most recent theorem defined via @racket
 Note that the proof state is implicitly given to each call by @racket[proof] and should not appear as
 an explicit argument.
 
-Examples:
+@examples[#:eval curnel-eval
-@racketblock[
 (define-theorem a-silly-theorem (forall (x : Nat) Nat))
-(proof
+(proof (intro x) (by-assumption))
-  (intro x)
-  (by-assumption))
 
 (define-theorem falseo (forall (x : Type) x))
-(proof
+(eval:alts (proof (interactive)) (void))
-  (interactive))
 ]
 }
 

stdlib/tactics/base.rkt

@@ -10,6 +10,7 @@
     proof-state
     proof-state-env
     proof-state-goals
+    proof-state-current-goal
     proof-state-proof
     proof-state-theorem
     new-proof

stdlib/tactics/sartactics.rkt

@@ -130,6 +130,5 @@
     rackunit
     "../bool.rkt")
   (define-theorem meow (forall (x : Bool) Bool))
-  #;(proof
+  #;(proof (interactive))
-    (interactive))
   )

stdlib/tactics/standard.rkt

@@ -110,7 +110,8 @@
   (define-theorem meow1 (forall (x : Bool) Bool))
   (proof
     (obvious)
-    (print))
+    ;; TODO: Add ability to check output
+    #;(print))
   (define-theorem meow2 (forall (x : Bool) Bool))
   (proof
     (intro x)
@@ -121,8 +122,7 @@
   (proof (obvious))
   ;; TODO: Fix this unit test so it doesn't require interaction
   (define-theorem meow4 (forall (x : Bool) Bool))
-  #;(proof
+  #;(proof (interactive))
-    (interactive))
   ;; TODO: Add check-cur-equal? for unit testing?
   #;(check-pred (curry cur-equal? '(lambda (x : bool) x)))
   )