From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 3 Jan 2023 21:19:15 +0000 (+0100)
Subject: METAS removed + matita.conf.xml committed
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=3965019212f05fd879e97ed6969b39aa5a26118b

METAS removed + matita.conf.xml committed
---

diff --git a/.gitignore b/.gitignore
index d2e1e23e5..05efd6e7a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -13,17 +13,8 @@ _build
 *.native
 *.byte
 
-matita/Makefile.defs
-matita/autom4te.cache
-matita/components/METAS/META*
-matita/config.log
-matita/configure
-
 matita/components/extlib/componentsConf.ml
-matita/matita/matita.conf.xml
 matita/matita/matita.glade.utf8
-matita/depend-stamp
-matita/config.status
 
 matita/matita/help/C/pdf-stamp
 matita/matita/help/C/html-stamp
diff --git a/matita/components/METAS/meta.helm-content.src b/matita/components/METAS/meta.helm-content.src
deleted file mode 100644
index 6973a54d9..000000000
--- a/matita/components/METAS/meta.helm-content.src
+++ /dev/null
@@ -1,4 +0,0 @@
-requires="helm-library helm-ng_kernel"
-version="0.0.1"
-archive(byte)="content.cma"
-archive(native)="content.cmxa"
diff --git a/matita/components/METAS/meta.helm-content_pres.src b/matita/components/METAS/meta.helm-content_pres.src
deleted file mode 100644
index 0e361298e..000000000
--- a/matita/components/METAS/meta.helm-content_pres.src
+++ /dev/null
@@ -1,4 +0,0 @@
-requires="helm-content helm-syntax_extensions camlp5.gramlib ulex-camlp5 helm-grafite"
-version="0.0.1"
-archive(byte)="content_pres.cma"
-archive(native)="content_pres.cmxa"
diff --git a/matita/components/METAS/meta.helm-disambiguation.src b/matita/components/METAS/meta.helm-disambiguation.src
deleted file mode 100644
index 6c286ea71..000000000
--- a/matita/components/METAS/meta.helm-disambiguation.src
+++ /dev/null
@@ -1,4 +0,0 @@
-requires="helm-content"
-version="0.0.1"
-archive(byte)="disambiguation.cma"
-archive(native)="disambiguation.cmxa"
diff --git a/matita/components/METAS/meta.helm-extlib.src b/matita/components/METAS/meta.helm-extlib.src
deleted file mode 100644
index a355cb2da..000000000
--- a/matita/components/METAS/meta.helm-extlib.src
+++ /dev/null
@@ -1,5 +0,0 @@
-requires="str unix camlp5.gramlib"
-version="0.0.1"
-archive(byte)="extlib.cma"
-archive(native)="extlib.cmxa"
-linkopts=""
diff --git a/matita/components/METAS/meta.helm-getter.src b/matita/components/METAS/meta.helm-getter.src
deleted file mode 100644
index b060fb62a..000000000
--- a/matita/components/METAS/meta.helm-getter.src
+++ /dev/null
@@ -1,5 +0,0 @@
-requires="http unix pcre zip helm-xml helm-logger helm-ng_kernel helm-registry"
-version="0.0.1"
-archive(byte)="getter.cma"
-archive(native)="getter.cmxa"
-linkopts=""
diff --git a/matita/components/METAS/meta.helm-grafite.src b/matita/components/METAS/meta.helm-grafite.src
deleted file mode 100644
index f86ae35e7..000000000
--- a/matita/components/METAS/meta.helm-grafite.src
+++ /dev/null
@@ -1,4 +0,0 @@
-requires="helm-content helm-ng_kernel"
-version="0.0.1"
-archive(byte)="grafite.cma"
-archive(native)="grafite.cmxa"
diff --git a/matita/components/METAS/meta.helm-grafite_engine.src b/matita/components/METAS/meta.helm-grafite_engine.src
deleted file mode 100644
index edea1b3ac..000000000
--- a/matita/components/METAS/meta.helm-grafite_engine.src
+++ /dev/null
@@ -1,5 +0,0 @@
-requires="helm-grafite_parser helm-ng_tactics helm-ng_extraction"
-version="0.0.1"
-archive(byte)="grafite_engine.cma"
-archive(native)="grafite_engine.cmxa"
-linkopts=""
diff --git a/matita/components/METAS/meta.helm-grafite_parser.src b/matita/components/METAS/meta.helm-grafite_parser.src
deleted file mode 100644
index c415c72b0..000000000
--- a/matita/components/METAS/meta.helm-grafite_parser.src
+++ /dev/null
@@ -1,5 +0,0 @@
-requires="helm-grafite ulex-camlp5 helm-ng_disambiguation helm-ng_library helm-content_pres"
-version="0.0.1"
-archive(byte)="grafite_parser.cma"
-archive(native)="grafite_parser.cmxa"
-linkopts=""
diff --git a/matita/components/METAS/meta.helm-library.src b/matita/components/METAS/meta.helm-library.src
deleted file mode 100644
index 2fd9b2917..000000000
--- a/matita/components/METAS/meta.helm-library.src
+++ /dev/null
@@ -1,5 +0,0 @@
-requires="helm-getter"
-version="0.0.1"
-archive(byte)="library.cma"
-archive(native)="library.cmxa"
-linkopts=""
diff --git a/matita/components/METAS/meta.helm-logger.src b/matita/components/METAS/meta.helm-logger.src
deleted file mode 100644
index 5b2e8d8ff..000000000
--- a/matita/components/METAS/meta.helm-logger.src
+++ /dev/null
@@ -1,5 +0,0 @@
-requires=""
-version="0.0.1"
-archive(byte)="logger.cma"
-archive(native)="logger.cmxa"
-linkopts=""
diff --git a/matita/components/METAS/meta.helm-ng_cic_content.src b/matita/components/METAS/meta.helm-ng_cic_content.src
deleted file mode 100644
index 1b45e784a..000000000
--- a/matita/components/METAS/meta.helm-ng_cic_content.src
+++ /dev/null
@@ -1,4 +0,0 @@
-requires="helm-library helm-ng_library helm-grafite helm-content helm-ng_refiner"
-version="0.0.1"
-archive(byte)="ng_cic_content.cma"
-archive(native)="ng_cic_content.cmxa"
diff --git a/matita/components/METAS/meta.helm-ng_disambiguation.src b/matita/components/METAS/meta.helm-ng_disambiguation.src
deleted file mode 100644
index 97a3c1346..000000000
--- a/matita/components/METAS/meta.helm-ng_disambiguation.src
+++ /dev/null
@@ -1,4 +0,0 @@
-requires="helm-ng_cic_content helm-ng_refiner helm-disambiguation"
-version="0.0.1"
-archive(byte)="ng_disambiguation.cma"
-archive(native)="ng_disambiguation.cmxa"
diff --git a/matita/components/METAS/meta.helm-ng_extraction.src b/matita/components/METAS/meta.helm-ng_extraction.src
deleted file mode 100644
index 16e86f1fc..000000000
--- a/matita/components/METAS/meta.helm-ng_extraction.src
+++ /dev/null
@@ -1,5 +0,0 @@
-requires="helm-ng_kernel helm-registry"
-version="0.0.1"
-archive(byte)="ng_extraction.cma"
-archive(native)="ng_extraction.cmxa"
-linkopts=""
diff --git a/matita/components/METAS/meta.helm-ng_kernel.src b/matita/components/METAS/meta.helm-ng_kernel.src
deleted file mode 100644
index f35420375..000000000
--- a/matita/components/METAS/meta.helm-ng_kernel.src
+++ /dev/null
@@ -1,5 +0,0 @@
-requires="helm-extlib"
-version="0.0.1"
-archive(byte)="ng_kernel.cma"
-archive(native)="ng_kernel.cmxa"
-linkopts=""
diff --git a/matita/components/METAS/meta.helm-ng_library.src b/matita/components/METAS/meta.helm-ng_library.src
deleted file mode 100644
index a40447075..000000000
--- a/matita/components/METAS/meta.helm-ng_library.src
+++ /dev/null
@@ -1,5 +0,0 @@
-requires="helm-ng_refiner helm-registry helm-library"
-version="0.0.1"
-archive(byte)="ng_library.cma"
-archive(native)="ng_library.cmxa"
-linkopts=""
diff --git a/matita/components/METAS/meta.helm-ng_paramodulation.src b/matita/components/METAS/meta.helm-ng_paramodulation.src
deleted file mode 100644
index 01d35b829..000000000
--- a/matita/components/METAS/meta.helm-ng_paramodulation.src
+++ /dev/null
@@ -1,5 +0,0 @@
-requires="helm-ng_refiner"
-version="0.0.1"
-archive(byte)="ng_paramodulation.cma hash.o"
-archive(native)="ng_paramodulation.cmxa hash.o"
-linkopts(byte)="-custom"
diff --git a/matita/components/METAS/meta.helm-ng_refiner.src b/matita/components/METAS/meta.helm-ng_refiner.src
deleted file mode 100644
index b866e9e56..000000000
--- a/matita/components/METAS/meta.helm-ng_refiner.src
+++ /dev/null
@@ -1,5 +0,0 @@
-requires="helm-ng_kernel"
-version="0.0.1"
-archive(byte)="ng_refiner.cma"
-archive(native)="ng_refiner.cmxa"
-linkopts=""
diff --git a/matita/components/METAS/meta.helm-ng_tactics.src b/matita/components/METAS/meta.helm-ng_tactics.src
deleted file mode 100644
index 130e39c3f..000000000
--- a/matita/components/METAS/meta.helm-ng_tactics.src
+++ /dev/null
@@ -1,4 +0,0 @@
-requires="helm-ng_disambiguation helm-ng_paramodulation"
-version="0.0.1"
-archive(byte)="ng_tactics.cma"
-archive(native)="ng_tactics.cmxa"
diff --git a/matita/components/METAS/meta.helm-registry.src b/matita/components/METAS/meta.helm-registry.src
deleted file mode 100644
index 82d364016..000000000
--- a/matita/components/METAS/meta.helm-registry.src
+++ /dev/null
@@ -1,4 +0,0 @@
-requires="str netstring helm-xml"
-version="0.0.1"
-archive(byte)="registry.cma"
-archive(native)="registry.cmxa"
diff --git a/matita/components/METAS/meta.helm-syntax_extensions.src b/matita/components/METAS/meta.helm-syntax_extensions.src
deleted file mode 100644
index 166bd498d..000000000
--- a/matita/components/METAS/meta.helm-syntax_extensions.src
+++ /dev/null
@@ -1,7 +0,0 @@
-requires="str"
-version="0.0.1"
-archive(byte)="syntax_extensions.cma"
-archive(native)="syntax_extensions.cmxa"
-requires(syntax,preprocessor)="camlp5"
-archive(syntax,preprocessor)="pa_extend.cmo pa_unicode_macro.cma profiling_macros.cma"
-linkopts=""
diff --git a/matita/components/METAS/meta.helm-thread.src b/matita/components/METAS/meta.helm-thread.src
deleted file mode 100644
index 8ee48782a..000000000
--- a/matita/components/METAS/meta.helm-thread.src
+++ /dev/null
@@ -1,7 +0,0 @@
-requires="str unix"
-version="0.0.1"
-archive(byte,mt)="thread.cma"
-archive(native,mt)="thread.cmxa"
-archive(byte)="thread_fake.cma"
-archive(native)="thread_fake.cmxa"
-linkopts=""
diff --git a/matita/components/METAS/meta.helm-xml.src b/matita/components/METAS/meta.helm-xml.src
deleted file mode 100644
index 5cde1bdb8..000000000
--- a/matita/components/METAS/meta.helm-xml.src
+++ /dev/null
@@ -1,5 +0,0 @@
-requires="zip expat helm-extlib camlp-streams"
-version="0.0.1"
-archive(byte)="xml.cma"
-archive(native)="xml.cmxa"
-linkopts=""
diff --git a/matita/matita/matita.conf.xml b/matita/matita/matita.conf.xml
new file mode 100644
index 000000000..431c3e0f0
--- /dev/null
+++ b/matita/matita/matita.conf.xml
@@ -0,0 +1,121 @@
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+  <section name="user">
+    <!-- User home directory. Here a ".matita" directory will be created
+    and used to store the part of the library developed by the user. -->
+    <key name="home">$(HOME)</key>
+    <!-- User name. It is used down in this configuration file.  If left
+    unspecified, name of the user executing matita will be used (as per
+    getent) -->
+    <key name="name">$(USER)</key>
+  </section>
+  <section name="matita">
+    <!-- Debug only. Stay away. -->
+    <!-- <key name="auto_disambiguation">true</key> -->
+    <!-- Debug only. Stay away. -->
+    <!-- <key name="environment_trust">true</key> -->
+    <key name="basedir">$(user.home)/.matita</key>
+    <!-- remove the old objects before putting the new ones -->
+    <key name="remove_old_objects">false</key>
+    <!-- Where support files are installed -->
+    <key name="rt_base_dir">/home/claudio/ricerca/matita5/helm/matita/matita</key>
+    <!-- Metadata owner. It will be used to create user-specific tables
+    in the SQL database. -->
+    <key name="owner">$(user.name)</key>
+    <!-- Initial GUI font size. -->
+    <!-- <key name="font_size">10</key> -->
+    <!--  Perform heavy checks when run interactively (like duplicate check) -->
+    <!-- <key name="do_heavy_checks">false</key> -->
+  </section>
+  <section name="db">
+    <!-- 
+    Every metadata key must have the following fields:
+      1) dbhost: a file:// or a mysql:// path
+      2) database name: use extension .db for file:// dbs
+      3) username
+      4) password: use 'none' for no password
+      5) dbtype: one of the following
+           'legacy' 
+              are read only dbs, used for the Coq/contribs stuff
+           'library' 
+	      is the standard library, becames writable in publish (-system)
+	      mode
+           'user' 
+              is the user own db (can be the same of marked as ro, tables
+              have different names and can coexist)
+
+    Note that:
+      exactly one 'user'    db must be specified
+      exactly one 'library' db can be specified
+      exactly one 'legacy'  db can  be specified
+    -->
+
+    <!-- The following snippet is used by the helm team
+         note that user's tables are named diffrently from library tables,
+	 so they can coexists on the same db -->
+
+    <key name="metadata">mysql://mowgli.cs.unibo.it matita helm none library</key>
+    <key name="metadata">mysql://mowgli.cs.unibo.it matita helm none user</key>
+
+    <!-- The following snippet it what you want to use a local sqlite db
+         and acess remotely to the coq library trought mowgli
+    <key name="metadata">mysql://mowgli.cs.unibo.it matita helm none legacy</key>
+    <key name="metadata">file://$(matita.rt_base_dir) metadata.db helm helm library</key>
+    <key name="metadata">file://$(matita.basedir) user.db helm helm user</key>
+    -->
+
+    <!-- 
+    If you have a large amount of metadata, you may be interested in using
+    MySql instead of Sqlite. The simplest way to create a MySql database is:
+      0) # become an user with database administration privileges
+      1) mysqladmin create matita
+      2) echo "grant all privileges on matita.* to helm;" | mysql matita
+      Note that this way the database will be open to anyone, apply
+      stricter permissions if needed.
+    -->
+  </section>
+  <section name="getter">
+    <!-- Cache dir for CIC XML documents downloaded from the net.
+    Beware that this dir may become really space-consuming. It wont be
+    used if all prefexises below are local (i.e. "file:///" URI scheme).
+    -->
+    <key name="cache_dir">$(matita.basedir)/getter/cache</key>
+    <!-- "Prefixes", i.e.: mappings URI -> URL of the global library
+    Each prefix mapps an URI of the cic:/ namespace to an URL where the
+    documents can actually be accessed. URL can be in the "file://" or
+    "http://" scheme. Only "file://" scheme can be used to store
+    documents created by the user.
+    Each prefix may be given a list of attributes. Currently supported
+    attributes are:
+    - "legacy" for parts of the library not generated by Matita (e.g.
+      exported from Coq)
+    - "ro" for parts of the library which are not writable by the user
+      (e.g. the Matita standard library)
+    "legacy" implies "ro"
+    -->
+    <key name="prefix">
+      cic:/matita/
+      file://$(matita.rt_base_dir)/xml/standard-library/
+      ro
+    </key>
+    <key name="prefix">
+      cic:/matita/
+      file://$(matita.basedir)/xml/matita/
+    </key>
+    <key name="prefix">
+      cic:/
+      file:///home/claudio/ricerca/matita5/helm/matita/matita/xml/legacy-library/coq/
+      legacy
+    </key>
+    <key name="prefix">
+      cic:/
+      file:///projects/helm/library/coq_contribs/
+      legacy
+    </key>
+    <key name="prefix">
+      cic:/
+      http://mowgli.cs.unibo.it/xml/
+      legacy
+    </key>
+  </section>
+</helm_registry>