diff options
| -rw-r--r-- | Makefile.build | 8 | ||||
| -rw-r--r-- | Makefile.common | 5 | ||||
| -rw-r--r-- | config/Makefile.template | 1 | ||||
| -rw-r--r-- | config/coq_config.mli | 2 | ||||
| -rwxr-xr-x | configure | 9 | ||||
| -rw-r--r-- | ide/coq.ml | 2 | ||||
| -rw-r--r-- | scripts/coqmktop.ml | 13 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 77 | ||||
| -rw-r--r-- | toplevel/mltop.mli | 21 |
10 files changed, 90 insertions, 50 deletions
diff --git a/Makefile.build b/Makefile.build index 872f8e30b..e776c5ec1 100644 --- a/Makefile.build +++ b/Makefile.build @@ -478,7 +478,7 @@ bin/coq-parser$(EXE):$(LIBCOQRUN) $(PARSERCMO) bin/coq-parser.opt$(EXE): $(LIBCOQRUN) $(PARSERCMX) $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) -linkall $(OPTFLAGS) -o $@ \ - $(LIBCOQRUN) nums.cmxa $(CMXA) $(PARSERCMX) + $(LIBCOQRUN) $(DYNLINKCMXA) nums.cmxa $(CMXA) $(PARSERCMX) pcoq-files:: $(INTERFACEVO) $(INTERFACERC) @@ -755,12 +755,14 @@ toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml4.ml.d toplevel/mlto ## In other words, the Byte-only code doesn't import a new module. toplevel/mltop.byteml: toplevel/mltop.ml4 # no camlp4deps here $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` -DByte -impl $< > $@ \ + $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` \ + -DByte -DHasDynlink -impl $< > $@ \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) toplevel/mltop.optml: toplevel/mltop.ml4 # no camlp4deps here $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` -impl $< > $@ \ + $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` \ + $(NATDYNLINKDEF) -impl $< > $@ \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) # files compiled with -rectypes diff --git a/Makefile.common b/Makefile.common index 1be1d0dfb..11cac4425 100644 --- a/Makefile.common +++ b/Makefile.common @@ -29,6 +29,11 @@ CHICKENOPT:=bin/coqchk.opt$(EXE) BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE) CHICKEN:=bin/coqchk$(EXE) +ifeq ($(HASNATDYNLINK),true) + DYNLINKCMXA:=dynlink.cmxa + NATDYNLINKDEF:=-DHasDynlink +endif + INSTALLBIN:=install INSTALLLIB:=install -m 644 MKDIR:=install -d diff --git a/config/Makefile.template b/config/Makefile.template index e0e7bf0b0..3fd726923 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -96,6 +96,7 @@ BEST=BESTCOMPILER # Your architecture # Can be obtain by UNIX command arch ARCH=ARCHITECTURE +HASNATDYNLINK=HASNATIVEDYNLINK # Your C compiler and co CC="CCEXEC" diff --git a/config/coq_config.mli b/config/coq_config.mli index 46404215f..e5a32708d 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -44,3 +44,5 @@ val with_geoproof : bool ref (* to (de)activate functions specific to Geoproof w val browser : string (** default web browser to use, may be overriden by environment variable COQREMOTEBROWSER *) + +val has_natdynlink : bool @@ -455,6 +455,13 @@ if [ "$coq_debug_flag" = "-g" ]; then esac fi +# Native dynlink +if test -f `"$CAMLC" -where`/dynlink.cmxa; then + HASNATDYNLINK=true +else + HASNATDYNLINK=false +fi + # Camlp4 / Camlp5 configuration if [ "$camlp5dir" != "" ]; then @@ -900,6 +907,7 @@ let camlp4 = "$CAMLP4" let camlp4lib = "$ESCCAMLP4LIB" let best = "$best_compiler" let arch = "$ARCH" +let has_natdynlink = $HASNATDYNLINK let osdeplibs = "$OSDEPLIBS" let version = "$VERSION" let date = "$DATE" @@ -985,6 +993,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \ -e "s|COQIDEOPT|$COQIDE|" \ -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \ -e "s|WITHDOCOPT|$with_doc|" \ + -e "s|HASNATIVEDYNLINK|$HASNATDYNLINK|" \ "$COQSRC/config/Makefile.template" > "$COQSRC/config/Makefile" chmod a-w "$COQSRC/config/Makefile" diff --git a/ide/coq.ml b/ide/coq.ml index 2c8d7b8db..2d8c2ff99 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -79,7 +79,7 @@ let version () = ver date Coq_config.arch Sys.os_type (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z) - (if Mltop.get () = Mltop.Native then "native" else "bytecode") + (if Mltop.is_native then "native" else "bytecode") (if Coq_config.best="opt" then "native" else "bytecode") let is_in_coq_lib dir = diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index c89ea827e..021b1a80d 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -83,7 +83,8 @@ let module_of_file name = (* Build the list of files to link and the list of modules names *) let files_to_link userfiles = - let dyn_objs = if not !opt then dynobjs else [] in + let dyn_objs = + if not !opt || Coq_config.has_natdynlink then dynobjs else [] in let toplevel_objs = if !top then topobjs else if !opt then notopobjs else [] in let ide_objs = if !coqide then @@ -240,17 +241,15 @@ let tmp_dynlink()= (* Initializes the kind of loading in the main program *) let declare_loading_string () = - if !opt then - "Mltop.set Mltop.Native;;\n" - else if not !top then - "Mltop.set Mltop.WithoutTop;;\n" + if not !top then + "Mltop.remove ();;" else "let ppf = Format.std_formatter;; - Mltop.set (Mltop.WithTop + Mltop.set_top {Mltop.load_obj=Topdirs.dir_load ppf; Mltop.use_file=Topdirs.dir_use ppf; Mltop.add_dir=Topdirs.dir_directory; - Mltop.ml_loop=(fun () -> Toploop.loop ppf) });;\n" + Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\n" (* create a temporary main file to link *) let create_tmp_main_file modules = diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 7567f0eb6..277bc8d09 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -132,7 +132,7 @@ let set_opt () = re_exec_version := "opt" let re_exec is_ide = let s = !re_exec_version in - let is_native = (Mltop.get()) = Mltop.Native in + let is_native = Mltop.is_native in (* Unix.readlink is not implemented on Windows architectures :-( let prog = try Unix.readlink "/proc/self/exe" diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index dd741d40a..4cf1f134f 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -62,17 +62,18 @@ type toplevel = { type kind_load = | WithTop of toplevel | WithoutTop - | Native (* Must be always initialized *) -let load = ref Native +let load = ref WithoutTop -(* Sets and initializes the kind of loading *) -let set kload = load := kload -let get () = !load +(* Are we in a native version of Coq? *) +let is_native = IFDEF Byte THEN false ELSE true END -(* Resets load *) -let remove ()= load := Native +(* Sets and initializes a toplevel (if any) *) +let set_top toplevel = load := WithTop toplevel + +(* Removes the toplevel (if any) *) +let remove ()= load := WithoutTop (* Tests if an Ocaml toplevel runs under Coq *) let is_ocaml_top () = @@ -81,10 +82,7 @@ let is_ocaml_top () = |_ -> false (* Tests if we can load ML files *) -let enable_load () = - match !load with - | WithTop _ | WithoutTop -> true - |_ -> false +let has_dynlink = IFDEF HasDynlink THEN true ELSE false END (* Runs the toplevel loop of Ocaml *) let ocaml_toploop () = @@ -103,7 +101,7 @@ let dir_ml_load s = str s ++ str" to Coq code.")) (* TO DO: .cma loading without toplevel *) | WithoutTop -> - IFDEF Byte THEN + IFDEF HasDynlink THEN (* WARNING * if this code section starts to use a module not used elsewhere * in this file, the Makefile dependency logic needs to be updated. @@ -117,10 +115,10 @@ let dir_ml_load s = [Filename.dirname gname] with | Dynlink.Error a -> errorlabstrm "Mltop.load_object" (str (Dynlink.error_message a)) - ELSE () END - | Native -> - errorlabstrm "Mltop.no_load_object" - (str"Loading of ML object file forbidden in a native Coq.") + ELSE + errorlabstrm "Mltop.no_load_object" + (str"Loading of ML object file forbidden in a native Coq.") + END (* Dynamic interpretation of .ml *) let dir_ml_use s = @@ -132,7 +130,7 @@ let dir_ml_use s = let add_ml_dir s = match !load with | WithTop t -> t.add_dir s; keep_copy_mlpath s - | WithoutTop -> keep_copy_mlpath s + | WithoutTop when has_dynlink -> keep_copy_mlpath s | _ -> () (* For Rec Add ML Path *) @@ -182,15 +180,44 @@ let mod_of_name name = in String.capitalize base -let file_of_name name = - let bname = String.uncapitalize name in - let fname = make_suffix bname ".cmo" in - if (is_in_path !coq_mlpath_copy fname) then fname - else let fname=make_suffix bname ".cma" in - if (is_in_path !coq_mlpath_copy fname) then fname +let get_ml_object_suffix name = + if Filename.check_suffix name ".cmo" then + Some ".cmo" + else if Filename.check_suffix name ".cma" then + Some ".cma" + else if Filename.check_suffix name ".cmxs" then + Some ".cmxs" else + None + +let file_of_name name = + let name = String.uncapitalize name in + let suffix = get_ml_object_suffix name in + let fail s = errorlabstrm "Mltop.load_object" - (str"File not found on loadpath : " ++ str (bname^".cm[oa]")) + (str"File not found on loadpath : " ++ str s) in + if is_native then + let name = match suffix with + | Some ((".cmo"|".cma") as suffix) -> + (Filename.chop_suffix name suffix) ^ ".cmxs" + | Some ".cmxs" -> name + | _ -> name ^ ".cmxs" + in + if is_in_path !coq_mlpath_copy name then name else fail name + else + let (full, base) = match suffix with + | Some ".cmo" | Some ".cma" -> true, name + | Some ".cmxs" -> false, Filename.chop_suffix name ".cmxs" + | _ -> false, name + in + if full then + if is_in_path !coq_mlpath_copy base then base else fail base + else + let name = base ^ ".cmo" in + if is_in_path !coq_mlpath_copy name then name else + let name = base ^ ".cma" in + if is_in_path !coq_mlpath_copy name then name else + fail (base ^ ".cm[oa]") (* TODO: supprimer ce hack, si possible *) (* Initialisation of ML modules that need the state (ex: tactics like @@ -242,7 +269,7 @@ let unfreeze_ml_modules x = (fun name -> let mname = mod_of_name name in if not (module_is_known mname) then - if enable_load() then + if has_dynlink then let fname = file_of_name mname in load_object mname fname else diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index 0ccb774e3..15fdbe4c5 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -16,25 +16,20 @@ type toplevel = { add_dir : string -> unit; ml_loop : unit -> unit } -(* Determines the behaviour of Coq with respect to ML files (compiled - or not) *) -type kind_load= - | WithTop of toplevel - | WithoutTop - | Native - -(* Sets and initializes the kind of loading *) -val set : kind_load -> unit -val get : unit -> kind_load - -(* Resets the kind of loading *) +(* Sets and initializes a toplevel (if any) *) +val set_top : toplevel -> unit + +(* Are we in a native version of Coq? *) +val is_native : bool + +(* Removes the toplevel (if any) *) val remove : unit -> unit (* Tests if an Ocaml toplevel runs under Coq *) val is_ocaml_top : unit -> bool (* Tests if we can load ML files *) -val enable_load : unit -> bool +val has_dynlink : bool (* Starts the Ocaml toplevel loop *) val ocaml_toploop : unit -> unit |