]> matita.cs.unibo.it Git - helm.git/commit - helm/software/matita/scripts/clean_db.sh
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)
commit111df95ac03f2ee21dfa2422a7f531f675b1c16d
tree9acbdebdfc334b2c9de51767405ffb28df40f684
parent2ce7fd1b8d48f86d1f93231fe35473551cd060e7
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:
helm/software/components/binaries/extractor/Makefile
helm/software/components/binaries/extractor/extractor.conf.xml
helm/software/components/binaries/extractor/extractor.ml
helm/software/components/binaries/extractor/extractor_manager.ml
helm/software/components/binaries/table_creator/table_creator.ml
helm/software/components/cic/.depend
helm/software/components/cic/cicUtil.ml
helm/software/components/cic_proof_checking/cicEnvironment.ml
helm/software/components/getter/http_getter.ml
helm/software/components/getter/http_getter.mli
helm/software/components/getter/http_getter_storage.ml
helm/software/components/getter/http_getter_storage.mli
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/hmysql/.depend
helm/software/components/hmysql/Makefile
helm/software/components/hmysql/hMysql.ml
helm/software/components/hmysql/hSql.ml [changed from symlink to file mode: 0644]
helm/software/components/hmysql/hSql.mli
helm/software/components/hmysql/hSqlite3.ml
helm/software/components/lexicon/lexiconEngine.ml
helm/software/components/lexicon/lexiconEngine.mli
helm/software/components/library/.depend
helm/software/components/library/.depend.opt
helm/software/components/library/Makefile
helm/software/components/library/libraryClean.ml
helm/software/components/library/libraryDb.ml
helm/software/components/library/libraryDb.mli
helm/software/components/library/libraryMisc.ml
helm/software/components/library/libraryMisc.mli
helm/software/components/library/libraryNoDb.ml [deleted file]
helm/software/components/library/libraryNoDb.mli [deleted file]
helm/software/components/library/librarySync.ml
helm/software/components/metadata/metadataConstraints.ml
helm/software/components/metadata/metadataConstraints.mli
helm/software/components/metadata/metadataDb.ml
helm/software/components/metadata/metadataDeps.ml
helm/software/components/metadata/sqlStatements.ml
helm/software/components/metadata/sqlStatements.mli
helm/software/components/tactics/.depend
helm/software/components/tactics/closeCoercionGraph.ml
helm/software/components/tactics/tactics.mli
helm/software/components/whelp/fwdQueries.ml
helm/software/components/whelp/whelp.ml
helm/software/configure.ac
helm/software/daemons/http_getter/main.ml
helm/software/daemons/whelp/searchEngine.ml
helm/software/matita/.depend
helm/software/matita/.depend.opt
helm/software/matita/Makefile
helm/software/matita/help/C/matita.xml
helm/software/matita/library/nat/div_and_mod_new.ma [deleted file]
helm/software/matita/library/nat/div_and_mod_new.ma.dontcompile [new file with mode: 0644]
helm/software/matita/matita.conf.xml.in
helm/software/matita/matitaGui.ml
helm/software/matita/matitaInit.ml
helm/software/matita/matitaMathView.ml
helm/software/matita/matitaScript.ml
helm/software/matita/matitaWiki.ml
helm/software/matita/matitacLib.ml
helm/software/matita/matitadep.ml
helm/software/matita/matitamakeLib.ml
helm/software/matita/matitaprover.ml
helm/software/matita/scripts/clean_db.sh [new file with mode: 0755]
helm/software/pkg-matita/tarballs/matita-0.1.0.tar.gz