← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/projects/sidekick/server-raw.lsp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/projects/sidekick/server-raw.lsp
 
1
; ACL2 Sidekick
 
2
; Copyright (C) 2014 Kookamara LLC
 
3
;
 
4
; Contact:
 
5
;
 
6
;   Kookamara LLC
 
7
;   11410 Windermere Meadows
 
8
;   Austin, TX 78759, USA
 
9
;   http://www.kookamara.com/
 
10
;
 
11
; License: (An MIT/X11-style license)
 
12
;
 
13
;   Permission is hereby granted, free of charge, to any person obtaining a
 
14
;   copy of this software and associated documentation files (the "Software"),
 
15
;   to deal in the Software without restriction, including without limitation
 
16
;   the rights to use, copy, modify, merge, publish, distribute, sublicense,
 
17
;   and/or sell copies of the Software, and to permit persons to whom the
 
18
;   Software is furnished to do so, subject to the following conditions:
 
19
;
 
20
;   The above copyright notice and this permission notice shall be included in
 
21
;   all copies or substantial portions of the Software.
 
22
;
 
23
;   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 
24
;   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 
25
;   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 
26
;   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 
27
;   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 
28
;   FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
 
29
;   DEALINGS IN THE SOFTWARE.
 
30
;
 
31
; Original author: Jared Davis <jared@kookamara.com>
 
32
 
 
33
(in-package "SIDEKICK")
 
34
 
 
35
#+hons
 
36
(acl2::mf-multiprocessing t)
 
37
 
 
38
(defvar *server* nil)
 
39
 
 
40
(defun maybe-launch-browser (host port)
 
41
  (b* ((state acl2::*the-live-state*)
 
42
       ((mv ? browser state) (getenv$ "SIDEKICK_BROWSER" state))
 
43
       ((unless (and (stringp browser)
 
44
                     (not (equal browser ""))))
 
45
        nil))
 
46
    (acl2::tshell-ensure)
 
47
    (acl2::tshell-run-background
 
48
     (str::cat browser " http://" host ":" (str::natstr port) "/"))))
 
49
 
 
50
(defun start-fn (port)
 
51
  (when *server*
 
52
    (stop))
 
53
  (let* ((port (or port
 
54
                   (b* ((state acl2::*the-live-state*)
 
55
                        ((mv ? port state) (getenv$ "SIDEKICK_PORT" state))
 
56
                        (port-num (str::strval port))
 
57
                        ((when port-num)
 
58
                         port-num)
 
59
                        ;; Special hack for Centaur: fall back to FVQ_PORT if
 
60
                        ;; it is defined.
 
61
                        ((mv ? port state) (getenv$ "FVQ_PORT" state))
 
62
                        (port-num (str::strval port))
 
63
                        ((when port-num)
 
64
                         port-num))
 
65
                     ;; Else, just use the default port
 
66
                     9000)))
 
67
 
 
68
         ;; For complicated cluster setups, you might want to fudge the host in
 
69
         ;; the usage message and in maybe-launch-browser.
 
70
         (host (b* (((mv ? host state) (getenv$ "SIDEKICK_HOST" state))
 
71
                    ((when (and (stringp host)
 
72
                                (not (equal host ""))))
 
73
                     host))
 
74
                 "localhost"))
 
75
         (root
 
76
          ;; Note: apparently this has to include the trailing slash!
 
77
          (str::cat *sidekick-dir* "/public/"))
 
78
         (server (make-instance 'hunchentoot:easy-acceptor
 
79
                                :port port
 
80
                                :document-root root)))
 
81
    (setf (hunchentoot:acceptor-access-log-destination server)
 
82
          (str::cat *sidekick-dir* "/access.out"))
 
83
    (hunchentoot:start server)
 
84
    (format t "; ----------------------------------------------------------------~%")
 
85
    (format t ";~%")
 
86
    (format t ";           Sidekick started, see http://~a:~D/~%" host port)
 
87
    (format t ";~%")
 
88
    (format t "; ----------------------------------------------------------------~%~%")
 
89
    (add-handlers)
 
90
    (setq *server* server)
 
91
    (maybe-launch-browser host port))
 
92
  nil)
 
93
 
 
94
(defun stop ()
 
95
  (when *server*
 
96
    (hunchentoot:stop *server*)
 
97
    (setq *server* nil))
 
98
  nil)
 
99
 
 
100
 
 
101
; We go to some trouble to cache PBT results so that the client can poll it
 
102
; frequently.  We could do more to cache other results like PBT and PCB
 
103
; results, but this seems pretty workable so far.
 
104
 
 
105
(defvar *pbt-cached-world* nil)
 
106
(defvar *pbt-cached-result* nil)
 
107
 
 
108
; Optimizations so that when new threads create hons spaces, these spaces are
 
109
; small.
 
110
(setq acl2::*hl-hspace-str-ht-default-size*      100)
 
111
(setq acl2::*hl-ctables-nil-ht-default-size*     100)
 
112
(setq acl2::*hl-ctables-cdr-ht-default-size*     100)
 
113
(setq acl2::*hl-ctables-cdr-ht-eql-default-size* 100)
 
114
(setq acl2::*hl-hspace-addr-ht-default-size*     100)
 
115
(setq acl2::*hl-hspace-sbits-default-size*       100)
 
116
(setq acl2::*hl-hspace-other-ht-default-size*    100)
 
117
(setq acl2::*hl-hspace-fal-ht-default-size*      100)
 
118
(setq acl2::*hl-hspace-persist-ht-default-size*  100)
 
119
 
 
120
(defmacro with-sidekick-bindings (&rest forms)
 
121
  `(b* ((?state
 
122
         ;; Bind state since we often need that.
 
123
         acl2::*the-live-state*)
 
124
        (acl2::*default-hs*
 
125
         ;; Give this thread its own hons space.  Hopefully it won't use it
 
126
         ;; for anything.
 
127
         nil)
 
128
        (acl2::*read-string-should-check-bad-lisp-object*
 
129
         ;; Turn this off because otherwise we run into hash table ownership
 
130
         ;; problems, because bad-lisp-objectp is memoized and memoization
 
131
         ;; isn't thread-safe.
 
132
         nil))
 
133
     . ,forms))
 
134
 
 
135
(defun add-handlers ()
 
136
 
 
137
  (hunchentoot:define-easy-handler (pbt-handler :uri "/pbt") ()
 
138
     (setf (hunchentoot:content-type*) "application/json")
 
139
     (b* ((state acl2::*the-live-state*)
 
140
          (world (w state))
 
141
          ((when (and *pbt-cached-result* (eq world *pbt-cached-world*)))
 
142
           *pbt-cached-result*)
 
143
          ((mv er val ?state) (json-pbt 0))
 
144
          (ans (bridge::json-encode
 
145
                (list (cons :error er)
 
146
                      (cons :val val)))))
 
147
       (setq *pbt-cached-world* world)
 
148
       (setq *pbt-cached-result* ans)
 
149
       (bridge::json-encode
 
150
        (list (cons :error er)
 
151
              (cons :val val)
 
152
              (cons :new t)))))
 
153
 
 
154
  (hunchentoot:define-easy-handler (pbtx-handler :uri "/pbtx") ()
 
155
     (setf (hunchentoot:content-type*) "application/json")
 
156
     (b* ((state acl2::*the-live-state*)
 
157
          (world (w state))
 
158
          ((mv er val ?state) (json-pbt :x)))
 
159
       (bridge::json-encode
 
160
        (list (cons :error er)
 
161
              (cons :val val)))))
 
162
 
 
163
  (hunchentoot:define-easy-handler (pcb-handler :uri "/pcb") (num full)
 
164
     (setf (hunchentoot:content-type*) "application/json")
 
165
     (b* ((num (or (str::strval num)
 
166
                   (and (equal num ":X") :x)
 
167
                   (and (equal num ":x") :x)
 
168
                   0))
 
169
          (state acl2::*the-live-state*)
 
170
          (fullp (equal full "1"))
 
171
          ((mv er val ?state) (json-pcb! num fullp)))
 
172
       (bridge::json-encode
 
173
        (list (cons :error er)
 
174
              (cons :val val)))))
 
175
 
 
176
  (hunchentoot:define-easy-handler (package-handler :uri "/package") ()
 
177
    (setf (hunchentoot:content-type*) "application/json")
 
178
    (b* ((state acl2::*the-live-state*)
 
179
         (pkg   (acl2::current-package state)))
 
180
      (bridge::json-encode
 
181
       (list (cons :package pkg)))))
 
182
 
 
183
  (hunchentoot:define-easy-handler (pc-handler :uri "/pc") (num)
 
184
     (setf (hunchentoot:content-type*) "application/json")
 
185
     (b* ((num (or (str::strval num)
 
186
                   (and (equal num ":X") :x)
 
187
                   (and (equal num ":x") :x)
 
188
                   0))
 
189
          (state acl2::*the-live-state*)
 
190
          ((mv er val ?state) (json-pc num)))
 
191
       (bridge::json-encode
 
192
        (list (cons :error er)
 
193
              (cons :val val)))))
 
194
 
 
195
  (hunchentoot:define-easy-handler (disassemble-handler :uri "/disassemble") (name)
 
196
     (setf (hunchentoot:content-type*) "application/json")
 
197
     (with-sidekick-bindings
 
198
       (b* (((mv ans state) (sk-get-disassembly name state)))
 
199
         ans)))
 
200
 
 
201
  (hunchentoot:define-easy-handler (lint-handler :uri "/lint") ()
 
202
     (setf (hunchentoot:content-type*) "application/json")
 
203
     (b* (((mv ans state) (json-lint state)))
 
204
       ans))
 
205
 
 
206
  (hunchentoot:define-easy-handler (props-handler :uri "/props") (name)
 
207
     (setf (hunchentoot:content-type*) "application/json")
 
208
     (with-sidekick-bindings
 
209
       (b* (((mv ans state) (sk-get-props name state)))
 
210
         ans)))
 
211
 
 
212
  (hunchentoot:define-easy-handler (origin-handler :uri "/origin") (name)
 
213
     (setf (hunchentoot:content-type*) "application/json")
 
214
     (with-sidekick-bindings
 
215
       (b* (((mv ans state) (sk-get-origin name state)))
 
216
         ans)))
 
217
 
 
218
  (hunchentoot:define-easy-handler (xdoc-handler :uri "/xdoc") (name)
 
219
     (setf (hunchentoot:content-type*) "application/json")
 
220
     (with-sidekick-bindings
 
221
       (b* (((mv ans state) (sk-get-xdoc name state)))
 
222
         ans)))
 
223
 
 
224
  (hunchentoot:define-easy-handler (webcommand-handler :uri "/webcommands") ()
 
225
     (setf (hunchentoot:content-type*) "application/json")
 
226
     (b* ((commands (get-webcommands-stack)))
 
227
       (bridge::json-encode
 
228
        (list (cons :commands commands)))))
 
229
 
 
230
  (hunchentoot:define-easy-handler (eventdata-handler :uri "/eventdata") (name)
 
231
     (setf (hunchentoot:content-type*) "application/json")
 
232
     (with-sidekick-bindings
 
233
       (b* (((mv ans state) (sk-get-eventdata name state)))
 
234
         ans)))
 
235
 
 
236
  (hunchentoot:define-easy-handler (ubt-handler :uri "/ubt" :default-request-type :post)
 
237
                                   ((n :parameter-type 'string))
 
238
    (setf (hunchentoot:content-type*) "application/json")
 
239
    (with-sidekick-bindings
 
240
      (b* (((mv ans state) (sk-undo-back-through n state)))
 
241
        ans)))
 
242
 
 
243
;; Proof explorer
 
244
 
 
245
  (hunchentoot:define-easy-handler (handle-explore-th :uri "/explore-th") ()
 
246
     (setf (hunchentoot:content-type*) "application/json")
 
247
     (with-sidekick-bindings
 
248
       (b* (((mv ans state) (sk-explore-th state)))
 
249
         ans)))
 
250
 
 
251
  (hunchentoot:define-easy-handler (handle-explore-commands :uri "/explore-commands") ()
 
252
     (setf (hunchentoot:content-type*) "application/json")
 
253
     (with-sidekick-bindings
 
254
       (b* (((mv ans state) (sk-explore-commands state)))
 
255
         ans)))
 
256
 
 
257
  (hunchentoot:define-easy-handler (explore-undo-handler :uri "/explore-undo" :default-request-type :post)
 
258
                                   ((n :parameter-type 'string))
 
259
    (setf (hunchentoot:content-type*) "application/json")
 
260
    (with-sidekick-bindings
 
261
      (b* (((mv ans state) (sk-explore-undo n state)))
 
262
        ans)))
 
263
 
 
264
  (hunchentoot:define-easy-handler (explore-contrapose-handler :uri "/explore-contrapose" :default-request-type :post)
 
265
                                   ((n :parameter-type 'string))
 
266
    (setf (hunchentoot:content-type*) "application/json")
 
267
    (with-sidekick-bindings
 
268
      (b* (((mv ans state) (sk-explore-contrapose n state)))
 
269
        ans)))
 
270
 
 
271
  (hunchentoot:define-easy-handler (explore-demote-handler :uri "/explore-demote" :default-request-type :post)
 
272
                                   ((n :parameter-type 'string))
 
273
    (setf (hunchentoot:content-type*) "application/json")
 
274
    (with-sidekick-bindings
 
275
      (b* (((mv ans state) (sk-explore-demote n state)))
 
276
        ans)))
 
277
 
 
278
  (hunchentoot:define-easy-handler (explore-drop-handler :uri "/explore-drop" :default-request-type :post)
 
279
                                   ((n :parameter-type 'string))
 
280
    (setf (hunchentoot:content-type*) "application/json")
 
281
    (with-sidekick-bindings
 
282
      (b* (((mv ans state) (sk-explore-drop n state)))
 
283
        ans)))
 
284
 
 
285
  (hunchentoot:define-easy-handler (explore-split-handler :uri "/explore-split" :default-request-type :post)
 
286
                                   ()
 
287
    (setf (hunchentoot:content-type*) "application/json")
 
288
    (with-sidekick-bindings
 
289
      (b* (((mv ans state) (sk-explore-split state)))
 
290
        ans)))
 
291
 
 
292
  (hunchentoot:define-easy-handler (explore-pro-handler :uri "/explore-pro" :default-request-type :post)
 
293
                                   ()
 
294
    (setf (hunchentoot:content-type*) "application/json")
 
295
    (with-sidekick-bindings
 
296
      (b* (((mv ans state) (sk-explore-pro state)))
 
297
        ans)))
 
298
 
 
299
 
 
300
  )