diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/nativelib.ml | 19 | ||||
| -rw-r--r-- | kernel/nativelib.mli | 3 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 8 |
3 files changed, 17 insertions, 13 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index a62b51e8aa..86eaaddc90 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -25,7 +25,7 @@ let open_header = ["Nativevalues"; let open_header = List.map mk_open open_header (* Directory where compiled files are stored *) -let output_dir = ".coq-native" +let output_dir = ref ".coq-native" (* Extension of generated ml files, stored for debugging purposes *) let source_ext = ".native" @@ -51,8 +51,13 @@ let () = at_exit (fun () -> be guessed until flags have been properly initialized. It also lets us avoid forcing [my_temp_dir] if we don't need it (eg stdlib file without native compute or native conv uses). *) -let include_dirs () = - let base = [Envars.coqlib () / "kernel"; Envars.coqlib () / "library"] in +let include_dirs = ref [] +let get_include_dirs () = + let base = match !include_dirs with + | [] -> + [Envars.coqlib () / "kernel"; Envars.coqlib () / "library"] + | _::_ as l -> l + in if Lazy.is_val my_temp_dir then (Lazy.force my_temp_dir) :: base else base @@ -88,8 +93,8 @@ let error_native_compiler_failed e = let call_compiler ?profile:(profile=false) ml_filename = let load_path = !get_load_paths () in - let load_path = List.map (fun dn -> dn / output_dir) load_path in - let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (include_dirs () @ load_path)) in + let load_path = List.map (fun dn -> dn / !output_dir) load_path in + let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (get_include_dirs () @ load_path)) in let f = Filename.chop_extension ml_filename in let link_filename = f ^ ".cmo" in let link_filename = Dynlink.adapt_filename link_filename in @@ -139,7 +144,7 @@ let compile_library dir code fn = let fn = fn ^ source_ext in let basename = Filename.basename fn in let dirname = Filename.dirname fn in - let dirname = dirname / output_dir in + let dirname = dirname / !output_dir in let () = try Unix.mkdir dirname 0o755 with Unix.Unix_error (Unix.EEXIST, _, _) -> () @@ -181,5 +186,5 @@ let call_linker ?(fatal=true) env ~prefix f upds = match upds with Some upds -> update_locations upds | _ -> () let link_library env ~prefix ~dirname ~basename = - let f = dirname / output_dir / basename in + let f = dirname / !output_dir / basename in call_linker env ~fatal:false ~prefix f None diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index 52d18acca6..155fde54e9 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -13,7 +13,8 @@ open Nativecode used by the native compiler. *) (* Directory where compiled files are stored *) -val output_dir : string +val output_dir : CUnix.physical_path ref +val include_dirs : CUnix.physical_path list ref val get_load_paths : (unit -> string list) ref diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index faa601e277..2ecd4880f7 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -61,7 +61,7 @@ let feedback_completion_typecheck = Feedback.feedback ~id:state_id Feedback.Complete) type typing_context = -| MonoTyCtx of Environ.env * unsafe_type_judgment * Univ.ContextSet.t * Id.Set.t * Stateid.t option +| MonoTyCtx of Environ.env * unsafe_type_judgment * Id.Set.t * Stateid.t option | PolyTyCtx of Environ.env * unsafe_type_judgment * Univ.universe_level_subst * Univ.AUContext.t * Id.Set.t * Stateid.t option let infer_declaration env (dcl : constant_entry) = @@ -155,7 +155,7 @@ let infer_opaque env = function let env = push_context_set ~strict:true univs env in let { opaque_entry_feedback = feedback_id; _ } = c in let tyj = Typeops.infer_type env typ in - let context = MonoTyCtx (env, tyj, univs, c.opaque_entry_secctx, feedback_id) in + let context = MonoTyCtx (env, tyj, c.opaque_entry_secctx, feedback_id) in let def = OpaqueDef () in { Cooking.cook_body = def; @@ -257,10 +257,8 @@ let build_constant_declaration env result = const_typing_flags = Environ.typing_flags env } let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_output) = match tyenv with -| MonoTyCtx (env, tyj, univs, declared, feedback_id) -> +| MonoTyCtx (env, tyj, declared, feedback_id) -> let ((body, uctx), side_eff) = body in - (* don't redeclare universes which are declared for the type *) - let uctx = Univ.ContextSet.diff uctx univs in let (body, uctx', valid_signatures) = handle env body side_eff in let uctx = Univ.ContextSet.union uctx uctx' in let env = push_context_set uctx env in |