}
let eval_coercion status ~add_composites uri =
- let basedir = Helm_registry.get "matita.basedir" in
let status,compounds =
- GrafiteSync.add_coercion ~basedir ~add_composites refinement_toolkit status uri in
+ GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri in
let moo_content = coercion_moo_statement_of uri in
let status = GrafiteTypes.add_moo_content [moo_content] status in
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
lemmas
let add_obj uri obj status =
- let basedir = Helm_registry.get "matita.basedir" in
- let status,lemmas = GrafiteSync.add_obj ~basedir refinement_toolkit uri obj status in
+ let status,lemmas = GrafiteSync.add_obj refinement_toolkit uri obj status in
status, lemmas
let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
let status,cmd = disambiguate_command status cmd in
- let basedir = Helm_registry.get "matita.basedir" in
let status,uris =
match cmd with
| GrafiteAst.Default (loc, what, uris) as cmd ->
LibraryObjects.set_default what uris;
GrafiteTypes.add_moo_content [cmd] status,[]
| GrafiteAst.Include (loc, baseuri) ->
- let moopath = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
- if not (Sys.file_exists moopath) then
- raise (IncludedFileNotCompiled moopath);
+ let moopath_rw, moopath_r =
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:true,
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:false
+ in
+ let moopath =
+ if Sys.file_exists moopath_r then moopath_r else
+ if Sys.file_exists moopath_rw then moopath_rw else
+ raise (IncludedFileNotCompiled moopath_rw)
+ in
let status = eval_from_moo.efm_go status moopath in
status,[]
| GrafiteAst.Set (loc, name, value) ->
HLog.error (sprintf "uri %s belongs to a read-only repository" value);
raise (ReadOnlyUri value)
end;
- if not (GrafiteMisc.is_empty value) && opts.clean_baseuri then begin
+ if not (Http_getter_storage.is_empty value) &&
+ opts.clean_baseuri
+ then begin
HLog.message ("baseuri " ^ value ^ " is not empty");
HLog.message ("cleaning baseuri " ^ value);
- LibraryClean.clean_baseuris ~basedir [value];
+ LibraryClean.clean_baseuris [value];
+ assert (Http_getter_storage.is_empty value);
end;
+ HExtlib.mkdir
+ (Filename.dirname (Http_getter.filename ~writable:true (value ^
+ "/foo.con")));
end;
GrafiteTypes.set_option status name value,[]
| GrafiteAst.Drop loc -> raise Drop