Readme.md revision a389e88e0acb83d8489bdc5e55bc5522b152bbec
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwThe database output of Hets is supposed to be used as part of [Ontohub](https://github.com/ontohub/ontohub-backend).
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwOntohub names some of the data type different from Hets.
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwThis document shows how the internal data types of Hets are mapped to the database.
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw# Mapping of Hets-internal data types to database types
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw| Hets-internal | Database |
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw| ------------- | ------------- |
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw| Logic | Language |
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw| sublogics | Logic |
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw| Syntax (IRI from `gTheorySyntax`) | Serialization |
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw| Comoprhism | LanguageMapping + LogicMapping |
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw| dependency relation of the LibEnv | Document, DocumentLink |
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw| (LibName, DGraph) | Document |
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw| Range | FileRange: The `[Pos]` list is broken down to the first and - if present - second element, interpreted as the beginning and end of the range. It is not saved at all if the list is empty. It is assumed that the path in all elements of the list is the same. |
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw| DGOrigin | OMSOrigin (enumeration type) |
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw| Conservativity | String (a table column, the `Unknown` constructor is mapped to the containing String) |
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw| ConsStatus | ConservativityStatus |
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw| (DGNodeLab, Node) | OMS |
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw| NodeName | part of OMS |
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw| G_theory | Split into Language, Logic, Signature, Serialization, Symbol, Sentence and associations between these |
dc20a3024900c47dd2ee44b9707e6df38f7d62a5as| G_sign | Signature + SignatureSymbol (association between Signature and Symbol, telling if a Symbol is imported) |
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw| GMorphism | SignatureMorphism + SymbolMapping |
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw| ExtSign sign symbol | Signature |
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw| symbol | Symbol |
8d96b23e24cf8db8618f698bfa580a25d7dc6029Alan Wright| Named sentence | Sentence: Axiom / OpenConjecture / CounterTheorem / Theorem |
8d96b23e24cf8db8618f698bfa580a25d7dc6029Alan Wright| (Node, Node, DGLinkLab) | Mapping |
8d96b23e24cf8db8618f698bfa580a25d7dc6029Alan Wright# Saving the data
8d96b23e24cf8db8618f698bfa580a25d7dc6029Alan WrightThe data is saved in transactions: If an error occurs during the process of saving, no data is written to the database.
dc20a3024900c47dd2ee44b9707e6df38f7d62a5as### Logic Graph
8d96b23e24cf8db8618f698bfa580a25d7dc6029Alan WrightThe logic graph is written in a separate command (`hets --logic-graph`).
8d96b23e24cf8db8618f698bfa580a25d7dc6029Alan WrightIt is assumed that no logics will be removed from Hets.
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwFuture logics will be inserted with every version of Hets, if the command is re-run on the same database.
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw### Development Graph
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwThe development graph is converted to the database types as shown in the table above.
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwWhile converting, a cache is held of all the Documents, Signatures, OMS, Sentences and Symbols that have already been processed to avoid duplicates.
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwIf a Document imports another Document, and the imported one is already present in the database, it is selected and its OMS are not saved again.
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwHowever, this sub-Document data is processed again to update the cache - only without inserting into the database.
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw# Parallelism
dc20a3024900c47dd2ee44b9707e6df38f7d62a5asTo allow for parallel analysis of Documents, mutexes are used on a PostgreSQL database ([advisory locks](https://www.postgresql.org/docs/10/static/explicit-locking.html)).
dc20a3024900c47dd2ee44b9707e6df38f7d62a5asSince Documents can be imported, finding and creating a Document must occur inside a mutex.
dc20a3024900c47dd2ee44b9707e6df38f7d62a5asThe key of this mutex is the location of the Document.
dc20a3024900c47dd2ee44b9707e6df38f7d62a5asDuring analysis of a Document, a Logic may need to be created because not all Logics are saved during the migration of the logic graph.
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwHence, finding and creating a Logic must occur inside a mutex that uses the same key as the logic graph migration.
8d96b23e24cf8db8618f698bfa580a25d7dc6029Alan Wright# Enumeration types
8d96b23e24cf8db8618f698bfa580a25d7dc6029Alan WrightPostgreSQL supports enumeration types which are used by Ontohub, but the SQL library of Hets, Persistent, does not support them at this point.
8d96b23e24cf8db8618f698bfa580a25d7dc6029Alan Wright[This fork of Persistent](https://github.com/eugenk/persistent/tree/add_support_for_postgresqls_enumerated_types) allows to use these on databases that do not need to be migrated by Hets.
8d96b23e24cf8db8618f698bfa580a25d7dc6029Alan WrightIt is a dependency of Hets that is easily built with Haskell-Stack by just using `make stack` and `make`.