Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Merge notes files.

  • Loading branch information...
commit a3d2ed9d2c41b3e32a3d5e1f8683549628fff5fa 1 parent 79aa94d
Jesse Alama authored
Showing with 247 additions and 0 deletions.
  1. +247 −0 notes.org
View
247 notes.org
@@ -1,3 +1,250 @@
+* TODO tmp directory naming: say "mitems" or somethig like that
+* TODO error messaging
+ It never gives anything useful, when the mizar tools die.
+* TODO Broken articles [29/85]
+ - [X] algspec1 (this breaks on mws, but not on my machine)
+ - [X] analmetr (this breaks on mws, but not on my machine)
+ - [X] anproj_2 (this breaks on mws, but not on my machine)
+ - [ ] binop_1 (this breaks on mws, but not on my machine)
+ - [ ] complfld
+ - [ ] conmetr1
+ - [ ] euclid
+ - [ ] filter_1
+ - [ ] fsm_1
+ - [ ] funcop_1
+ - [ ] funct_7
+ - [ ] fvsum_1
+ - [ ] gobrd11
+ - [ ] gobrd12
+ - [ ] gobrd13
+ - [ ] gr_cy_1
+ - [ ] group_2
+ - [ ] hessenbe
+ - [ ] isocat_2
+ - [ ] jordan
+ - [ ] lattice4
+ - [ ] lopclset
+ - [ ] mcart_2
+ - [ ] member_1
+ - [ ] midsp_2
+ - [ ] nat_lat
+ - [ ] nattra_1
+ - [ ] normform
+ - [ ] polynom1
+ - [ ] power
+ - [ ] projred1
+ - [ ] radix_1
+ - [ ] real_lat
+ - [ ] relset_1
+ - [ ] rlsub_1
+ - [ ] rlsub_2
+ - [ ] rmod_2
+ - [ ] rmod_3
+ - [ ] rmod_4
+ - [ ] seq_4
+ - [ ] seqm_3
+ - [ ] toprealb
+ - [ ] transgeo
+ - [ ] translac
+ - [ ] vectsp_1
+ - [ ] vectsp_5
+ - [ ] waybel25
+ - [ ] waybel26
+ - [ ] waybel27
+ - [ ] waybel28
+ - [ ] waybel29
+ - [ ] waybel_4
+ - [ ] xboole_0
+ - [ ] xxreal_3
+ - [ ] yellow16
+ - [ ] zf_fund1
+ - [ ] zf_lang
+ - [X] analmetr
+ - [X] arytm_3
+ - [X] classes2
+ - [X] dtconstr
+ - [X] filter_1
+ - [X] fib_num4
+ - [X] jgraph_2
+ - [X] jordan
+ - [X] metric_1
+ - [X] nagata_2
+ - [X] numbers
+ - [X] pre_ff
+ - [X] qmax_1
+ - [X] scmbsort
+ - [X] scm_comp
+ - [X] sin_cos
+ - [X] scmisort
+ - [X] scpinvar
+ - [X] scpisort
+ - [ ] scpqsort (watch out, this one is huge)
+ - [X] sincos10
+ - [X] topgen_3
+ - [X] toprealb
+ - [X] vectsp_1
+ - [X] xreal_0 (like sin_cos)
+ - [X] xcmplx_0 (like sin_cos)
+ - [X] zf_model
+** TODO Broken for some weird reason
+ These kill the analyzer:
+ - afinsq_1 (item11 breaks the verifier)
+ - classes1 (JA1 alone breaks this)
+ - complex1 (dellink alone breaks this)
+ - clvect_1 (JA1 alone breaks this)
+ - euclid_9 (item51 breaks the verifier)
+ - int_3 (item4 breaks the verifier)
+ - lattice3 (item4 breaks the verifier)
+* DONE Optimization of Josef's dependency code, in the case of theorems
+ We can determine, from the .refx file, precisely which were used.
+* TODO Consider using relprem in the reduction code
+* DONE Itemize TARSKI
+ CLOSED: [2010-12-31 Fri 14:00]
+ Break up TARSKI into bits, so that we have see a finer dependence on it.
+* DONE Re-itemize TARSKI
+ Watch out for canceled stuff!
+* TODO Don't create a directory for itemizing a non-existence article
+* TODO Broken as of 2011/04/26
+ - waybel_4: reported
+* TODO Put the original, untransformed .miz into the article directory
+* Website
+** DONE Strip the ":: CKB5 semantic presentation" header
+** DONE Adjust XSL stylesheet so that it doesn't output the HTML element
+ There's a "body_only" option in Josef's XSL, but it seems that even
+ when this is set to true, we still get stuff like
+
+ <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+ <html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
+** DONE Tarski and Hidden presentation
+ At the moment, trying to view items from thes two article results
+ in 404s.
+** TODO Smarter presentation of long lists of dependencies
+ The result is that these long lists can make the page into giant
+ lists, obscuring content. Perhaps instead of presenting a flat
+ list of dependencies, we could divide the dependencies by article.
+** TODO Article-view of dependencies
+ For now, we pesent dependencies only for particular items. When
+ viewing a whole article, we might present all of the dependencies
+ of that article (the union of the dependencies of the article's
+ items).
+** TODO SVG presentation
+ For item-level dependencies and article-level dependencies, as well
+ as for the whole dependency graph
+** DONE Path search
+ URLs like
+
+ /funct_1/5/xboole_0/10
+
+ could be a presentation of a path (if one exists) of dependencies
+ that goes from funct_1:5 to xboole_0:10. Perhaps show all paths
+ (not sure how complex the computation is going to be). We might
+ try article level dependencies, too:
+
+ /funct_1/xboole_0
+
+ would show all paths from any item of funct_1 to any item of
+ xboole_0. (Now we're talking large-scale computation, almost
+ ceratinly.)
+** TODO Interface for testing dependencies
+ Suppose one is interested in verifying the dependency data: is it
+ really true that the item I'm now looking at depends on one of the
+ items in the given list? One could verify this claim by looking at
+ the result of attempting to verify the current item in a context in
+ which the suspicious dependent item is missing. One could then see
+ the error output from the verifier (there had better be such error
+ output!).
+** DONE Main page introducing the dependencies
+** DONE Sort list of dependencies
+ hidden:1, hidden:2, etc., not hidden:4, hidden:3, ...
+** DONE Steal favicon.ico from mizar.org
+** DONE Set this thing up at mizar.cs.ualberta.ca
+** TODO Color scheme for different kinds of items
+
+ Seems to me that we could have four kinds:
+
+ - theorem/lemma/deftheorem
+ - scheme
+ - constructor/definiens/pattern
+ - cluster/identification
+
+ Use colorschemedesigner. Cool candidates:
+
+ - http://colorschemedesigner.com/#0041Tw0w0w0w0
+ - http://colorschemedesigner.com/#0442pmKOzO7L9
+ - http://colorschemedesigner.com/#3a41TNmNbKVnj
+** TODO Serve the site through port 80, rather than 4242
+ Some places might block traffic to and from this port. (The
+ network that I sometimes use at the University of Lisbon blocks
+ it.)
+** TODO Error handling: if we get a lisp error, don't display a ghastly "Internal Server Error" page
+** DONE Get a liting of all titles and authors for the MML
+ Convert it to HTML; give back to Mizar community.
+** TODO Set up some kind of testing
+ Desparately needed.
+
+ Use the example of drakma-based testing at
+
+ http://weitz.de/hunchentoot/#testing
+** DONE Freek Wiedijk's list
+** TODO Provide a "site is down for a moment, back soon!" server
+ There could be a function for disabling the current server. It
+ unregisters all URIs from the current acceptor, then sets up a new
+ regular expression-based acceptor that takes all URIs (i.e.,
+ request URIs matching the pattern "*") and simply prints a "This
+ site is temporarily down for maintainence and will be back
+ shortly." There would then be a function that re-enables the site
+ by first de-registering the global URI dispatcher, and then
+ re-registering all the URIs for the (intended, non-maintainance)
+ site.
+** DONE Permit loading the site with just a specified initial segment of mml.lar
+** TODO Save the site data in list format, so we can simply read it.
+ Probably faster. Alternatively, we could compile the lisp, and then load
+ it later. That would be ideal. We need to think of a way of flexibly
+ storing and possibly recomputing such data, though.
+** TODO Figure out a workaround for Josef's xsl:document hack.
+ That way, I can apply stylesheets live, and don't need to have
+ static HTML files sitting around.
+** DONE Respond gracefully to HEAD requests
+ Don't do a big expensive computation just to see whether a HEAD
+ works. (I have in mind cases where we search for paths.)
+** DONE Respond gracefully to OPTIONS requests
+** DONE Disallow POST, PUT, DELETE
+ For now. If we want to permit people to upload articles for their
+ own itemization, we will want to support at least POST.
+
+** TODO Save the server state occasionally, restart using that image
+ In case the whole process dies.
+** TODO Piotr's suggestion for presenting the dependency data
+ Present the list of dependencies not in alphabetical order, but by
+ the order determined by the dependency graph itself.
+
+ The whole thing is a directed acyclic graph, so this is possible,
+ but the computation of this might be expensive.
+** TODO When computing paths, present an interface for specifying beginning, intermediate, and final nodes
+** TODO Smart restart when the disk is full and unable to write to the logs
+** TODO Veifying dependencies
+ Dependence verification tasks:
+
+ - verify, with mizar, for an item A, that the set of items on which
+ we claim that A depends really is sufficient to prove A. (Taken
+ for granted.)
+ - verify, with an ATP, for an item A, that the set of items on
+ which we claim that A depends really is sufficient to prove A.
+ - verify, with an ATP, for an item A, that removing any one of the
+ items on which we claim that A depends result in
+ countersatisfiability. (Won't necessarily happen;
+ mizar-minimality might not always coincide with logical
+ minimality.)
+
+ URIs:
+
+ - /dependence/<item>/sufficiency: verify that the claimed set of
+ needed items is sufficient to justify the item
+
+ - /dependence/<item>/minimality: verify that the claimed set of
+ needed items is minimal: no item can be removed from the set.
+** TODO A script for starting the site when the computer starts up
+ Should be some standard infrastructure for this.
* How to itemize multiple articles
I think we've got itemization of single articles down. How to
itemize multiple articles?
Please sign in to comment.
Something went wrong with that request. Please try again.