From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 3 Dec 2005 10:35:10 +0000 (+0000)
Subject: 1. metadata are no longer stored in .moo files.
X-Git-Tag: make_still_working~8055
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dbb9f64a437b4abda0b9f47a527ab6135d596e28;p=helm.git

1. metadata are no longer stored in .moo files.
   They are now stored (and retrieved) in .metadata files if -nodb is set.
   In this way the "library" library no longer depends on "content_pres"
2. removed files in grafite_parser that were commited by mistake
---

diff --git a/helm/ocaml/METAS/meta.helm-grafite2.src b/helm/ocaml/METAS/meta.helm-grafite2.src
index c6603db5c..058167e4a 100644
--- a/helm/ocaml/METAS/meta.helm-grafite2.src
+++ b/helm/ocaml/METAS/meta.helm-grafite2.src
@@ -1,4 +1,4 @@
-requires="helm-library helm-tactics helm-cic_disambiguation"
+requires="helm-library helm-grafite helm-tactics helm-cic_disambiguation"
 version="0.0.1"
 archive(byte)="grafite2.cma"
 archive(native)="grafite2.cmxa"
diff --git a/helm/ocaml/METAS/meta.helm-library.src b/helm/ocaml/METAS/meta.helm-library.src
index 366269cf9..d4955e05d 100644
--- a/helm/ocaml/METAS/meta.helm-library.src
+++ b/helm/ocaml/METAS/meta.helm-library.src
@@ -1,4 +1,4 @@
-requires="helm-grafite helm-metadata"
+requires="helm-cic_acic helm-metadata"
 version="0.0.1"
 archive(byte)="library.cma"
 archive(native)="library.cmxa"
diff --git a/helm/ocaml/grafite/grafiteAst.ml b/helm/ocaml/grafite/grafiteAst.ml
index a7b0f3eea..3d176fbe5 100644
--- a/helm/ocaml/grafite/grafiteAst.ml
+++ b/helm/ocaml/grafite/grafiteAst.ml
@@ -112,14 +112,6 @@ type alias_spec =
   | Symbol_alias of string * int * string (* name, instance no, description *)
   | Number_alias of int * string          (* instance no, description *)
 
-type metadata =
-  | Dependency of string  (* baseuri without trailing slash *)
-  | Baseuri of string 
-
-let compare_metadata = Pervasives.compare
-
-let eq_metadata = (=)
-
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
 let magic = 4
@@ -145,8 +137,6 @@ type ('term,'obj) command =
         CicNotationPt.cic_appl_pattern
       (* description (i.e. id), symbol, arg pattern, appl pattern *)
 
-  | Metadata of loc * metadata
-
     (* DEBUGGING *)
   | Dump of loc (* dump grammar on stdout *)
     (* DEBUGGING *)
@@ -155,26 +145,6 @@ type ('term,'obj) command =
 (* composed magic: term + command magics. No need to change this value *)
 let magic = magic + 10000 * CicNotationPt.magic
 
-let reash_cmd_uris =
-  let reash_uri uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in
-  function
-  | Default (loc, name, uris) ->
-      let uris = List.map reash_uri uris in
-      Default (loc, name, uris)
-  | Interpretation (loc, dsc, args, cic_appl_pattern) ->
-      let rec aux =
-        function
-        | CicNotationPt.UriPattern uri ->
-            CicNotationPt.UriPattern (reash_uri uri)
-        | CicNotationPt.ApplPattern args ->
-            CicNotationPt.ApplPattern (List.map aux args)
-        | CicNotationPt.VarPattern _
-        | CicNotationPt.ImplicitPattern as pat -> pat
-      in
-      let appl_pattern = aux cic_appl_pattern in
-      Interpretation (loc, dsc, args, appl_pattern)
-  | cmd -> cmd
-
 type ('term, 'lazy_term, 'reduction, 'ident) tactical =
   | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
   | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactical
diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml
index 7687bc522..ce4a585b3 100644
--- a/helm/ocaml/grafite/grafiteAstPp.ml
+++ b/helm/ocaml/grafite/grafiteAstPp.ml
@@ -206,11 +206,6 @@ let pp_dir_opt = function
   | Some `LeftToRight -> "> "
   | Some `RightToLeft -> "< "
 
-let pp_metadata =
-  function
-  | Dependency buri -> sprintf "dependency %s" buri
-  | Baseuri buri -> sprintf "baseuri %s" buri
-
 let pp_command = function
   | Include (_,path) -> "include " ^ path
   | Qed _ -> "qed"
@@ -235,7 +230,6 @@ let pp_command = function
         (pp_associativity assoc)
         (pp_precedence prec)
         (pp_l2_pattern l2_pattern)
-  | Metadata (_, m) -> sprintf "metadata %s" (pp_metadata m)
   | Render _
   | Dump _ -> assert false  (* ZACK: debugging *)
 
@@ -293,7 +287,6 @@ let pp_cic_command = function
   | Render _
   | Dump _
   | Interpretation _
-  | Metadata _
   | Notation _
   | Obj _ -> assert false (* not implemented *)
 
diff --git a/helm/ocaml/grafite/grafiteAstPp.mli b/helm/ocaml/grafite/grafiteAstPp.mli
index eefcd9ccb..1ecfb4352 100644
--- a/helm/ocaml/grafite/grafiteAstPp.mli
+++ b/helm/ocaml/grafite/grafiteAstPp.mli
@@ -30,7 +30,6 @@ val pp_tactic:
 
 val pp_command:
   (CicNotationPt.term,CicNotationPt.obj) GrafiteAst.command -> string
-val pp_metadata: GrafiteAst.metadata -> string
 val pp_macro: ('a -> string) -> 'a GrafiteAst.macro -> string
 
 val pp_comment:
diff --git a/helm/ocaml/grafite/grafiteMarshal.ml b/helm/ocaml/grafite/grafiteMarshal.ml
index dd9febedb..8b4f8858b 100644
--- a/helm/ocaml/grafite/grafiteMarshal.ml
+++ b/helm/ocaml/grafite/grafiteMarshal.ml
@@ -28,24 +28,48 @@ exception Corrupt_moo of string
 exception Version_mismatch of string
 
 type ast_command = (Cic.term, Cic.obj) GrafiteAst.command
-type moo = ast_command list * GrafiteAst.metadata list  (** <moo, metadata> *)
+type moo = ast_command list
 
 let marshal_flags = []
 
+let rehash_cmd_uris =
+  let rehash_uri uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in
+  function
+  | GrafiteAst.Default (loc, name, uris) ->
+      let uris = List.map rehash_uri uris in
+      GrafiteAst.Default (loc, name, uris)
+  | GrafiteAst.Interpretation (loc, dsc, args, cic_appl_pattern) ->
+      let rec aux =
+        function
+        | CicNotationPt.UriPattern uri ->
+            CicNotationPt.UriPattern (rehash_uri uri)
+        | CicNotationPt.ApplPattern args ->
+            CicNotationPt.ApplPattern (List.map aux args)
+        | CicNotationPt.VarPattern _
+        | CicNotationPt.ImplicitPattern as pat -> pat
+      in
+      let appl_pattern = aux cic_appl_pattern in
+      GrafiteAst.Interpretation (loc, dsc, args, appl_pattern)
+  | GrafiteAst.Coercion (loc, term, close) ->
+      GrafiteAst.Coercion (loc, CicUtil.rehash_term term, close)
+  | GrafiteAst.Notation _
+  | GrafiteAst.Alias _ as cmd -> cmd
+  | cmd ->
+      prerr_endline "Found a command not expected in a .moo:";
+      prerr_endline (GrafiteAstPp.pp_cic_command cmd);
+      assert false
+
 (** .moo file format
  * - an integer -- magic number -- denoting the version of the dumped data
  *   structure. Different magic numbers stand for incompatible data structures
  * - an integer -- checksum -- denoting the hash value (computed with
  *   Hashtbl.hash) of the string representation of the dumped data structur
- * - marshalled pair: first component is a list of GrafiteAst.command (real moo
- *   content), second component is a list of GrafiteAst.metadata
+ * - marshalled data: list of GrafiteAst.command
  *)
 
-let save_moo ~fname (moo, metadata) =
+let save_moo ~fname moo =
  let oc = open_out fname in
- let marshalled = 
-   Marshal.to_string (List.rev moo, List.rev metadata) marshal_flags 
- in
+ let marshalled = Marshal.to_string (List.rev moo) marshal_flags in
  let checksum = Hashtbl.hash marshalled in
  output_binary_int oc GrafiteAst.magic;
  output_binary_int oc checksum;
@@ -67,7 +91,7 @@ let load_moo ~fname =
         let (moo:moo) =
           Marshal.from_string marshalled 0
         in
-        moo
+        List.map rehash_cmd_uris moo
       with End_of_file -> raise (Corrupt_moo fname))
     ()
 
diff --git a/helm/ocaml/grafite/grafiteMarshal.mli b/helm/ocaml/grafite/grafiteMarshal.mli
index 8fb1b2398..9be797a44 100644
--- a/helm/ocaml/grafite/grafiteMarshal.mli
+++ b/helm/ocaml/grafite/grafiteMarshal.mli
@@ -29,7 +29,7 @@ exception Corrupt_moo of string
 exception Version_mismatch of string
 
 type ast_command = (Cic.term, Cic.obj) GrafiteAst.command
-type moo = ast_command list * GrafiteAst.metadata list  (** <moo, metadata> *)
+type moo = ast_command list
 
 val save_moo: fname:string -> moo -> unit
 
diff --git a/helm/ocaml/grafite/grafiteParser.ml b/helm/ocaml/grafite/grafiteParser.ml
index 3d0ea500b..64db52295 100644
--- a/helm/ocaml/grafite/grafiteParser.ml
+++ b/helm/ocaml/grafite/grafiteParser.ml
@@ -492,10 +492,6 @@ EXTEND
     | IDENT "interpretation"; id = QSTRING;
       (symbol, args, l3) = interpretation ->
         GrafiteAst.Interpretation (loc, id, (symbol, args), l3)
-    | IDENT "metadata"; [ IDENT "dependency" | IDENT "baseuri" ] ; URI ->
-        (** metadata commands lives only in .moo, where they are in marshalled
-         * form *)
-        raise (HExtlib.Localized (loc,CicNotationParser.Parse_error "metadata not allowed here"))
 
     | IDENT "dump" -> GrafiteAst.Dump loc
     | IDENT "render"; u = URI ->
diff --git a/helm/ocaml/grafite2/grafiteEngine.ml b/helm/ocaml/grafite2/grafiteEngine.ml
index fe67c2fc4..70fb767a8 100644
--- a/helm/ocaml/grafite2/grafiteEngine.ml
+++ b/helm/ocaml/grafite2/grafiteEngine.ml
@@ -25,7 +25,8 @@
 
 exception Drop
 exception UnableToInclude of string
-exception IncludedFileNotCompiled of string
+exception IncludedFileNotCompiled of string (* file name *)
+exception MetadataNotFound of string        (* file name *)
 
 type options = { 
   do_heavy_checks: bool ; 
@@ -476,15 +477,23 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
   | GrafiteAst.Include (loc, path) ->
      let absolute_path = make_absolute opts.include_paths path in
      let moopath = GrafiteMisc.obj_file_of_script ~basedir absolute_path in
-     let status = ref status in
+     let metadatapath =
+       GrafiteMisc.metadata_file_of_script ~basedir absolute_path in
      if not (Sys.file_exists moopath) then
        raise (IncludedFileNotCompiled moopath);
+     let status =
+       if Helm_registry.get_bool "db.nodb" then
+         if not (Sys.file_exists metadatapath) then
+           raise (MetadataNotFound metadatapath)
+         else
+           GrafiteTypes.add_metadata
+             (LibraryNoDb.load_metadata ~fname:metadatapath) status
+       else
+         status
+     in
+     let status = ref status in
      eval_from_moo.efm_go status moopath;
      !status
-  | GrafiteAst.Metadata (loc, m) ->
-      (match m with
-      | GrafiteAst.Dependency uri -> GrafiteTypes.add_moo_metadata [m] status
-      | GrafiteAst.Baseuri _ -> status)
   | GrafiteAst.Set (loc, name, value) -> 
       let status = 
         if name = "baseuri" then begin
@@ -500,7 +509,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
             HLog.message ("cleaning baseuri " ^ value);
             LibraryClean.clean_baseuris ~basedir [value]
           end;
-          GrafiteTypes.add_moo_metadata [GrafiteAst.Baseuri value] status
+          GrafiteTypes.add_metadata [LibraryNoDb.Baseuri value] status
         end else
           status
       in
@@ -551,7 +560,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
       let status = GrafiteTypes.add_moo_content [stm] status in
       let uris =
         List.map
-          (fun uri -> GrafiteAst.Dependency (UriManager.buri_of_uri uri))
+          (fun uri -> LibraryNoDb.Dependency (UriManager.buri_of_uri uri))
           (CicNotationUtil.find_appl_pattern_uris cic_appl_pattern)
       in
       let diff =
@@ -559,7 +568,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
          DisambiguateChoices.lookup_symbol_by_dsc symbol dsc]
       in
       let status = MatitaSync.set_proof_aliases status diff in
-      let status = GrafiteTypes.add_moo_metadata uris status in
+      let status = GrafiteTypes.add_metadata uris status in
       status
   | GrafiteAst.Notation _ as stm -> GrafiteTypes.add_moo_content [stm] status
   | GrafiteAst.Obj (loc,obj) ->
@@ -645,9 +654,9 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
   let ast_of_cmd cmd =
     GrafiteAst.Executable (DisambiguateTypes.dummy_floc,
       GrafiteAst.Command (DisambiguateTypes.dummy_floc,
-        (GrafiteAst.reash_cmd_uris cmd)))
+        cmd))
   in
-  let moo, metadata = GrafiteMarshal.load_moo fname in
+  let moo = GrafiteMarshal.load_moo fname in
   List.iter 
     (fun ast -> 
       let ast = ast_of_cmd ast in
@@ -656,19 +665,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
          ~disambiguate_tactic:(fun status _ tactic -> ref status,tactic)
          ~disambiguate_command:(fun status cmd -> status,cmd)
          !status ast)
-    moo;
-  List.iter
-    (fun m ->
-      let ast =
-        ast_of_cmd (GrafiteAst.Metadata (DisambiguateTypes.dummy_floc, m))
-      in
-      status :=
-        eval_ast.ea_go
-         ~disambiguate_tactic:(fun status _ tactic -> ref status,tactic)
-         ~disambiguate_command:(fun status cmd -> status,cmd)
-         !status ast)
-    metadata
-
+    moo
 } and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command
   ?(do_heavy_checks=false) ?(include_paths=[]) ?(clean_baseuri=true) status st 
 ->
diff --git a/helm/ocaml/grafite2/grafiteMisc.ml b/helm/ocaml/grafite2/grafiteMisc.ml
index 910f8a483..8739b7a07 100644
--- a/helm/ocaml/grafite2/grafiteMisc.ml
+++ b/helm/ocaml/grafite2/grafiteMisc.ml
@@ -72,3 +72,8 @@ let baseuri_of_file file =
 let obj_file_of_script ~basedir f =
   let baseuri = baseuri_of_file f in
    LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri
+
+let metadata_file_of_script ~basedir f =
+  let baseuri = baseuri_of_file f in
+   LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri
+
diff --git a/helm/ocaml/grafite2/grafiteMisc.mli b/helm/ocaml/grafite2/grafiteMisc.mli
index 8cc384abc..9f1486b0b 100644
--- a/helm/ocaml/grafite2/grafiteMisc.mli
+++ b/helm/ocaml/grafite2/grafiteMisc.mli
@@ -33,3 +33,4 @@ val is_empty: string -> bool
 val baseuri_of_file : string -> string
 
 val obj_file_of_script : basedir:string -> string -> string
+val metadata_file_of_script : basedir:string -> string -> string
diff --git a/helm/ocaml/grafite2/grafiteTypes.ml b/helm/ocaml/grafite2/grafiteTypes.ml
index 2e2daf4e7..c73e8bd3c 100644
--- a/helm/ocaml/grafite2/grafiteTypes.ml
+++ b/helm/ocaml/grafite2/grafiteTypes.ml
@@ -53,6 +53,7 @@ type status = {
   aliases: DisambiguateTypes.environment;
   multi_aliases: DisambiguateTypes.multiple_environment;
   moo_content_rev: GrafiteMarshal.moo;
+  metadata: LibraryNoDb.metadata list;
   proof_status: proof_status;
   options: options;
   objects: UriManager.uri list;
@@ -115,7 +116,7 @@ let get_proof_conclusion status goal =
   | _ -> raise (Statement_error "no ongoing proof")
  
 let add_moo_content cmds status =
-  let content, metadata = status.moo_content_rev in
+  let content = status.moo_content_rev in
   let content' =
     List.fold_right
       (fun cmd acc ->
@@ -132,7 +133,7 @@ let add_moo_content cmds status =
   in
 (*   prerr_endline ("new moo content: " ^ String.concat " " (List.map
     GrafiteAstPp.pp_command content')); *)
-  { status with moo_content_rev = content', metadata }
+  { status with moo_content_rev = content' }
 
 let get_option status name =
   try
@@ -174,26 +175,29 @@ let get_string_option status name =
 
 let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
 
-let add_moo_metadata new_metadata status =
-  let content, metadata = status.moo_content_rev in
-  let metadata' =
-    List.fold_left
-      (fun acc m ->
-        match m with
-        | GrafiteAst.Dependency buri ->
-            let is_self = (* self dependency *)
-              try
-                get_string_option status "baseuri" = buri
-              with Option_error _ -> false  (* baseuri not yet set *)
-            in
-            if is_self
-              || List.exists (GrafiteAst.eq_metadata m) metadata (* duplicate *)
-            then acc
-            else m :: acc
-        | _ -> m :: acc)
-      metadata new_metadata
-  in
-  { status with moo_content_rev = content, metadata' }
+let add_metadata new_metadata status =
+  if Helm_registry.get_bool "db.nodb" then
+    let metadata = status.metadata in
+    let metadata' =
+      List.fold_left
+        (fun acc m ->
+          match m with
+          | LibraryNoDb.Dependency buri ->
+              let is_self = (* self dependency *)
+                try
+                  get_string_option status "baseuri" = buri
+                with Option_error _ -> false  (* baseuri not yet set *)
+              in
+              if is_self (* duplicate *)
+                || List.exists (LibraryNoDb.eq_metadata m) metadata
+              then acc
+              else m :: acc
+          | _ -> m :: acc)
+        metadata new_metadata
+    in
+    { status with metadata = metadata' }
+  else
+    status
 
 let dump_status status = 
   HLog.message "status.aliases:\n";
diff --git a/helm/ocaml/grafite2/grafiteTypes.mli b/helm/ocaml/grafite2/grafiteTypes.mli
index 17544d5bd..361a00825 100644
--- a/helm/ocaml/grafite2/grafiteTypes.mli
+++ b/helm/ocaml/grafite2/grafiteTypes.mli
@@ -48,6 +48,7 @@ type status = {
   aliases: DisambiguateTypes.environment;         (** disambiguation aliases *)
   multi_aliases: DisambiguateTypes.multiple_environment;
   moo_content_rev: GrafiteMarshal.moo;
+  metadata: LibraryNoDb.metadata list;
   proof_status: proof_status;                             (** logical status *)
   options: options;
   objects: UriManager.uri list;  (** in-scope objects *)
@@ -59,7 +60,7 @@ val dump_status : status -> unit
 
   (** list is not reversed, head command will be the first emitted *)
 val add_moo_content: GrafiteMarshal.ast_command list -> status -> status
-val add_moo_metadata: GrafiteAst.metadata list -> status -> status
+val add_metadata: LibraryNoDb.metadata list -> status -> status
 
 val get_option : status -> string -> option_value
 val get_string_option : status -> string -> string
diff --git a/helm/ocaml/grafite2/matitaSync.ml b/helm/ocaml/grafite2/matitaSync.ml
index 26ebbd032..2424d178f 100644
--- a/helm/ocaml/grafite2/matitaSync.ml
+++ b/helm/ocaml/grafite2/matitaSync.ml
@@ -56,7 +56,7 @@ let set_proof_aliases status new_aliases =
     (function
     | GrafiteAst.Ident_alias (_, suri) ->
         let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in
-        Some (GrafiteAst.Dependency buri)
+        Some (LibraryNoDb.Dependency buri)
     | _ -> None)
  in
  let aliases =
@@ -75,7 +75,7 @@ let set_proof_aliases status new_aliases =
      DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases
    in
    let status = add_moo_content (commands_of_aliases aliases) new_status in
-   let status = add_moo_metadata (deps_of_aliases aliases) status in
+   let status = add_metadata (deps_of_aliases aliases) status in
    status
 
 (** given a uri and a type list (the contructors types) builds a list of pairs
diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.cmi b/helm/ocaml/grafite_parser/grafiteDisambiguate.cmi
deleted file mode 100644
index 51403bfa4..000000000
Binary files a/helm/ocaml/grafite_parser/grafiteDisambiguate.cmi and /dev/null differ
diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.cmo b/helm/ocaml/grafite_parser/grafiteDisambiguate.cmo
deleted file mode 100644
index d78935a1b..000000000
Binary files a/helm/ocaml/grafite_parser/grafiteDisambiguate.cmo and /dev/null differ
diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.cmx b/helm/ocaml/grafite_parser/grafiteDisambiguate.cmx
deleted file mode 100644
index bef746423..000000000
Binary files a/helm/ocaml/grafite_parser/grafiteDisambiguate.cmx and /dev/null differ
diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
index 9e52f92b1..3c79cc040 100644
--- a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
@@ -238,7 +238,6 @@ let disambiguate_command status =
   | GrafiteAst.Dump _
   | GrafiteAst.Include _
   | GrafiteAst.Interpretation _
-  | GrafiteAst.Metadata _
   | GrafiteAst.Notation _
   | GrafiteAst.Qed _
   | GrafiteAst.Render _
diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.o b/helm/ocaml/grafite_parser/grafiteDisambiguate.o
deleted file mode 100644
index 14ccd78c4..000000000
Binary files a/helm/ocaml/grafite_parser/grafiteDisambiguate.o and /dev/null differ
diff --git a/helm/ocaml/grafite_parser/grafite_parser.a b/helm/ocaml/grafite_parser/grafite_parser.a
deleted file mode 100644
index 40b142e9f..000000000
Binary files a/helm/ocaml/grafite_parser/grafite_parser.a and /dev/null differ
diff --git a/helm/ocaml/grafite_parser/grafite_parser.cma b/helm/ocaml/grafite_parser/grafite_parser.cma
deleted file mode 100644
index 9bdad074f..000000000
Binary files a/helm/ocaml/grafite_parser/grafite_parser.cma and /dev/null differ
diff --git a/helm/ocaml/grafite_parser/grafite_parser.cmxa b/helm/ocaml/grafite_parser/grafite_parser.cmxa
deleted file mode 100644
index cd3799fda..000000000
Binary files a/helm/ocaml/grafite_parser/grafite_parser.cmxa and /dev/null differ
diff --git a/helm/ocaml/grafite_parser/matitaDisambiguator.cmx b/helm/ocaml/grafite_parser/matitaDisambiguator.cmx
deleted file mode 100644
index 1f8b72b6c..000000000
Binary files a/helm/ocaml/grafite_parser/matitaDisambiguator.cmx and /dev/null differ
diff --git a/helm/ocaml/library/.depend b/helm/ocaml/library/.depend
index 1ad51256b..279a4ea65 100644
--- a/helm/ocaml/library/.depend
+++ b/helm/ocaml/library/.depend
@@ -1,4 +1,3 @@
-coercGraph.cmi: coercDb.cmi 
 cicElim.cmo: cicElim.cmi 
 cicElim.cmx: cicElim.cmi 
 cicRecord.cmo: cicRecord.cmi 
@@ -7,15 +6,17 @@ libraryMisc.cmo: libraryMisc.cmi
 libraryMisc.cmx: libraryMisc.cmi 
 libraryDb.cmo: libraryDb.cmi 
 libraryDb.cmx: libraryDb.cmi 
-coercGraph.cmo: coercDb.cmi coercGraph.cmi 
-coercGraph.cmx: coercDb.cmx coercGraph.cmi 
 coercDb.cmo: coercDb.cmi 
 coercDb.cmx: coercDb.cmi 
 librarySync.cmo: libraryDb.cmi coercDb.cmi cicRecord.cmi cicElim.cmi \
     librarySync.cmi 
 librarySync.cmx: libraryDb.cmx coercDb.cmx cicRecord.cmx cicElim.cmx \
     librarySync.cmi 
-libraryClean.cmo: librarySync.cmi libraryMisc.cmi libraryDb.cmi \
-    libraryClean.cmi 
-libraryClean.cmx: librarySync.cmx libraryMisc.cmx libraryDb.cmx \
-    libraryClean.cmi 
+coercGraph.cmo: librarySync.cmi coercDb.cmi coercGraph.cmi 
+coercGraph.cmx: librarySync.cmx coercDb.cmx coercGraph.cmi 
+libraryNoDb.cmo: libraryNoDb.cmi 
+libraryNoDb.cmx: libraryNoDb.cmi 
+libraryClean.cmo: librarySync.cmi libraryNoDb.cmi libraryMisc.cmi \
+    libraryDb.cmi libraryClean.cmi 
+libraryClean.cmx: librarySync.cmx libraryNoDb.cmx libraryMisc.cmx \
+    libraryDb.cmx libraryClean.cmi 
diff --git a/helm/ocaml/library/Makefile b/helm/ocaml/library/Makefile
index c22a61976..ee07c8162 100644
--- a/helm/ocaml/library/Makefile
+++ b/helm/ocaml/library/Makefile
@@ -9,6 +9,7 @@ INTERFACE_FILES = \
 	coercDb.mli \
 	librarySync.mli \
 	coercGraph.mli \
+	libraryNoDb.mli \
 	libraryClean.mli \
 	$(NULL)
 IMPLEMENTATION_FILES = \
diff --git a/helm/ocaml/library/libraryClean.ml b/helm/ocaml/library/libraryClean.ml
index a7a3d7345..00f2c4ef0 100644
--- a/helm/ocaml/library/libraryClean.ml
+++ b/helm/ocaml/library/libraryClean.ml
@@ -122,10 +122,10 @@ let close_uri_list uri_to_remove =
   in
   uri_to_remove, depend
 
-let rec close_using_db uris next =
+let rec close_db uris next =
   match next with
   | [] -> uris
-  | l -> let uris, next = close_uri_list l in close_using_db uris next @ uris
+  | l -> let uris, next = close_uri_list l in close_db uris next @ uris
   
 let cleaned_no = ref 0;;
 
@@ -145,7 +145,7 @@ let moo_root_dir = lazy (
   String.sub url 7 (String.length url - 7)  (* remove heading "file:///" *)
 )
 
-let close_using_moos buris =
+let close_nodb buris =
   let rev_deps = Hashtbl.create 97 in
   let all_moos =
     HExtlib.find ~test:(fun name -> Filename.check_suffix name ".moo")
@@ -153,11 +153,11 @@ let close_using_moos buris =
   in
   List.iter
     (fun path -> 
-      let _, metadata = GrafiteMarshal.load_moo ~fname:path in
+      let metadata = LibraryNoDb.load_metadata ~fname:path in
       let baseuri_of_current_moo = 
         let rec aux = function 
           | [] -> assert false
-          | GrafiteAst.Baseuri buri::_ -> buri
+          | LibraryNoDb.Baseuri buri::_ -> buri
           | _ :: tl -> aux tl
         in
         aux metadata
@@ -165,7 +165,7 @@ let close_using_moos buris =
       let deps = 
         HExtlib.filter_map 
           (function 
-          | GrafiteAst.Dependency buri -> Some buri
+          | LibraryNoDb.Dependency buri -> Some buri
           | _ -> None ) 
         metadata
       in
@@ -198,9 +198,9 @@ let clean_baseuris ?(verbose=true) ~basedir buris =
     List.iter debug_prerr buris; 
   let l = 
     if Helm_registry.get_bool "db.nodb" then
-      close_using_moos buris
+      close_nodb buris
     else
-      close_using_db [] buris 
+      close_db [] buris 
   in
   let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in
   let l = List.map UriManager.uri_of_string l in
diff --git a/helm/ocaml/library/libraryMisc.ml b/helm/ocaml/library/libraryMisc.ml
index 2b6d64f63..e953859b6 100644
--- a/helm/ocaml/library/libraryMisc.ml
+++ b/helm/ocaml/library/libraryMisc.ml
@@ -23,7 +23,10 @@
  * http://helm.cs.unibo.it/
  *)
 
-
 let obj_file_of_baseuri ~basedir ~baseuri =
  let path = basedir ^ "/xml" ^ Pcre.replace ~pat:"^cic:" ~templ:"" baseuri in
   path ^ ".moo"
+
+let metadata_file_of_baseuri ~basedir ~baseuri =
+ let path = basedir ^ "/xml" ^ Pcre.replace ~pat:"^cic:" ~templ:"" baseuri in
+  path ^ ".metadata"
diff --git a/helm/ocaml/library/libraryMisc.mli b/helm/ocaml/library/libraryMisc.mli
index fc93095eb..03a4742c5 100644
--- a/helm/ocaml/library/libraryMisc.mli
+++ b/helm/ocaml/library/libraryMisc.mli
@@ -23,5 +23,6 @@
  * http://helm.cs.unibo.it/
  *)
 
-
 val obj_file_of_baseuri: basedir:string -> baseuri:string -> string
+val metadata_file_of_baseuri: basedir:string -> baseuri:string -> string
+
diff --git a/helm/ocaml/library/libraryNoDb.ml b/helm/ocaml/library/libraryNoDb.ml
new file mode 100644
index 000000000..12a2e96da
--- /dev/null
+++ b/helm/ocaml/library/libraryNoDb.ml
@@ -0,0 +1,75 @@
+(* Copyright (C) 2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open Printf
+
+exception Checksum_failure of string
+exception Corrupt_metadata of string
+exception Version_mismatch of string
+
+let magic = 1
+
+type metadata =
+  | Dependency of string  (* baseuri without trailing slash *)
+  | Baseuri of string 
+
+let eq_metadata (m1:metadata) (m2:metadata) = m1 = m2
+
+let marshal_flags = []
+
+(** .metadata file format
+ * - an integer -- magic number -- denoting the version of the dumped data
+ *   structure. Different magic numbers stand for incompatible data structures
+ * - an integer -- checksum -- denoting the hash value (computed with
+ *   Hashtbl.hash) of the string representation of the dumped data structur
+ * - marshalled data: list of metadata
+ *)
+
+let save_metadata ~fname metadata =
+  let oc = open_out fname in
+  let marshalled = Marshal.to_string metadata marshal_flags in
+  let checksum = Hashtbl.hash marshalled in
+  output_binary_int oc magic;
+  output_binary_int oc checksum;
+  output_string oc marshalled;
+  close_out oc
+
+let load_metadata ~fname =
+  let ic = open_in fname in
+  HExtlib.finally
+    (fun () -> close_in ic)
+    (fun () ->
+      try
+        let file_magic = input_binary_int ic in
+        if file_magic <> magic then raise (Version_mismatch fname);
+        let file_checksum = input_binary_int ic in
+        let marshalled = HExtlib.input_all ic in
+        let checksum = Hashtbl.hash marshalled in
+        if checksum <> file_checksum then raise (Checksum_failure fname);
+        let (metadata:metadata list) = Marshal.from_string marshalled 0 in
+        metadata
+      with End_of_file -> raise (Corrupt_metadata fname))
+    ()
+
diff --git a/helm/ocaml/library/libraryNoDb.mli b/helm/ocaml/library/libraryNoDb.mli
new file mode 100644
index 000000000..33b1b1eb3
--- /dev/null
+++ b/helm/ocaml/library/libraryNoDb.mli
@@ -0,0 +1,36 @@
+(* Copyright (C) 2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* TODO the strings below should be UriManager.uri, but UriManager ATM does not
+ * support their format *)
+type metadata =
+  | Dependency of string  (* baseuri without trailing slash *)
+  | Baseuri of string 
+
+val eq_metadata: metadata -> metadata -> bool
+
+val save_metadata: fname:string -> metadata list -> unit
+val load_metadata: fname:string -> metadata list
+