[opentheory-users] reading articles from standard input

[Ramana Kumar]

On Mon, Oct 1, 2012 at 5:32 AM, Joe Leslie-Hurd <joe at gilith.com> wrote:

> 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,


Thanks!

I had packaged the tool for Arch Linux (and derivatives) here, when 1.2
first came out:
  https://aur.archlinux.org/packages.php?ID=61879

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


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

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


>
> 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).
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20121002/02a76c7e/attachment.htm>