← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/projects/sidekick/public/index.html

  • 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/public/index.html
 
1
<!HTML>
 
2
<html>
 
3
<head>
 
4
<meta charset="UTF-8">
 
5
<title>ACL2 Sidekick</title>
 
6
 
 
7
<!--
 
8
ACL2 Sidekick
 
9
Copyright (C) 2014 Kookamara LLC
 
10
 
 
11
Contact:
 
12
 
 
13
  Kookamara LLC
 
14
  11410 Windermere Meadows
 
15
  Austin, TX 78759, USA
 
16
  http://www.kookamara.com/
 
17
 
 
18
License: (An MIT/X11-style license)
 
19
 
 
20
  Permission is hereby granted, free of charge, to any person obtaining a
 
21
  copy of this software and associated documentation files (the "Software"),
 
22
  to deal in the Software without restriction, including without limitation
 
23
  the rights to use, copy, modify, merge, publish, distribute, sublicense,
 
24
  and/or sell copies of the Software, and to permit persons to whom the
 
25
  Software is furnished to do so, subject to the following conditions:
 
26
 
 
27
  The above copyright notice and this permission notice shall be included in
 
28
  all copies or substantial portions of the Software.
 
29
 
 
30
  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 
31
  IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 
32
  FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 
33
  AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 
34
  LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 
35
  FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
 
36
  DEALINGS IN THE SOFTWARE.
 
37
-->
 
38
 
 
39
<link rel="stylesheet" type="text/css" href="style.css"/>
 
40
<link rel="icon" type="image/png" href="icons/favicon.png"/>
 
41
<script src="lib/jquery-2.1.0.min.js"></script>
 
42
<script src="common.js"></script>
 
43
<script src="toolbar.js"></script>
 
44
</head>
 
45
 
 
46
<style>
 
47
<!--
 
48
 
 
49
#fancymenu {
 
50
   margin-left: 2em;
 
51
}
 
52
 
 
53
#fancymenu td {
 
54
   padding-bottom: 1em;
 
55
   padding-right: 1em;
 
56
   font-size: 90%;
 
57
}
 
58
 
 
59
#fancymenu a {
 
60
   text-decoration: none;
 
61
   font-size: 110%;
 
62
}
 
63
 
 
64
#fancymenu th {
 
65
   font-family: "Tahoma", "Geneva", "Verdana", sans-serif;
 
66
   font-size: 80%;
 
67
}
 
68
 
 
69
// -->
 
70
</style>
 
71
 
 
72
<body>
 
73
 
 
74
<div id="toolbar"></div>
 
75
 
 
76
<div id="main">
 
77
 
 
78
<div align="center" style="padding-top: 1em; padding-bottom: 1.5em;">
 
79
<table>
 
80
<tr>
 
81
<td rowspan="2"><img src="icons/superhero-right.png"></td>
 
82
<td valign="middle" class="logo"> ACL2 Sidekick </td>
 
83
<!-- <td rowspan="2"><img src="superhero-right.png"></td> -->
 
84
</tr>
 
85
<tr>
 
86
<td align="center" style="font-family: Geneva, Verdana, sans-serif; font-variant: small-caps; letter-spacing: .4em;">extreme beta</td>
 
87
</tr>
 
88
</table>
 
89
</div>
 
90
 
 
91
<div id="left" style="float: left; width: 55%;">
 
92
 
 
93
<h3 style="margin-top: 0; padding-top: 0;">Welcome!</h3>
 
94
 
 
95
<p>The ACL2 Sidekick extends ACL2 with many graphical capabilities.  It lets
 
96
you browse through your session, profile slow proofs, analyze your theory, and
 
97
inspect things right from your web browser.</p>
 
98
 
 
99
 
 
100
<h4>Tools</h4>
 
101
 
 
102
<form id="lookup_form2" method="get" action="lookup.html">
 
103
<table id="fancymenu">
 
104
<tr>
 
105
<th><a href="session.html"><img src="icons/session.png"/></a><br/>
 
106
:session</th>
 
107
<td><a href="session.html">Session Viewer</a></br/>
 
108
Explore the history of your ACL2 session<br/>
 
109
See the effects of commands</td>
 
110
</tr>
 
111
 
 
112
<tr>
 
113
<th><a href="profiler.html"><img src="icons/profiler.png"/></a><br/>
 
114
:bozo</th>
 
115
<td><a href="profiler.html">Proof Profiler</a><br/>
 
116
See what the prover is doing<br/>
 
117
Identify slow rules<br/>
 
118
</td>
 
119
</tr>
 
120
 
 
121
<tr>
 
122
<th><a href="linter.html"><img src="icons/linter.png"/></a><br/>
 
123
:lint</th>
 
124
<td><a href="linter.html">Theory Linter</a><br/>
 
125
Identify conflicting and redundant rules<br/>
 
126
</td>
 
127
</tr>
 
128
 
 
129
<tr>
 
130
<th><a href="explore.html"><img src="icons/explore.png"/></a><br/>
 
131
:explore</th>
 
132
<td><a href="explore.html">Proof Explorer</a><br/>
 
133
Carry out proofs interactively<br/>
 
134
</td>
 
135
</tr>
 
136
 
 
137
<tr>
 
138
<th><a href="lookup.html"><img src="icons/lookup.png"/></a><br/>
 
139
:show</th>
 
140
<td><a href="lookup.html">Show Anything</a><br/>
 
141
See documentation, properties, disassembly, ...<br/>
 
142
<!-- <tt><label for="lookup2">:show</label></tt> -->
 
143
<input id="lookup2" name="lookup" type="text" size="20" placeholder="append"></input>
 
144
<input type="submit" style="position: absolute; left: -9999px; width: 1px; height: 1px;" hidefocus="true" tabindex="-1"></input>
 
145
</td>
 
146
</tr>
 
147
 
 
148
</table>
 
149
</form>
 
150
 
 
151
 
 
152
</div>
 
153
 
 
154
<div id="right" style="float: left; width: 44%; margin: 0; padding-top: 0;">
 
155
 
 
156
<h4 style="margin-top: 0; padding-top: 0;">Development Notes</h4>
 
157
 
 
158
<p>Warning: this is <b>highly experimental</b> software that may have serious
 
159
bugs.  For updates or to submit any bug reports or suggestions, please see the
 
160
<a href='https://github.com/jaredcdavis/sidekick'>github project</a>.</p>
 
161
 
 
162
 
 
163
<p>General wishlist</p>
 
164
 
 
165
<ul>
 
166
 
 
167
<li>Some kind of locking mechanism for access to things like ens.</li>
 
168
 
 
169
<li>Better s-expression display: clickable function names that lead
 
170
    to the lookup page.</li>
 
171
 
 
172
<li>Current :pcb display is terrible; show how the macros expand, add
 
173
    links to lookup page, etc.</li>
 
174
 
 
175
<li>Develop help page that gets triggered by failed proofs: try
 
176
  counterexample generation, type-like analysis, syntax highlighting
 
177
  to point out the different arg, etc.</li>
 
178
 
 
179
</ul>
 
180
 
 
181
<h4>Miscellaneous Ideas</h4>
 
182
 
 
183
<p>History-management.lisp has functions
 
184
like <tt>print-time-summary</tt>.  If we plugged into that and
 
185
associated times with events/commands in a sensible way, then we could
 
186
use the information to annotate the session history with how long
 
187
everything took, sort by long-taking events, etc.  Similar
 
188
for <tt>print-steps-summary</tt>.</p>
 
189
 
 
190
<p>It also has things like <tt>print-warnings-summary</tt>.  We could
 
191
perhaps similarly associate warnings with events, and then be able t
 
192
graphically show which events had warnings.</p>
 
193
 
 
194
<p>It also has <tt>print-rules-summary</tt>.  If we associated events
 
195
with the rules that were used, we could maybe cross-reference that
 
196
against the rules introduced by commands, to be able to say, "show me
 
197
where this theorem gets used later in my file".</p>
 
198
 
 
199
<p>Is there something sensible we can do with proof-supporters?</p>
 
200
 
 
201
</div>
 
202
 
 
203
</div>
 
204
 
 
205
<div id="footer"></div>
 
206
 
 
207
</body>
 
208
</html>
 
209
 
 
210
 
 
211