diff options
| -rw-r--r-- | .gitignore | 3 | ||||
| -rw-r--r-- | Makefile.build | 21 | ||||
| -rw-r--r-- | _tags | 2 | ||||
| -rwxr-xr-x | configure | 67 | ||||
| -rw-r--r-- | dev/dynlink.ml | 51 | ||||
| -rw-r--r-- | myocamlbuild.ml | 20 | ||||
| -rw-r--r-- | toplevel/mltop.ml (renamed from toplevel/mltop.ml4) | 24 |
7 files changed, 99 insertions, 89 deletions
diff --git a/.gitignore b/.gitignore index c3669497f..2b497f9a9 100644 --- a/.gitignore +++ b/.gitignore @@ -136,15 +136,12 @@ tactics/eqdecide.ml tactics/extratactics.ml tactics/extraargs.ml tools/coq_tex.ml -toplevel/mltop.ml toplevel/whelp.ml ide/coqide_main.ml ide/coqide_main_opt.ml # other auto-generated files -toplevel/mltop.optml -toplevel/mltop.byteml kernel/byterun/coq_jumptbl.h kernel/copcodes.ml scripts/tolink.ml diff --git a/Makefile.build b/Makefile.build index f2fabf918..6efdf95a4 100644 --- a/Makefile.build +++ b/Makefile.build @@ -742,27 +742,6 @@ grammar/grammar.cma: | grammar/grammar.mllib.d $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@ -# toplevel/mltop.ml4 (ifdef Byte) - -## NB: mltop.ml correspond to the byte version (and hence need no special rules) -## while the opt version is in mltop.optml. Since mltop.optml uses mltop.ml.d -## as dependency file, be sure to import the same modules in the different sections -## of the ml4 - -MLTOP:=toplevel/mltop - -$(MLTOP).cmx: $(MLTOP).optml | $(MLTOP).ml.d $(MLTOP).ml4.d - $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $< -o $@ - -$(MLTOP).ml: $(MLTOP).ml4 config/Makefile # no camlp4deps here - $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -DByte -DHasDynlink -impl $< -o $@ - -$(MLTOP).optml: $(MLTOP).ml4 config/Makefile # no camlp4deps here - $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) $(NATDYNLINKDEF) -impl $< -o $@ - ide/coqide_main.ml: ide/coqide_main.ml4 $(SHOW)'CAMLP4O $<' $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -impl $< -o $@ @@ -28,8 +28,6 @@ ## tags for camlp4 files -"toplevel/mltop.ml4": is_mltop - "toplevel/whelp.ml4": use_grammar "parsing/g_constr.ml4": use_compat5 @@ -465,36 +465,6 @@ if [ "$coq_debug_flag" = "-g" ]; then esac fi -# Native dynlink -if [ "$natdynlink" = "yes" -a -f "$CAMLLIB"/dynlink.cmxa ]; then - HASNATDYNLINK=true -else - HASNATDYNLINK=false -fi - -case $HASNATDYNLINK,$ARCH,`uname -r`,$CAMLVERSION in - true,Darwin,9.*,3.11.*) # ocaml 3.11.0 dynlink on MacOS 10.5 is buggy - NATDYNLINKFLAG=os5fixme;; - #Possibly a problem on 10.6.0/10.6.1/10.6.2 - #May just be a 32 vs 64 problem for all 10.6.* - true,Darwin,10.0.*,3.11.*) # Possibly a problem on 10.6.0 - NATDYNLINKFLAG=os5fixme;; - true,Darwin,10.1.*,3.11.*) # Possibly a problem on 10.6.1 - NATDYNLINKFLAG=os5fixme;; - true,Darwin,10.2.*,3.11.*) # Possibly a problem on 10.6.2 - NATDYNLINKFLAG=os5fixme;; - true,Darwin,10.*,3.11.*) - if [ `getconf LONG_BIT` = "32" ]; then - # Still a problem for x86_32 - NATDYNLINKFLAG=os5fixme - else - # Not a problem for x86_64 - NATDYNLINKFLAG=$HASNATDYNLINK - fi;; - *) - NATDYNLINKFLAG=$HASNATDYNLINK;; -esac - # Camlp4 / Camlp5 configuration # Assume that camlp(4|5) binaries are at the same place as ocaml ones @@ -572,6 +542,13 @@ if [ "$best_compiler" = "opt" ] ; then best_compiler=byte echo "Cannot find native-code $CAMLP4," echo "only the bytecode version of Coq will be available." + elif [ ! -f "$CAMLLIB"/dynlink.cmxa ]; then + best_compiler=byte + echo "Cannot find native-code dynlink library," + echo "only the bytecode version of Coq will be available." + echo "For building a native-code Coq, you may try to first" + echo "compile and install a dummy dynlink.cmxa (see dev/dynlink.ml)" + echo "and then run ./configure -natdynlink no" else if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then echo "Native and bytecode compilers do not have the same version!" @@ -584,6 +561,36 @@ if [ "$best_compiler" = "opt" ] ; then fi fi +# Native dynlink +if [ "$natdynlink" = "yes" -a -f "$CAMLLIB"/dynlink.cmxa ]; then + HASNATDYNLINK=true +else + HASNATDYNLINK=false +fi + +case $HASNATDYNLINK,$ARCH,`uname -r`,$CAMLVERSION in + true,Darwin,9.*,3.11.*) # ocaml 3.11.0 dynlink on MacOS 10.5 is buggy + NATDYNLINKFLAG=os5fixme;; + #Possibly a problem on 10.6.0/10.6.1/10.6.2 + #May just be a 32 vs 64 problem for all 10.6.* + true,Darwin,10.0.*,3.11.*) # Possibly a problem on 10.6.0 + NATDYNLINKFLAG=os5fixme;; + true,Darwin,10.1.*,3.11.*) # Possibly a problem on 10.6.1 + NATDYNLINKFLAG=os5fixme;; + true,Darwin,10.2.*,3.11.*) # Possibly a problem on 10.6.2 + NATDYNLINKFLAG=os5fixme;; + true,Darwin,10.*,3.11.*) + if [ `getconf LONG_BIT` = "32" ]; then + # Still a problem for x86_32 + NATDYNLINKFLAG=os5fixme + else + # Not a problem for x86_64 + NATDYNLINKFLAG=$HASNATDYNLINK + fi;; + *) + NATDYNLINKFLAG=$HASNATDYNLINK;; +esac + # OS dependent libraries OSDEPLIBS="-cclib -lunix" diff --git a/dev/dynlink.ml b/dev/dynlink.ml new file mode 100644 index 000000000..810e0ffca --- /dev/null +++ b/dev/dynlink.ml @@ -0,0 +1,51 @@ + +(** Some architectures may have a native ocaml compiler but no native + dynlink.cmxa (e.g. ARM). If you still want to build a native coqtop + there, you'll need this dummy implementation of Dynlink. + Compile it and install with: + + ocamlopt -a -o dynlink.cmxa dynlink.ml + sudo cp -i dynlink.cmxa `ocamlopt -where` + + Then build coq this way: ./configure -natdynlink no && make world +*) + +let is_native = true (* This file will only be given to the native compiler *) + +type linking_error = +| Undefined_global of string +| Unavailable_primitive of string +| Uninitialized_global of string + +type error = +| Not_a_bytecode_file of string +| Inconsistent_import of string +| Unavailable_unit of string +| Unsafe_file +| Linking_error of string * linking_error +| Corrupted_interface of string +| File_not_found of string +| Cannot_open_dll of string +| Inconsistent_implementation of string + +exception Error of error + +let error_message = function + | Not_a_bytecode_file s -> "Native dynamic link not supported (module "^s^")" + | _ -> "Native dynamic link not supported" + +let loadfile : string -> unit = fun s -> raise (Error (Not_a_bytecode_file s)) +let loadfile_private = loadfile + +let adapt_filename s = s + +let init () = () +let allow_only : string list -> unit = fun _ -> () +let prohibit : string list -> unit = fun _ -> () +let default_available_units : unit -> unit = fun _ -> () +let allow_unsafe_modules : bool -> unit = fun _ -> () +let add_interfaces : string list -> string list -> unit = fun _ _ -> () +let add_available_units : (string * Digest.t) list -> unit = fun _ -> () +let clear_available_units : unit -> unit = fun _ -> () +let digest_interface : string -> string list -> Digest.t = + fun _ _ -> failwith "digest_interface" diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 0ed205350..793522f84 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -299,26 +299,6 @@ let extra_rules () = begin mlp_cmo "tools/compat5b"; end; -(** Special case of toplevel/mltop.ml4: - - mltop.ml will be the old mltop.optml and be used to obtain mltop.cmx - - we add a special mltop.ml4 --> mltop.cmo rule, before all the others -*) - flag ["is_mltop"; "p4option"] flag_dynlink; - -(*TODO: this is rather ugly for a simple file, we should try to - benefit more from predefined rules *) - let mltop = "toplevel/mltop" in - let ml4 = mltop^".ml4" and mlo = mltop^".cmo" and - ml = mltop^".ml" and mld = mltop^".ml.depends" - in - rule "mltop_byte" ~deps:[ml4;mld] ~prod:mlo ~insert:`top - (fun env build -> - Ocaml_compiler.prepare_compile build ml; - Cmd (S [!Options.ocamlc; A"-c"; A"-pp"; - Quote (S [camlp4o; T(tags_of_pathname ml4 ++ "p4mod"); - A"-DByte";A"-DHasDynlink";camlp4compat;A"-impl"]); - camlp4incl; incl ml4; A"-impl"; P ml4])); - (** All caml files are compiled with +camlp4/5 and ide files need +lablgtk2 *) diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml index 09dd2a67f..2ca3a4cd7 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml @@ -37,6 +37,14 @@ open System (I do not know of a solution to this problem, other than to put all the needed names into the ML Module object.) *) + +(* NB: this module relies on OCaml's Dynlink library. The bytecode version + of Dynlink is always available, but there are some architectures + with native compilation and no dynlink.cmxa. Instead of nasty IFDEF's + here for hiding the calls to Dynlink, we now simply reject this rather + rare situation during ./configure, and give instructions there about how + to build a dummy dynlink.cmxa, cf. dev/dynlink.ml. *) + (* This path is where we look for .cmo *) let coq_mlpath_copy = ref ["."] let keep_copy_mlpath path = @@ -61,7 +69,7 @@ type kind_load = let load = ref WithoutTop (* Are we in a native version of Coq? *) -let is_native = IFDEF Byte THEN false ELSE true END +let is_native = Dynlink.is_native (* Sets and initializes a toplevel (if any) *) let set_top toplevel = load := WithTop toplevel @@ -76,7 +84,7 @@ let is_ocaml_top () = |_ -> false (* Tests if we can load ML files *) -let has_dynlink = IFDEF HasDynlink THEN true ELSE false END +let has_dynlink = Coq_config.has_natdynlink || not is_native (* Runs the toplevel loop of Ocaml *) let ocaml_toploop () = @@ -93,23 +101,13 @@ let dir_ml_load s = | (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u | _ -> errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++ str s ++ str" to Coq code.")) -(* TO DO: .cma loading without toplevel *) | WithoutTop -> - 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. - *) let warn = Flags.is_verbose() in let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in try Dynlink.loadfile gname; - with | Dynlink.Error a -> + with Dynlink.Error a -> errorlabstrm "Mltop.load_object" (str (Dynlink.error_message a)) - 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 = |