hets -update
hets -revert
-update this switch doesn't start hets, but instead updates the entire application. First available packages are checked, then latest builds of the hets binary, as well as the latest version of the hets-library. This requires root access.
-revert this switch is used to revert to the previous version, once hets -update was used. Notice that only the Hets binary is reverted. This requires root access.
-v[0-5], --verbose[=0-5] sets the verbosity level, default is -v1. A good warning level is -v2 that also shows read and written files.
-q, --quiet same as -v0, no output is sent to stdout.
-V, --version prints version details and exits.
-h, --help, --usage prints help information and exits.
-g, --gui starts the graphical user interface to show graphs. Without this (and the -I) option hets will run in batch mode and process (aka analyse) all input files.
-u, --uncolored uses no colors in shown graphs.
-I, --interactive runs hets in interactive mode expecting input from the console after all input files given as arguments have been processed. If also the option -g is given a graph may pop up only after input has been terminated using Ctrl-D.
-p, --just-parse skips static analysis, just parses input files.
-s, --just-structured skips basic i.e. logic specific analysis, just does structured analysis.
-l LOGIC, --logic=LOGIC selects a logic if it is not given in source files, the default is CASL.
-L DIR, --hets-libdirs=DIR manually sets the path to the library source directories. Use a colon separated paths for multiple directories.
-m FILE, --modelSparQ=FILE sets lisp file for SparQ definitions (works for CASL only).
-x, --xml uses xml packages (rather than plain text) to communicate.
-X, --server start hets as web-server
-c HOSTNAME:PORT, --connect=HOSTNAME:PORT runs the interface with the -I option by comunicating via a connection to the port.
-s PORT, --listen=PORT runs the interface with the -I option by listening to the port
-i ITYPE, --input-type=ITYPE manually sets the input type. Input file types can be one of: casl, het, owl, hs, maude, elf, prf, omdoc, hpf, clf.
-d STRING, --dump=STRING dump internal data depending on STRING.
-e ENCODING, --encoding=ENCODING uses latin1 (default) or utf8 encoding for input and output files.
-O DIR, --output-dir=DIR manually sets the destination directory for output files.
-o OTYPES, --output-types=OTYPES sets the output types, default is nothing. Output file types can be one (or more) of prf, env, owl, omdoc, xml, exp, hs, thy, comptable.xml, (sig|th)[.delta], pp.(het|tex|xml), graph.(exp.dot|dot), dfg[.c], tptp[.c]. (Use a comma-separated list without blanks.)
-R, --recursive produces output files (given via -o) also for imported libraries
-A, --apply-automatic-rule applies automatic dev-graph strategy directly after static analysis.
-N, --normal-form computes normal forms. This takes a long time.
-n NSPECS, --named-specs=NSPECS Create certain output files only for the given named specs given as comma-separated list without blanks.
-t TRANS, --translation=TRANS translates all specifications (or those listed using the above -n option) by the translation given as composition via a colon-separated list without blanks.
-a ANALYSIS, --casl-amalg=ANALYSIS sets the CASL amalgamability options. The ANALYSIS can be one (or more) from none, sharing, cell, or colimit-thinness as comma-separated list without blanks.
HETS_LIB defines paths to the hets libraries.
HETS_OWL_TOOLS defines the path to the hets owl tools library.
HETS_ISABELLE_LIB defines the path to the Isabelle library.
HETS_MAUDE_LIB defines the path to the Maude Hets library
HETS_GMOC defines the path to the Gmoc directory containing bin/gmoc and Configuration.xml
HETS_REDUCE defines the path to the executable redcsl
HETS_APROVE defines the path to AProVE.jar
HETS_ONTODMU defines the path to OntoDMU.jar
HETS_JNI_LIBS defines the path to the FaCT++JNI library directory if it is not /lib
PELLET_PATH defines the path to the Pellet root directory.
TWELF_LIB defines the path to the TWELF root directory.
MAUDE_LIB defines the path to the MAUDE library directory.
HETS_HOLLIGHT_TOOLS defines the path to the HolLight image.
Some of these variables are set inside the script /usr/bin/hets
hets -g -A /usr/lib/hets/hets-lib/Calculi/Space/RCCVerification.het Check if all nodes can be proven. Only one node is heterogeneous and needs the Isabelle prover. Copy the file /usr/lib/hets/hets-lib/RCCVerification_RCC_FO_in_MetricSpace_T.thy to your working directory (with write access) to allow hets to reuse the given proofs.
hets -g /usr/lib/hets/hets-lib/Basic/LinearAlgebra_II.casl Check Edit/Prove/Automatic, followed by Edit/Undo.
hets -g -i owl /usr/lib/hets/hets-owl-tools/tests/wine.rdf Check out the OWL parser.
hets -g /usr/lib/hets/hets-lib/TestSuite/Conservative/Nat.casl Check conservativity of the link. This will result in "The link is mono".
hets -g /usr/lib/hets/hets-lib/Ontology/Examples/Family.het Check OWL conservativity checker on the Family <-> FamilyBase links. One can be proven, while the other cannot.
hets -g -A /usr/lib/hets/hets-lib/HidingOWL.het Choose Edit/Consistency Checker and prove the goals.
hets -g /usr/lib/hets/hets-lib/HolLight/example_binom.hol Import the full HolLight theory and a small lemma on binomials. You can use the translation to Isabelle.
For bugs report at hets-devel@mailhost.informatik.uni-bremen.de or use the trac http://trac.informatik.uni-bremen.de:8080/hets