]> matita.cs.unibo.it Git - helm.git/commit
maxipatch for support of multiple DBs.
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 6 Jul 2007 14:49:47 +0000 (14:49 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 6 Jul 2007 14:49:47 +0000 (14:49 +0000)
commitbb9aa02b52977c05fe678a4e15bfc64e27c2c5f5
tree9cf05826d2933b6f9c52c5303ea8e8eada0d6c63
parent1775c4a3db08d048840d8d47e4f22899c3735544
maxipatch for support of multiple DBs.

new 3 different kind of BD can coexist:
user) the user db, where his stuff is stored
   tables are named foo_user
library) the library db, a read only database where the standard library should be
   installed and that is the target of the publish act
legacy) a legacy database (not mandatory) where really read only data is stored

every db can be implement with an sqlite file or a mysql database.

the default configuration file sets 1 and 2 to be the mysql matita database on mowgli,
thus nothing should change for mowgli users. database 3 is not used if you are on mowgli.

the way it should be used by matita users out of the unibo network is commented in the config file:
1) file://~/.matita/user.db for his development
2) file:///usr/share/matita/metadata.db for the matita precompiled standard library
3) mysql://mowgli.cs.unibo.it for the legacy coq stuff, both queries and xml are fetched trough
   the net

this allows us to really distribute matita in a rather sane way, with a
precompiled library visible systemwide and having all per user data and
metadata in ~/.matita. There is no need for the user to install and configure
mysql, and can use mowgli just decommenting few lines in the config file.
64 files changed:
components/binaries/extractor/Makefile
components/binaries/extractor/extractor.conf.xml
components/binaries/extractor/extractor.ml
components/binaries/extractor/extractor_manager.ml
components/binaries/table_creator/table_creator.ml
components/cic/.depend
components/cic/cicUtil.ml
components/cic_proof_checking/cicEnvironment.ml
components/getter/http_getter.ml
components/getter/http_getter.mli
components/getter/http_getter_storage.ml
components/getter/http_getter_storage.mli
components/grafite_engine/grafiteEngine.ml
components/hmysql/.depend
components/hmysql/Makefile
components/hmysql/hMysql.ml
components/hmysql/hSql.ml [changed from symlink to file mode: 0644]
components/hmysql/hSql.mli
components/hmysql/hSqlite3.ml
components/lexicon/lexiconEngine.ml
components/lexicon/lexiconEngine.mli
components/library/.depend
components/library/.depend.opt
components/library/Makefile
components/library/libraryClean.ml
components/library/libraryDb.ml
components/library/libraryDb.mli
components/library/libraryMisc.ml
components/library/libraryMisc.mli
components/library/libraryNoDb.ml [deleted file]
components/library/libraryNoDb.mli [deleted file]
components/library/librarySync.ml
components/metadata/metadataConstraints.ml
components/metadata/metadataConstraints.mli
components/metadata/metadataDb.ml
components/metadata/metadataDeps.ml
components/metadata/sqlStatements.ml
components/metadata/sqlStatements.mli
components/tactics/.depend
components/tactics/closeCoercionGraph.ml
components/tactics/tactics.mli
components/whelp/fwdQueries.ml
components/whelp/whelp.ml
configure.ac
daemons/http_getter/main.ml
daemons/whelp/searchEngine.ml
matita/.depend
matita/.depend.opt
matita/Makefile
matita/help/C/matita.xml
matita/library/nat/div_and_mod_new.ma [deleted file]
matita/library/nat/div_and_mod_new.ma.dontcompile [new file with mode: 0644]
matita/matita.conf.xml.in
matita/matitaGui.ml
matita/matitaInit.ml
matita/matitaMathView.ml
matita/matitaScript.ml
matita/matitaWiki.ml
matita/matitacLib.ml
matita/matitadep.ml
matita/matitamakeLib.ml
matita/matitaprover.ml
matita/scripts/clean_db.sh [new file with mode: 0755]
pkg-matita/tarballs/matita-0.1.0.tar.gz