[opentheory-users] reading articles from standard input

[Joe Leslie-Hurd]

Hi Ramana,

>> You can prefix an input with a type
> Is this documented anywhere?
> 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?

I've just released a version of the tool with much improved usage
documentation, 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.

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).