src/Tools/WWW_Find/doc/README
author wenzelm
Wed, 02 Dec 2009 12:04:07 +0100
changeset 33930 6a973bd43949
parent 33817 f6a4da31f2f1
permissions -rw-r--r--
slightly less ambitious settings, to avoid potential out-of-memory problem;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     1
Requirements
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     2
------------
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     3
  lighttpd
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     4
  polyml (other ML systems untested)
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     5
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     6
Quick setup
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     7
-----------
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     8
*  install lighttpd if necessary
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     9
   (and optionally disable automatic startup on default www port)
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    10
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    11
Quick instructions
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    12
------------------
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    13
* start the server with:
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    14
    isabelle wwwfind start
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    15
  (add -l for logging from ML)
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    16
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    17
* connect (by default) on port 8000:
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    18
    http://localhost:8000/isabelle/find_theorems
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    19
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    20
* test with the echo server:
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    21
    http://localhost:8000/isabelle/echo
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    22
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    23
* check the status with:
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    24
    isabelle wwwfind status
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    25
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    26
* stop the server with:
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    27
    isabelle wwwfind stop
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    28