<div class="gmail_quote">On Mon, Oct 1, 2012 at 5:32 AM, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> <div class="im">Hi Ramana, >> You can prefix an input with a type </div>> Is this documented anywhere? <div class="im">> In particular, would it be hard to include in the usage/help text the > tool emits, or to write a man page or manual for the tool? </div>I've just released a version of the tool with much improved usage documentation,</blockquote><div> Thanks! I had packaged the tool for Arch Linux (and derivatives) here, when 1.2 first came out: <a href="https://aur.archlinux.org/packages.php?ID=61879">https://aur.archlinux.org/packages.php?ID=61879</a> But I notice that the new release does not have a new version, just a new "release date". Should the package version include the release date as well? I.e., the version would be 1.2.20120930. (That would mean I should update the AUR package...) </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> so for instance opentheory info -h shows the legal input formats for the info command. Also, the output from the opentheory help command (copied below) is in a suitable form to be turned into a man page if needed for a distro package of the opentheory tool. </blockquote><div> If the tool can spit it out, I don't see why a man page with the same text is necessary. (I guess you meant if there are packaging rules that require a man page for everything...?) </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> Cheers, Joe _____________________________________________ $ opentheory help opentheory: displaying help on all available commands usage: opentheory [global options] command [command options] INPUT ... where the available commands are: opentheory cleanup ..... clean up theory packages staged for installation opentheory export ...... export an installed theory package from OpenTheory opentheory help ........ display help on all available commands opentheory info ........ extract information from theory packages and files opentheory init ........ initialize a new package directory opentheory install ..... install a package from a theory file or repo opentheory list ........ list installed theory packages opentheory uninstall ... uninstall an installed theory package opentheory update ...... update repo package lists opentheory upload ...... upload theory packages to a repo Displaying all options: -d, --root-dir DIR .... (global) use this theory package directory --repo REPO ........... (global) use these theory package repos --format FORMAT ....... (info) format package information --information ......... (info) display all package information --summary ............. (info) display the package summary --article ............. (info) output the theory package in article format --inference ........... (info) display the number of primitive inferences --theory .............. (info) display the package theory file --files ............... (info) list the package files --includes ............ (info) list the included theory packages --requires ............ (info) list satisfying required theory packages --document ............ (info) output the package document in HTML format --theorems ............ (info) output the package theorems in article format -o, --output FILE ..... (info) write previous package information to FILE --show-assumptions .... (info) do not omit satisfied assumptions --show-derivations .... (info) show the assumptions/axioms for each theorem --upgrade-theory ...... (info) upgrade the theory file to the latest versions --preserve-theory ..... (info) do not optimize the theory file --repo ................ (init) configure the new package directory as a repo --reinstall ........... (install) uninstall the package if it exists --auto-uninstall ...... (install) also uninstall included packages --manual .............. (install) do not also install included packages --name NAME ........... (install) confirm the package name --checksum CHECKSUM ... (install) confirm the package checksum --stage ............... (install) stage the package for installation --dependency-order .... (list) list packages in dependency order --include-order ....... (list) list packages in include order --reverse-order ....... (list) reverse the order --format FORMAT ....... (list) set the output format --auto ................ (uninstall) also uninstall included packages --manual .............. (upload) do not also upload subtheory packages --yes ................. (upload) do not ask for confirmation -- .................... no more options -?, -h, --help ........ display option information and exit -v, --version ......... display version information INPUT is one of the following forms: 1. A theory package: NAME-VERSION or NAME (for the latest version) 2. A theory file: FILE.thy or theory:FILE 3. A proof article file: FILE.art or article:FILE 4. A theory package tarball: FILE.tgz or tarball:FILE 5. A theory package staged for installation: staged:NAME-VERSION The list command takes a special QUERY input: QUERY represents a subset S of the installed theory packages P, as follows: 1. A FUNCTION expression in the grammar below is parsed from the command line, which represents a function f of type S -> S 2. Another function g of type S -> S is computed, which may be represented by the FUNCTION expression ~Empty (Latest - Subtheories) All 3. The set f(g({})) is evaluated as the result, where {} is the empty set FUNCTION // represents a function with type S -> S <- SET // the constant function with return value SET || PREDICATE // the filter function with predicate PREDICATE || FUNCTION FUNCTION // \f g s. f (g s) || FUNCTION | FUNCTION // \f g s. { p in P | p in f(s) \/ p in g(s) } || FUNCTION & FUNCTION // \f g s. { p in P | p in f(s) /\ p in g(s) } || FUNCTION - FUNCTION // \f g s. { p in P | p in f(s) /\ ~p in g(s) } || FUNCTION? // \f. Identity | f || FUNCTION* // \f. Identity | f | f f | f f f | ... || FUNCTION+ // \f. f | f f | f f f | ... || Identity // \s. s || Requires // \s. { p in P | ?q in s. q requires p } || RequiredBy // \s. { p in P | ?q in s. p requires q } || Includes // \s. { p in P | ?q in s. q includes p } || IncludedBy // \s. { p in P | ?q in s. p includes q } || Subtheories // \s. { p in P | ?q in s. p is a subtheory of q } || SubtheoryOf // \s. { p in P | ?q in s. q is a subtheory of p } || Versions // \s. { p in P | ?q in s. p is a version of q } || Latest // \s. { p in s | ~?q in s. q is a later version of p } || Deprecated // (Identity - Latest) (Requires | Includes)* || Obsolete // All - (Requires | Includes)* || Upgradable // EarlierThanRepo || Uploadable // Mine /\ ~OnRepo /\ ~EarlierThanRepo /\ ConsistentWithRepo PREDICATE // represents a predicate with type P -> bool <- PREDICATE \/ PREDICATE // \f g p. f(p) \/ g(p) || PREDICATE /\ PREDICATE // \f g p. f(p) /\ g(p) || ~PREDICATE // \f p. ~f(p) || Empty // does the package have an empty theory (i.e., main {})? || Mine // does the package author match a name in the config file? || Closed // are all the required theories installed? || Acyclic // is the required theory graph free of cycles? || WellFounded // are all assumptions satisfied and inputs grounded? || OnRepo // is there a theory package with the same name on the repo? || IdenticalOnRepo // is this exact same theory package on the repo? || ConsistentWithRepo // are all the included packages consistent with the repo? || EarlierThanRepo // is there a later version of this ackage on the repo? || LaterThanRepo // is this package later than all versions on the repo? SET // represents a set with type S <- All // P || None // {} || NAME // \n. Latest { p in P | p has name n } || NAME-VERSION // \n v. { p in P | p has name n and version v } NAME is any package name (e.g., base). VERSION is any package version (e.g., 1.0). FILE is any filename; use - to read from stdin or write to stdout. FORMAT is any string containing {NAME,VERSION,DESCRIPTION,CHECKSUM,EMPTY}. DIR is any directory on the file system. REPO is the name of any repo in the config file (e.g., gilith). <div class="HOEnZb"><div class="h5"> _______________________________________________ opentheory-users mailing list <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> <a href="http://www.gilith.com/mailman/listinfo/opentheory-users" target="_blank">http://www.gilith.com/mailman/listinfo/opentheory-users</a> </div></div></blockquote></div>