From ccfcc920b2136ab056d676a99618b9f2dde6b78f Mon Sep 17 00:00:00 2001 From: pboutill Date: Fri, 7 Jan 2011 14:26:26 +0000 Subject: Coqide is not built with coqmktop any more git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13777 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile.build | 13 ++++++------- Makefile.common | 9 +++++++++ ide/coqide_main.ml | 1 + scripts/coqmktop.ml | 25 ++++--------------------- 4 files changed, 20 insertions(+), 28 deletions(-) create mode 100644 ide/coqide_main.ml diff --git a/Makefile.build b/Makefile.build index e6227aea6..feb09fd57 100644 --- a/Makefile.build +++ b/Makefile.build @@ -245,7 +245,6 @@ scripts/tolink.ml: Makefile.build Makefile.common $(HIDE)echo "let copts = \"-cclib -lcoqrun\"" > $@ $(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@ $(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@ - $(HIDE)echo "let ide = \""$(IDEMOD)"\"" >> $@ # coqc @@ -308,14 +307,14 @@ coqide-byte: $(COQIDEBYTE) $(COQIDE) coqide-opt: $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE) coqide-files: $(IDEFILES) -$(COQIDEOPT): $(COQTOPOPT) $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) ide/ide.cmxa - $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -ide -opt $(OPTFLAGS) -o $@ +$(COQIDEOPT): $(LINKIDEOPT) $(LIBCOQRUN) $(COQTOPOPT) + $(SHOW)'OCAMLOPT -o $@' + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa gtkThread.cmx dynlink.cmxa str.cmxa $(CAMLP4MOD).cmxa $(LIBCOQRUN) $(LINKIDEOPT) $(STRIP) $@ -$(COQIDEBYTE): $(COQTOPBYTE) $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) ide/ide.cma - $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -g -ide -top $(BYTEFLAGS) -o $@ +$(COQIDEBYTE): $(LINKIDE) $(LIBCOQRUN) $(COQTOPBYTE) + $(SHOW)'OCAMLOPT -o $@' + $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma gtkThread.cmo dynlink.cma str.cma $(CAMLP4MOD).cma $(COQRUNBYTEFLAGS) $(LIBCOQRUN) $(LINKIDE) $(COQIDE): cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE) diff --git a/Makefile.common b/Makefile.common index 95063aa2f..9e45758c4 100644 --- a/Makefile.common +++ b/Makefile.common @@ -29,6 +29,12 @@ CHICKENOPT:=bin/coqchk.opt$(EXE) BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE) CHICKEN:=bin/coqchk$(EXE) +ifeq ($(CAMLP4),camlp4) +CAMLP4MOD:=camlp4lib +else +CAMLP4MOD:=gramlib +endif + ifneq ($(HASNATDYNLINK),false) DYNLINKCMXA:=dynlink.cmxa NATDYNLINKDEF:=-DHasDynlink @@ -213,6 +219,9 @@ LINKCMX:=$(CONFIG:.cmo=.cmx) $(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa) IDECMA:=ide/ide.cma +LINKIDE:=$(LINKCMO) $(IDECMA) ide/coqide_main.ml +LINKIDEOPT:=$(LINKCMX) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml + # modules known by the toplevel of Coq OBJSMOD:=Coq_config $(shell cat $(CORECMA:.cma=.mllib)) diff --git a/ide/coqide_main.ml b/ide/coqide_main.ml new file mode 100644 index 000000000..52c956c3c --- /dev/null +++ b/ide/coqide_main.ml @@ -0,0 +1 @@ +let () = Coqide.start () diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index d4a76b6cc..0ff487fb4 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -27,7 +27,6 @@ let split_list l = Str.split spaces l let copts = split_list Tolink.copts let core_objs = split_list Tolink.core_objs let core_libs = split_list Tolink.core_libs -let ide = split_list Tolink.ide (* 3. Toplevel objects *) let camlp4topobjs = @@ -51,12 +50,10 @@ let opt = ref false let full = ref false let top = ref false let searchisos = ref false -let coqide = ref false let echo = ref false let src_dirs () = - [ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ] @ - if !coqide then [[ "ide" ]] else [] + [ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ] let includes () = let coqlib = Envars.coqlib () in @@ -65,8 +62,7 @@ let includes () = (fun d l -> "-I" :: ("\"" ^ List.fold_left Filename.concat coqlib d ^ "\"") :: l) (src_dirs ()) (["-I"; "\"" ^ camlp4lib ^ "\""] @ - ["-I"; "\"" ^ coqlib ^ "\""] @ - (if !coqide then ["-thread"; "-I"; "+lablgtk2"] else [])) + ["-I"; "\"" ^ coqlib ^ "\""]) (* Transform bytecode object file names in native object file names *) let native_suffix f = @@ -92,18 +88,10 @@ let files_to_link userfiles = 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 "Threads"::"Lablgtk"::"GtkThread"::ide else [] - in - let ide_libs = - if !coqide then - ["threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ; "ide/ide.cma" ] - else [] - in - let objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs @ ide_objs in + let objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs in let modules = List.map module_of_file (objs @ userfiles) in - let libs = dyn_objs @ libobjs @ core_libs @ toplevel_objs @ ide_libs in + let libs = dyn_objs @ libobjs @ core_libs @ toplevel_objs in let libstolink = (if !opt then List.map native_suffix libs else libs) @ userfiles in @@ -143,7 +131,6 @@ let usage () = \n -o exec-file Specify the name of the resulting toplevel\ \n -boot Run in boot mode\ \n -echo Print calls to external commands\ -\n -ide Build a toplevel for the Coq IDE\ \n -full Link high level tactics\ \n -opt Compile in native code\ \n -searchisos Build a toplevel for SearchIsos\ @@ -169,8 +156,6 @@ let parse_args () = | "-opt" :: rem -> opt := true ; parse (op,fl) rem | "-full" :: rem -> full := true ; parse (op,fl) rem | "-top" :: rem -> top := true ; parse (op,fl) rem - | "-ide" :: rem -> - coqide := true; parse (op,fl) rem | "-v8" :: rem -> Printf.eprintf "warning: option -v8 deprecated"; parse (op,fl) rem @@ -257,8 +242,6 @@ let create_tmp_main_file modules = (* Start the right toplevel loop: Coq or Coq_searchisos *) if !searchisos then output_string oc "Cmd_searchisos_line.start();;\n" - else if !coqide then - output_string oc "Coqide.start();;\n" else output_string oc "Coqtop.start();;\n"; close_out oc; -- cgit v1.2.3