Permalink
Browse files

Coqmktop without Sys.command, changes in ./configure -*byteflags options

NB: Please re-run ./configure after pulling this commit

 For launching ocamlc/ocamlopt, coqmktop doesn't use Sys.command anymore,
 but rather CUnix.sys_command, which is based on Unix.create_process.
 This way, we do not need to bother with the underlying shell
 (/bin/sh or cmd.exe) and the way arguments are to be quoted :-).
 Btw, many cleanups of coqmktop.

 Only difficulty: the -coqrunbyteflags of ./configure is a "meta-option"
 that collect as a string several sub-options to be given by coqmktop to ocamlc.
 For instance ./configure -coqrunbyteflags "-dllib -lcoqrun". We need now to
 parse all these sub-options. To ease that, I've made the following changes
 to the ./configure options:

 * The -coqrunbyteflags and its blank-separated argument isn't accepted
   anymore, and is replaced by a new option -vmbyteflags which expects
   a comma-separated argument. For instance:

   ./configure -vmbyteflags "-dllib,-lcoqrun"

   Btw, on this example, the double-quotes aren't mandatory anymore :-)

 * The -coqtoolsbyteflags isn't accepted anymore. To the best of my
   knowledge, nobody ever used it directly (it was internally triggered
   as a byproduct of the -custom option). The only interest I can think of
   for this option was to cancel the default use of ocamlc custom-linking
   on Win32 and MacOS. For that, ./configure now provides a -no-custom option.
  • Loading branch information...
1 parent 74bd95d commit c734ccd8081e52ee5576d0efac9b065d4f37f7d5 @letouzey letouzey committed Jan 22, 2014
Showing with 227 additions and 215 deletions.
  1. +4 −0 CHANGES
  2. +1 −1 INSTALL
  3. +3 −3 Makefile.build
  4. +1 −1 config/coq_config.mli
  5. +42 −45 configure.ml
  6. +3 −3 myocamlbuild.ml
  7. +173 −162 tools/coqmktop.ml
View
@@ -105,6 +105,10 @@ Internal Infrastructure
an executable compiled with the best OCaml compiler available.
The bytecode program coqtop.byte is still produced. Same for other
utilities.
+- Some options of the ./configure script slightly changed:
+ * The -coqrunbyteflags and its blank-separated argument is replaced
+ by option -vmbyteflags which expects a comma-separated argument.
+ * The -coqtoolsbyteflags option is discontinued, see -no-custom instead.
Changes from V8.4beta2 to V8.4
==============================
View
@@ -315,7 +315,7 @@ DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES.
the directory of the standard library of OCaml;
- recompile your bytecode executables after reconfiguring the location of
of the shared library:
- ./configure -coqrunbyteflags "-dllib -lcoqrun -dllpath <path>" ...
+ ./configure -vmbyteflags "-dllib,-lcoqrun,-dllpath,<path>" ...
where <path> is the directory where the dllcoqrun.so is installed;
- (not recommended) compile bytecode executables with a custom OCaml
runtime by using:
View
@@ -113,7 +113,7 @@ DEPFLAGS= $(LOCALINCLUDES)
define bestocaml
$(if $(OPT),\
$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@,\
-$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(1) $(addsuffix .cma,$(2)) $^)
+$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ $(1) $(addsuffix .cma,$(2)) $^)
endef
CAMLP4DEPS=$(shell LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $(1) \#))
@@ -247,7 +247,7 @@ endif
$(CHICKENBYTE): checker/check.cma checker/main.ml
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -thread $(COQTOOLSBYTEFLAGS) -o $@ $(SYSCMA) $^
+ $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -thread -o $@ $(SYSCMA) $^
# coqmktop
$(COQMKTOP): $(patsubst %.cma,%$(BESTLIB),$(COQMKTOPCMO:.cmo=$(BESTOBJ)))
@@ -636,7 +636,7 @@ install-library:
$(MKDIR) $(FULLCOQLIB)
$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS)
$(MKDIR) $(FULLCOQLIB)/user-contrib
-ifneq ($(COQRUNBYTEFLAGS),"-custom")
+ifndef CUSTOM
$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
endif
ifeq ($(BEST),opt)
@@ -38,7 +38,7 @@ val best : string (* byte/opt *)
val arch : string (* architecture *)
val arch_is_win32 : bool
val osdeplibs : string (* OS dependant link options for ocamlc *)
-val coqrunbyteflags : string (* -custom/-dllib -lcoqrun *)
+val vmbyteflags : string list (* -custom/-dllib -lcoqrun *)
(* val defined : string list (* options for lib/ocamlpp *) *)
View
@@ -208,9 +208,8 @@ let arg_string_option r = Arg.String (fun s -> r := Some s)
module Prefs = struct
let prefix = ref (None : string option)
let local = ref false
- let coqrunbyteflags = ref (None : string option)
- let coqtoolsbyteflags = ref (None : string option)
- let custom = ref false
+ let vmbyteflags = ref (None : string option)
+ let custom = ref (None : bool option)
let bindir = ref (None : string option)
let libdir = ref (None : string option)
let configdir = ref (None : string option)
@@ -248,12 +247,12 @@ let args_options = Arg.align [
"<dir> Set installation directory to <dir>";
"-local", Arg.Set Prefs.local,
" Set installation directory to the current source tree";
- "-coqrunbyteflags", arg_string_option Prefs.coqrunbyteflags,
- "<flags> Set link flags for VM-dependent bytecode (coqtop)";
- "-coqtoolsbyteflags", arg_string_option Prefs.coqtoolsbyteflags,
- "<flags> Set link flags for VM-independant bytecode (coqdep,coqdoc,...)";
- "-custom", Arg.Set Prefs.custom,
- " Generate all bytecode executables with -custom (not recommended)";
+ "-vmbyteflags", arg_string_option Prefs.vmbyteflags,
+ "<flags> Comma-separated link flags for the VM of coqtop.byte";
+ "-custom", Arg.Unit (fun () -> Prefs.custom := Some true),
+ " Build bytecode executables with -custom (not recommended)";
+ "-no-custom", Arg.Unit (fun () -> Prefs.custom := Some false),
+ " Do not build with -custom on Windows and MacOS";
"-bindir", arg_string_option Prefs.bindir,
"<dir> Where to install bin files";
"-libdir", arg_string_option Prefs.libdir,
@@ -284,7 +283,7 @@ let args_options = Arg.align [
" Specifies to use camlp4 instead of camlp5";
"-camlp5dir",
Arg.String (fun s -> Prefs.usecamlp5:=true; Prefs.camlp5dir:=Some s),
- "<dir> Specifies where to look for the Camlp5 library and tells to use it";
+ "<dir> Specifies where is the Camlp5 library and tells to use it";
"-arch", arg_string_option Prefs.arch,
"<arch> Specifies the architecture";
"-opt", Arg.Set Prefs.opt,
@@ -316,7 +315,7 @@ let args_options = Arg.align [
"-makecmd", Arg.Set_string Prefs.makecmd,
"<command> Name of GNU Make command";
"-no-native-compiler", Arg.Clear Prefs.nativecompiler,
- " Disables compilation to native code for conversion and normalization";
+ " No compilation to native code for conversion and normalization";
"-coqwebsite", Arg.Set_string Prefs.coqwebsite,
" URL of the coq website";
"-force-caml-version", arg_bool Prefs.force_caml_version,
@@ -855,60 +854,59 @@ let datadir =
(** * OCaml runtime flags *)
-(** Determine if we enable -custom by default (Windows and MacOS) *)
+(** Do we use -custom (yes by default on Windows and MacOS) *)
+
let custom_os = arch_win32 || arch = "Darwin"
+let use_custom = match !Prefs.custom with
+ | Some b -> b
+ | None -> custom_os
+
+let custom_flag = if use_custom then "-custom" else ""
+
let build_loadpath =
ref "# you might want to set CAML_LD_LIBRARY_PATH by hand!"
let config_runtime () =
- match !Prefs.coqrunbyteflags with
- | Some flags -> flags
- | _ when !Prefs.custom || custom_os -> "-custom"
+ match !Prefs.vmbyteflags with
+ | Some flags -> string_split ',' flags
+ | _ when use_custom -> [custom_flag]
| _ when !Prefs.local ->
- sprintf "-dllib -lcoqrun -dllpath '%s/kernel/byterun'" coqtop
+ ["-dllib";"-lcoqrun";"-dllpath";coqtop/"kernel/byterun"]
| _ ->
let ld="CAML_LD_LIBRARY_PATH" in
build_loadpath := sprintf "export %s:='%s/kernel/byterun':$(%s)" ld coqtop ld;
- sprintf "-dllib -lcoqrun -dllpath '%s'" libdir
-
-let coqrunbyteflags = config_runtime ()
-
-let config_tools_runtime () =
- match !Prefs.coqtoolsbyteflags with
- | Some flags -> flags
- | _ when !Prefs.custom || custom_os -> "-custom"
- | _ -> ""
+ ["-dllib";"-lcoqrun";"-dllpath";libdir]
-let coqtoolsbyteflags = config_tools_runtime ()
+let vmbyteflags = config_runtime ()
(** * Summary of the configuration *)
let print_summary () =
let pr s = printf s in
pr "\n";
- pr " Architecture : %s\n" arch;
+ pr " Architecture : %s\n" arch;
if operating_system <> "" then
- pr " Operating system : %s\n" operating_system;
- pr " Coq VM bytecode link flags : %s\n" coqrunbyteflags;
- pr " Coq tools bytecode link flags : %s\n" coqtoolsbyteflags;
- pr " OS dependent libraries : %s\n" osdeplibs;
- pr " Objective-Caml/Camlp4 version : %s\n" caml_version;
- pr " Objective-Caml/Camlp4 binaries in : %s\n" camlbin;
- pr " Objective-Caml library in : %s\n" camllib;
- pr " Camlp4 library in : %s\n" camlp4lib;
+ pr " Operating system : %s\n" operating_system;
+ pr " Coq VM bytecode link flags : %s\n" (String.concat " " vmbyteflags);
+ pr " Other bytecode link flags : %s\n" custom_flag;
+ pr " OS dependent libraries : %s\n" osdeplibs;
+ pr " OCaml/Camlp4 version : %s\n" caml_version;
+ pr " OCaml/Camlp4 binaries in : %s\n" camlbin;
+ pr " OCaml library in : %s\n" camllib;
+ pr " Camlp4 library in : %s\n" camlp4lib;
if best_compiler = "opt" then
- pr " Native dynamic link support : %B\n" hasnatdynlink;
+ pr " Native dynamic link support : %B\n" hasnatdynlink;
if coqide <> "no" then
- pr " Lablgtk2 library in : %s\n" !lablgtkdir;
+ pr " Lablgtk2 library in : %s\n" !lablgtkdir;
if !idearchdef = "QUARTZ" then
pr " Mac OS integration is on\n";
- pr " CoqIde : %s\n" coqide;
- pr " Documentation : %s\n"
+ pr " CoqIde : %s\n" coqide;
+ pr " Documentation : %s\n"
(if withdoc then "All" else "None");
- pr " Web browser : %s\n" browser;
- pr " Coq web site : %s\n\n" !Prefs.coqwebsite;
+ pr " Web browser : %s\n" browser;
+ pr " Coq web site : %s\n\n" !Prefs.coqwebsite;
if not !Prefs.nativecompiler then
pr " Native compiler for conversion and normalization disabled\n\n";
if !Prefs.local then
@@ -961,7 +959,7 @@ let write_configml f =
pr "(* Exact command that generated this file: *)\n";
pr "(* %s *)\n\n" (String.concat " " (Array.to_list Sys.argv));
pr_b "local" !Prefs.local;
- pr_s "coqrunbyteflags" coqrunbyteflags;
+ pr "let vmbyteflags = ["; List.iter (pr "%S;") vmbyteflags; pr "]\n";
pr_o "coqlib" (if !Prefs.local then None else Some libdir);
pr_o "configdir" configdir;
pr_o "datadir" datadir;
@@ -1045,9 +1043,8 @@ let write_makefile f =
pr "COQ_CONFIGURED=yes\n\n";
pr "# Local use (no installation)\n";
pr "LOCAL=%B\n\n" !Prefs.local;
- pr "# Bytecode link flags for VM (\"-custom\" or \"-dllib -lcoqrun\")\n";
- pr "COQRUNBYTEFLAGS=%s\n" coqrunbyteflags;
- pr "COQTOOLSBYTEFLAGS=%s\n" coqtoolsbyteflags;
+ pr "# Bytecode link flags : should we use -custom or not ?\n";
+ pr "CUSTOM=%s\n" custom_flag;
pr "%s\n\n" !build_loadpath;
pr "# Paths for true installation\n";
List.iter (fun (v,msg,_,_) -> pr "# %s: path for %s\n" v msg) install_dirs;
View
@@ -259,9 +259,9 @@ let extra_rules () = begin
let lines = List.map (fun s -> s^"\n") lines in
let line0 = "\n(* Adapted variables for ocamlbuild *)\n" in
(* TODO : line2 isn't completely accurate with respect to ./configure:
- the case of -local -coqrunbyteflags foo isn't supported *)
+ the case of -local -vmbyteflags foo isn't supported *)
let line1 =
- "let coqrunbyteflags = \"-dllib -lcoqrun\"\n"
+ "let vmbyteflags = [\"-dllib\";\"-lcoqrun\"]\n"
in
Echo (lines @ (if local then [line0;line1] else []),
"coq_config.ml"));
@@ -316,7 +316,7 @@ let extra_rules () = begin
flag ["compile"; "c"] cflags;
dep ["ocaml"; "use_libcoqrun"; "compile"] [libcoqrun];
dep ["ocaml"; "use_libcoqrun"; "link"; "native"] [libcoqrun];
- flag ["ocaml"; "use_libcoqrun"; "link"; "byte"] (Sh Coq_config.coqrunbyteflags);
+ flag ["ocaml"; "use_libcoqrun"; "link"; "byte"] (Sh Coq_config.vmbyteflags);
(* we need to use a different ocamlc. For now we copy the rule *)
if w32 then
Oops, something went wrong.

0 comments on commit c734ccd

Please sign in to comment.