[WIP] 1691 dg calculus on database (#1752) * Add database dependencies. * first experimental version of DB interface - just store DG names * also write dg nodes to db * hints for further programming * Connect to PostgreSQL databases using a Rails database.yml. * Move the schema to an own module. * mapping of Hets datatypes to DB * more explanation on index maps * Save the LogicGraph and Development Graph in the database. * Add config option for DB file. * Move dbConfig into HetcatsOpts, move migrations into onDatabase. * Save errors to the database. * Associate the data with a given file version. * Fix saving independent documents, non-signature symbols and remove debug prints. * Remove theoryMap from DBCache. * Fix names of Loc/Ids. * Drop unneeded database columns. * Save SignatureMorphisms and SymbolMappings. Major refactoring in Persistence.DevGraph. * Handle Library and NativeDocument properly. * Rename Range to FileRange because of constraints in Ontohub. * Use PostgreSQL Enums. * Rename Warning to Warn because of constraints in Ontohub. * Use proper location as Loc/Id. * Include persistent-fork into Hets repository as a git submodule. * Find the FileVersion of an import and save the Document accordingly. * Add advisoryLocked function. * Ignore the _dependencies directory. * Only save a Document if it does not yet exist. * Lock language migration and document saving. * Use mutex, write logic graph in ins own command Write logic graph: Since both commands, DG analysis and LG output need to write Logics to the database, we need the same mutex kex for these two tasks. This splits the LG output into its own command to allow for multiple processes to write analysis data at once. * Get the submodule via https. * Add readme for the persistence layer. * Fix findFileVersion function. * Fix export warning. * Find a FileVersion at the current commit instead of the previous version. * Make the symbolKind part of a symbol's Loc/Id. * Make concatMapM more generic. * Correctly associate symbols along heterogeneous links. * Set evaluationState of FileVersion. * Allow to omit the --database-fileversion-id option. * Simplify the travis configuration. * Add database job to travis. * Find FileVersion of the last change. * Fix dependency relation order. * Add MySQL support. * Add restack target to Makefile. * Add option to disallow migrations That means, PostgreSQL can be used without Ontohub. * Remove unused import. * Update Stack release and use persistent-template of the fork. * Make the existing columns in the schema MySQL compatible. * Work-around migration errors caused by class table inheritance. * Use PostgreSQL and MySQL in travis. * Use better job labels in Travis. * Possibly fix travis. * Add SQLite to Travis. * Add installation instructions. * Add DGVerificationGeneric constructor. * Rename ConsStatus to ConservativityStatus. * Add error handling. * Fix symbol's fullName. * Set Logic name to Language Name when there is no Logic name. * Do not print migrations. * Fix key length for MySQL. * Add namespace to Loc/Ids. * Add option for re-analysis. * Add a testfile. * Improve error messages. * Create the freeness parameter OMS. * Add failing testfiles. * Remove code duplication. * Temporarily remove failing test files - until #1655 and #1597 have been solved. * Try longer locId in MySQL. * Fix mapping type. * Add default implementation of symbolKind. * Add Indexes. * Quiet down PostgreSQL on CREATE INDEX IF NOT EXISTS. * Add PostgreSQL 9.6 to addons. * Allow Hets-database to run without ontohub. * Reduce column size for MySQL. * Move the database-specific dependencies into their own module. * Upgrade persistent (rebase on master). * Minimise the module exports on Database. * Upgrade stack.yml to new stack version. * Fix SQLite module. * WIP: Try System.Plugins. * Remove System.Plugins again. * Deactivate MySQL. * Remove System.Plugins from the dependencies. * Finalise db_mapping.txt * Update readme. * Don't use PostgreSQL for hets-desktop. * Use hets_server in Travis/PostgreSQL job. * Add PostgreSQL as a dependency to the server package. * Update some documentation. * Fix runtime dependencies. * Describe main db options in the UserGuide. * Add libpq5 to debian dependencies. * Clean the database.yml files and link them from the UserGuide.

Add macOS caches to gitignore.

Complete TPTP support (#1707) * Add option to print the AST in XML/JSON output. Turn it off by default. * Add abstract syntax of TPTP. * Add parens and brackets to Common.Lexer. * Add TPTP Parser. * Add TPTP Sign. * Add TPTP Morphism. * Add TPTP StaticAnalysis. * Fix IRI character parsing. * Add TPTP Pretty. * Add TPTP Logic. * Map the tptp and p file extension to the TPTP logic for input. * Add LibDefn parser for TPTP. * Write TPTP output. * Add EProver to TPTP. * Add TPTP Sublogics. * Add SPASS prover to TPTP. * Add Vampire prover to TPTP. * Add Darwin prover to TPTP. * Add Leo-II prover to TPTP. * Add Geo-III prover to TPTP - It does not support a timeout. * Add CVC4 prover to TPTP. * Add Isabelle prover to TPTP. * Make IRI compatible with TPTP library file names. * Revert "fail if names of sentences appear as names of symbols #1630" This is a combination of 3 commits: * Revert "check that the Result has no errors" This reverts commit 9542b929f3cfabf1491c3f0489acf92ba703968f. * Revert "better error message" This reverts commit a7ea46d4c76b11735234092d0a50efcbc56f9642. * Revert "fail if names of sentences appear as names of symbols" This reverts commit 2487bae09bf3aabc7085880aee616648fe5ca241. * Fix usage of magic file There were other (system) magic files invoked as well with a higher priority. Using the MAGIC environment variable instead of the argument --magic-file overrides this behaviour and only uses the specified magic file. * Fix magic file The escaping of "@" and "(" is not needed. The escaping of a trailing space in clif is needed. * Add TPTP to magic file. * Add Satallax prover to TPTP. * Properly check for http[s] URIs. * Allow file:// in libdirs. * Allow only one http[s] libdir - Parse the port correctly. * Fix all remaining parsing problems. * Move functions to debug the parser to a separate module. * Get rid of all TPTP related compiler warnings. * Move the type 'Morphism' to 'TPTP.Morphism'. * Rename: TPTP/Logic.hs -> TPTP/Logic_TPTP.hs * Implement all_sublogics. * Recognise negated_conjecture as a proof obligation.

Ignore stack file. (#1726)

Introduce semantic versioning (#1716) * Put the version into Driver/Version.hs. * Fix version strings. * Add --numeric-version option. * Adjust HETS_VERSION in Makefile. * Remove rev.txt. * get fully rid of GIT_TIMESTAMP + minor simplifications * Rename function hetcats_version to hets_version. * Use camelCase.

Replace system-ghc with haskell-stack.

remove unsused/generated files; update .gitignore

Makefile cleanup/fixes + new install* features

adjusted initialize_java

also ignore QVTR generated files

ignore emacs backup files

also ignore files generated by java/ant

ignore files created by ghc-7.8

added new files to .gitignore git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18254 cec4b9c1-7d33-0410-9eda-942365e851bb

removed generated files git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17969 cec4b9c1-7d33-0410-9eda-942365e851bb

removed generated files git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17962 cec4b9c1-7d33-0410-9eda-942365e851bb

removed leading spaces in new .gitignore git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17959 cec4b9c1-7d33-0410-9eda-942365e851bb

improved .gitignore git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17958 cec4b9c1-7d33-0410-9eda-942365e851bb

added THF/As.hs to .gitignore file git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17825 cec4b9c1-7d33-0410-9eda-942365e851bb

new files for .gitignore git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16986 cec4b9c1-7d33-0410-9eda-942365e851bb

Added new files to .gitignore git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16901 cec4b9c1-7d33-0410-9eda-942365e851bb

ignore file for git git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@16729 cec4b9c1-7d33-0410-9eda-942365e851bb