parts and with X=$DEKTOP to remove the desktop specific parts.
define the binary name => less dups required
@SDESKTOP@
@EDESKTOP@
@SSERVER@
@ESERVER@
\*(BN
[-v[level]] [-q] [-V] [-h] [-F] [-G]
@SDESKTOP@
[-g] [-u]
@EDESKTOP@
[-I] [-p] [-s] [-l logic] [-y ser] [-L dirs]
[-m file] [-x] [-X] [-c host:port] [-S port]
[-C urls] [-i itype] [-d string] [-e enc]
[-O dir] [-o otypes] [-U file] [-R] [-A] [-N]
[-n specs] [-w views] [-t trans] [-a analysis]
[-M] file...
Hets is a parsing, static analysis and proof management tool combining various tools for different specification languages, thus providing a tool for the heterogeneous specification language HetCASL. The structuring constructs of this language are those of CASL, plus some new heterogeneous constructs for indicating the language and for language translations. Hence, Hets is based on a graph of logics and languages.
Hets is available as a desktop as well as a server variant. The server variant named hets-server is the same as the desktop variant named hets, but without GUI support and thus has no dependencies to GUI toolkits like Tcl/Tk or Gnome.
-v[level], --verbose[=level] Set the verbosity to level. Allowed is 0..5, default is 1. A good warning level is 2 that also shows read and written files.
-q , --quiet Same as -v0, no output is sent to stdout.
-V , --version Print version details and exits.
-h , --help , --usage Print help information and exit.
-F , --file-type Display file type, only.
-G , --logic-graph Show the logic graph as xml.
@SDESKTOP@
-g , --gui Show the development graph in a GUI window. Without this (and the -I) option hets will run in batch mode and process (aka analyse) all input files.
-u , --uncolored Use no colors in shown graphs.
@EDESKTOP@
-I , --interactive Run hets in interactive mode expecting input from the console after
all input files given as arguments have been processed.
@SDESKTOP@
If also the option -g is given a graph may pop up only after input has been
terminated using Ctrl-D.
@EDESKTOP@
-p , --just-parse Skip static analysis, just parse input files.
-s , --just-structured Skip basic i.e. logic specific analysis, just parse input files and do structured analysis.
-l logic, --logic=logic Select the given logic as the initial logic for processing the specifications if it is not given in source files. The default is CASL.
-y ser, --serialization=ser Use the given logic syntax ser.
-L dirlist, --hets-libdirs=dirlist Set the specification library directories to dirlist. dirlist is a single or more directories separated by a colon (equivalent to HETS LIB).
-m file, --modelSparQ=file Sets the lisp file for SparQ definitions to file (works for CASL only).
-x , --xml Uses xml packages (rather than plain text) to communicate.
-X , --server Start hets as web-server.
-c host:port, --connect=host:port Runs the interface with the -I option by communicating via a connection to the given host and port.
-S port, --listen=port Runs the interface with the -I option by listening to the given port.
-C urls, --url-catalog=urls A comma-separated list of URL pairs, whereby each pair denotes srcURL=tarURL.
-i itype, --input-type=itype Set the input type to expect explicitly to itype. The following input types are allowed: casl , het , dol , omn , owl , rdf , obo , ttl , hs , exp , maude , elf , hol , isa , thy , prf , omdoc , hpf , clf , clif , xml , fcstd , xmi , qvt , tptp , [tree.]gen_trm[.baf]. By default env, casl, or het are tried in this order.
-d string, --dump=string Dump internal data depending on the given string.
-e encoding, --encoding=encoding Use the given encoding for input and output file handling. Allowed are latin1 (default) or utf8\fb.
-O dir, --output-dir=DIR Set the destination directory for output files to dir.
-o otypes, --output-types=otypes Set the list of output types to otypes (default is an empty list). The list may contain one or more output file types separated by a comma. Known output types are: prf , env , omn , owl , rdf , obo , ttl , nt , clif , kif , omdoc , xml , json , exp , hs , thy , comptable.xml , fcxml , sym.xml , syms.xml , (sig|th)[.delta], pp.(het|tex|xml|html), pp.(stripped.het|labelled.tex), graph.(exp.dot|dot), dfg [ .c ] , tptp [ .c ] .
-U file, --xupdate=file Apply additional updates from the given file to a graph.
-R , --recursive Produce output files (given via -o) also for imported libraries.
-A , --apply-automatic-rule Apply automatic strategy tzo the development graph right after static analysis.
-N , --normal-form Compute all normal forms for nodes with incoming hiding links. This takes a long time.
-n specs, --named-specs=specs Create certain output files only for the given specs, which is comma-separated list of named specs.
-w views, --view=views Process the given views, which is a list of comma-separated SIMPLE-IDs.
-t trans, --translation=trans Translate all specifications (or those listed using the above -n option) using trans, which is a comma-separated list of one or more comorphism names.
-a analysis, --casl-amalg=analysis Set the CASL amalgamability options to analysis, which is a comma-separated list of one or more of the following options: none, sharing, cell (default), or colimit-thinness. If the list is empty the amalgamability analysis for CASL gets skipped.
-M , --MMT Use MMT.
@EDESKTOP@
@SSERVER@
@ESERVER@
In the following examples ${HETS_LIB} denotes the directory containing the hets specification and it is assumed, that the current working directory is writable, e.g. /tmp/.
\*(CL -A ${HETS_LIB}/Calculi/Space/RCCVerification.het
Check if all nodes can be proven. Only one node is heterogeneous and needs the Isabelle prover. To allow hets the reuse of the given proofs, copy the file ${HETS_LIB}/RCCVerification_RCC_FO_in_MetricSpace__T.thy to your working directory.
\*(CL ${HETS_LIB}/Basic/LinearAlgebra_II.casl
Check Edit/Prove/Automatic, followed by Edit/Undo.
\*(CL -i owl ${HETS_OWL_TOOLS}/tests/wine.rdf
Check out the OWL parser.
\*(CL ${HETS_LIB}/TestSuite/Conservative/Nat.casl
Check conservativity of the link. This will result in "The link is mono".
\*(CL ${HETS_LIB}/Ontology/Examples/Family.het
Check OWL conservativity checker on the Family <-> FamilyBase links. One can be proven, while the other cannot.
\*(CL -A ${HETS_LIB}/HidingOWL.het
Choose Edit/Consistency Checker and prove the goals.
\*(CL ${HETS_LIB}/HolLight/example_binom.hol
Import the full HolLight theory and a small lemma on binomials. You can use the translation to Isabelle.
Hets uses the following environment variables to determine the path to the
tools it needs. Relative pathes mentioned below should be absolute pathes,
so depending on the install directory, you need to add the corresponding
prefix like /usr/ or /local/usr/ .
looks not so good, when aligned.
HETS_MAGIC The magic file used by hets via the GNU file utility to determine the content type of files to process. Default: lib/hets/hets.magic
HETS_LIB The path to het's own libraries. Default: lib/hets/hets-lib
HETS_ISABELLE_LIB The path to the Isabelle library. Default: ${HETS_LIB}/Isabelle
HETS_HOLLIGHT_TOOLS The path to the HolLight image.a Default: lib/hets/hets-hollight-tools
HETS_MAUDE_LIB The path to the Maude Hets library. Default: lib/hets/hets-maude-lib
HETS_OWL_TOOLS The path to the hets owl tools library. Default: lib/hets/hets-owl-tools
HETS_APROVE The path to AProVE.jar . Default: ${HETS_OWL_TOOLS}/AProVE.jar
HETS_ONTODMU The path to OntoDMU.jar . Default: ${HETS_OWL_TOOLS}/OntoDMU.jar
HETS_JNI_LIBS The directory path which contains the FaCT++ JNI library libFaCTPlusPlusJNI.so. Default: ${HETS_OWL_TOOLS}/lib/native/`uname -m`
HETS_GMOC The path to the Gmoc directory containing bin/gmoc and Configuration.xml
HETS_REDUCE The path to the executable redcsl.
PELLET_PATH The path to the Pellet root directory. Default: share/pellet
TWELF_LIB The path to the TWELF root directory. Default: share/twelf/bin
MAUDE_LIB The path to the MAUDE library directory. Default: share/maude .da
Some tools used by hets under the hood require java(1), the GNU file
utility (on Solaris named gfile(1)) and openssl(1openssl).
Make sure that your PATH environment variable is set properly,
so that they can be find/called just by their basename.
@SSOLARIS@
@SSERVER@
The hets server service is managed by the service management facility, smf(5), under the service identifier:
It gets not automatically enabled on install. Administrative actions on this service, such as enabling, disabling, or requesting restart, can be performed using svcadm(1M). The service's status can be queried using the svcs(1) command.
Per default the server listens on port 800. If you wanna change it or wanna
change related environments variables, use svccfg(1M) to adjust them as
usual.
@ESERVER@
@ESOLARIS@
hets, the Heterogenous Tool Set is the work of University of Bremen and the Otto-von-Guericke University Magdeburg. This manual page was initially written by Corneliu-Claudiu Prodescu <cprodescu@googlemail.com> and uses the same license as hets itself. The complete user guide can be found beneath the install directory at share/doc/hets/UserGuide.pdf.
Please report any bugs to hets-devel@informatik.uni-bremen.de or via https://github.com/spechub/Hets/issues/.