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
-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"
-requires="helm-grafite helm-metadata"
+requires="helm-cic_acic helm-metadata"
version="0.0.1"
archive(byte)="library.cma"
archive(native)="library.cmxa"
| 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
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 *)
(* 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
| 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"
(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 *)
| Render _
| Dump _
| Interpretation _
- | Metadata _
| Notation _
| Obj _ -> assert false (* not implemented *)
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:
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;
let (moo:moo) =
Marshal.from_string marshalled 0
in
- moo
+ List.map rehash_cmd_uris moo
with End_of_file -> raise (Corrupt_moo fname))
()
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
| 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 ->
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 ;
| 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
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
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 =
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) ->
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
~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
->
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
+
val baseuri_of_file : string -> string
val obj_file_of_script : basedir:string -> string -> string
+val metadata_file_of_script : basedir:string -> string -> string
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;
| _ -> 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 ->
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
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";
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 *)
(** 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
(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 =
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
| GrafiteAst.Dump _
| GrafiteAst.Include _
| GrafiteAst.Interpretation _
- | GrafiteAst.Metadata _
| GrafiteAst.Notation _
| GrafiteAst.Qed _
| GrafiteAst.Render _
-coercGraph.cmi: coercDb.cmi
cicElim.cmo: cicElim.cmi
cicElim.cmx: cicElim.cmi
cicRecord.cmo: cicRecord.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
coercDb.mli \
librarySync.mli \
coercGraph.mli \
+ libraryNoDb.mli \
libraryClean.mli \
$(NULL)
IMPLEMENTATION_FILES = \
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;;
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")
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
let deps =
HExtlib.filter_map
(function
- | GrafiteAst.Dependency buri -> Some buri
+ | LibraryNoDb.Dependency buri -> Some buri
| _ -> None )
metadata
in
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
* 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"
* 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
+
--- /dev/null
+(* 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))
+ ()
+
--- /dev/null
+(* 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
+
projects / helm.git / commitdiff