From b2dd4dd979577e4f384750872f7f0e7f9bd8df94 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 5 Jul 2016 18:22:53 +0200 Subject: Revert "Merge remote-tracking branch 'github/pr/229' into trunk" This reverts commit b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385, reversing changes made to da99355b4d6de31aec5a660f7afe100190a8e683. Hugo asked for more discussion on this topic, and it was not in the roadmap. I merged it prematurely because I thought there was a consensus. Also, I missed that it was changing coq_makefile. Sorry about that. --- INSTALL | 36 ++++++++------------------ Makefile | 7 ++--- Makefile.build | 57 +++++++++++++++++++++++++++-------------- Makefile.checker | 2 +- Makefile.common | 22 +++------------- Makefile.ide | 45 ++++++++++++-------------------- Makefile.install | 22 +++++----------- plugins/micromega/sos_types.mli | 40 ----------------------------- tools/coq_makefile.ml | 50 ++++++++++-------------------------- tools/coqdep.ml | 24 +++++------------ tools/coqdep_boot.ml | 6 +---- tools/coqdep_common.ml | 20 +++++---------- tools/coqdep_common.mli | 5 +--- tools/coqdoc/cdglobals.mli | 49 ----------------------------------- 14 files changed, 105 insertions(+), 280 deletions(-) delete mode 100644 plugins/micromega/sos_types.mli delete mode 100644 tools/coqdoc/cdglobals.mli diff --git a/INSTALL b/INSTALL index 56ff522dc..5a300010d 100644 --- a/INSTALL +++ b/INSTALL @@ -55,6 +55,8 @@ QUICK INSTALLATION PROCEDURE. 1. ./configure 2. make 3. make install (you may need superuser rights) +4. make clean + INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). ================================================= @@ -130,13 +132,10 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). make - to compile Coq in the best OCaml mode available (native-code if supported, - bytecode otherwise). + to compile Coq in Objective Caml bytecode (and native-code if supported). This will compile the entire system. This phase can take more or less time, - depending on your architecture and is fairly verbose. On a multi-core machine, - it is recommended to compile in parallel, via make -jN where N is your number - of cores. + depending on your architecture and is fairly verbose. 6- You can now install the Coq system. Executables, libraries, manual pages and emacs mode are copied in some standard places of your system, defined at @@ -152,19 +151,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) -7- Optionally, you could build the bytecode version of Coq via: - - make byte - - and install it via - - make install-byte - - This version is quite slower than the native code version of Coq, but could - be helpful for debugging purposes. In particular, coqtop.byte embeds an OCaml - toplevel accessible via the Drop command. - -8- You can now clean all the sources. (You can even erase them.) +7- You can now clean all the sources. (You can even erase them.) make clean @@ -202,14 +189,11 @@ THE AVAILABLE COMMANDS. coqtop The Coq toplevel coqc The Coq compiler - Under architecture where ocamlopt is available, coqtop is the native code - version of Coq. On such architecture, you could additionally request - the build of the bytecode version of Coq via 'make byte' and install it via - 'make install-byte'. This will create an extra binary named coqtop.byte, - that could be used for debugging purpose. If native code isn't available, - coqtop.byte is directly built by 'make', and coqtop is a link to coqtop.byte. - coqc also invokes the fastest version of Coq. Options -opt and -byte to coqtop - and coqc selects a particular binary. + Under architecture where ocamlopt is available, there are actually two + binaries for the interactive system, coqtop.byte and coqtop (respectively + bytecode and native code versions of Coq). coqtop is a link to coqtop.byte + otherwise. coqc also invokes the fastest version of Coq. Options -opt and + -byte to coqtop and coqc selects a particular binary. * `coqtop' launches Coq in the interactive mode. By default it loads basic logical definitions and tactics from the Init directory. diff --git a/Makefile b/Makefile index db23ad0a8..93b89a489 100644 --- a/Makefile +++ b/Makefile @@ -109,17 +109,14 @@ NOARG: world .PHONY: NOARG help noconfig submake help: - @echo "Please use either:" + @echo "Please use either" @echo " ./configure" @echo " make world" @echo " make install" @echo " make clean" @echo "or make archclean" + @echo @echo "For make to be verbose, add VERBOSE=1" - @echo "Bytecode compilation is now a separate target:" - @echo " make byte" - @echo " make install-byte" - @echo "Please do mix bytecode and native targets in the same make -j" UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.ml?') ifdef UNSAVED_FILES diff --git a/Makefile.build b/Makefile.build index 90834ec8c..ebf2996f1 100644 --- a/Makefile.build +++ b/Makefile.build @@ -17,16 +17,9 @@ world: coq coqide documentation revision -coq: coqlib coqbinaries tools +coq: coqlib coqbinaries tools printers -# Note: 'world' do not build the bytecode binaries anymore. -# For that, you can use the 'byte' rule. Native and byte compilations -# shouldn't be done in a same make -j... run, otherwise both ocamlc and -# ocamlopt might race for access to the same .cmi files. - -byte: coqbyte coqide-byte pluginsbyte printers - -.PHONY: world coq byte +.PHONY: world coq ########################################################################### # Includes @@ -91,7 +84,7 @@ STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)" TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) COQOPTS=$(COQ_XML) $(NATIVECOMPUTE) -BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile +BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile # The SHOW and HIDE variables control whether make will echo complete commands # or only abbreviated versions. @@ -181,7 +174,7 @@ ifndef ORDER_ONLY_SEP $(error This Makefile needs GNU Make 3.81 or later (that is a version that supports the order-only dependency feature without major bugs.)) endif -VO_TOOLS_DEP := $(COQTOPBEST) +VO_TOOLS_DEP := $(COQTOPEXE) ifdef COQ_XML VO_TOOLS_DEP += $(COQDOC) endif @@ -320,11 +313,11 @@ grammar/%.cmi: grammar/%.mli # Main targets (coqmktop, coqtop.opt, coqtop.byte) ########################################################################### -.PHONY: coqbinaries coqbyte +.PHONY: coqbinaries -coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) +coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(COQTOPBYTE) \ + $(CHICKEN) $(CHICKENBYTE) $(CSDPCERT) $(FAKEIDE) -coqbyte: $(COQTOPBYTE) $(CHICKENBYTE) ifeq ($(BEST),opt) $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) @@ -510,13 +503,18 @@ test-suite: world $(ALLSTDLIB).v # For plugin packs +# Note: both ocamlc -pack and ocamlopt -pack will create the same .cmi, and there's +# apparently no way to avoid that (no -intf-suffix hack as below). +# We at least ensure that these two commands won't run at the same time, by a fake +# dependency from the packed .cmx to the packed .cmo. + %.cmo: %.mlpack $(SHOW)'OCAMLC -pack -o $@' $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -pack -o $@ $(filter-out %.mlpack, $^) -%.cmx: %.mlpack +%.cmx: %.mlpack %.cmo $(SHOW)'OCAMLOPT -pack -o $@' - $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^) + $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack %.cmo, $^) COND_BYTEFLAGS= \ $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(BYTEFLAGS) @@ -532,6 +530,27 @@ COND_OPTFLAGS= \ $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $< +## NB: for the moment ocamlopt erases and recreates .cmi if there's no .mli around. +## This can lead to nasty things with make -j. To avoid that: +## 1) We make .cmx always depend on .cmi +## 2) This .cmi will be created from the .mli, or trigger the compilation of the +## .cmo if there's no .mli (see rule below about MLWITHOUTMLI) +## 3) We tell ocamlopt to use the .cmi as the interface source file. With this +## hack, everything goes as if there is a .mli, and the .cmi is preserved +## and the .cmx is checked with respect to this .cmi + +HACKMLI = $(if $(wildcard $ term -> unit - -type positivstellensatz = - Axiom_eq of int - | Axiom_le of int - | Axiom_lt of int - | Rational_eq of Num.num - | Rational_le of Num.num - | Rational_lt of Num.num - | Square of term - | Monoid of int list - | Eqmul of term * positivstellensatz - | Sum of positivstellensatz * positivstellensatz - | Product of positivstellensatz * positivstellensatz;; - -val output_psatz : out_channel -> positivstellensatz -> unit diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index f116c5580..c86253477 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -293,8 +293,9 @@ let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function let cmxss = List.rev_append cmos mllibs in let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxss)] inc in let where_what_oth = vars_to_put_by_root - [("VOFILES",vfiles);("VFILES",vfiles);("GLOBFILES",vfiles); - ("NATIVEFILES",vfiles);("CMIFILES",cmis)] + [("VOFILES",vfiles);("VFILES",vfiles); + ("GLOBFILES",vfiles);("NATIVEFILES",vfiles); + ("CMOFILES",cmos);("CMIFILES",cmis);("CMAFILES",mllibs)] inc in let doc_dir = where_put_doc inc in if is_install = Project_file.UnspecInstall then begin @@ -305,12 +306,6 @@ let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function install_include_by_root "0755" where_what_cmxs; print "\n"; end; - if not_empty cmxss then begin - print "install-byte:\n"; - install_include_by_root "0755" - (vars_to_put_by_root [("CMOFILES",cmos);("CMAFILES",mllibs)] inc); - print "\n"; - end; if not_empty cmxss then begin print "install-toploop: $(MLLIBFILES:.mllib=.cmxs)\n"; printf "\t install -d \"$(DSTROOT)\"$(COQTOPINSTALL)/\n"; @@ -511,7 +506,7 @@ let variables is_install opt (args,defs) = end; (* Coq executables and relative variables *) if !some_vfile || !some_mlpackfile || !some_mllibfile then - print "COQDEP?=\"$(COQBIN)coqdep\" -c -dyndep var\n"; + print "COQDEP?=\"$(COQBIN)coqdep\" -c\n"; if !some_vfile then begin print "COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n"; print "COQCHKFLAGS?=-silent -o\n"; @@ -542,16 +537,7 @@ else CAMLP4EXTEND= endif\n"; print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\ - $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n"; - print "ifeq '$(OPT)' '-byte'\n"; - print "USEBYTE:=true\n"; - print "DYNOBJ:=.cmo\n"; - print "DYNLIB:=.cma\n"; - print "else\n"; - print "USEBYTE:=\n"; - print "DYNOBJ:=.cmxs\n"; - print "DYNLIB:=.cmxs\n"; - print "endif\n\n"; + $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; end; match is_install with | Project_file.NoInstall -> () @@ -770,19 +756,13 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other print "HASNATDYNLINK_OR_EMPTY :=\n"; print "endif\n\n"; section "Definition of the toplevel targets."; - let has_cmo = !some_mlfile || !some_ml4file || !some_mlpackfile in - let has_ml = has_cmo || !some_mllibfile in - print "all:"; - if !some_vfile then print " $(VOFILES)"; - if has_ml then print " $(if $(USEBYTE),bytefiles,optfiles)"; + print "all: "; + if !some_vfile then print "$(VOFILES) "; + if !some_mlfile || !some_ml4file || !some_mlpackfile then print "$(CMOFILES) "; + if !some_mllibfile then print "$(CMAFILES) "; + if !some_mlfile || !some_ml4file || !some_mllibfile || !some_mlpackfile + then print "$(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) "; print_list "\\\n " other_targets; print "\n\n"; - print "bytefiles:"; - if has_cmo then print " $(CMOFILES)"; - if !some_mllibfile then print " $(CMAFILES)"; - print "\n\n"; - print "optfiles:"; - if has_ml then print " $(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES))"; - print "\n\n"; if !some_mlifile then begin print "mlihtml: $(MLIFILES:.mli=.cmi)\n"; @@ -828,11 +808,9 @@ let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc = print ".PHONY: "; print_list " " - ("all" :: "archclean" :: "beautify" :: "byte" :: "bytefiles" - :: "clean" :: "cleanall" - :: "gallina" :: "gallinahtml" :: "html" :: "install" :: "install-byte" - :: "install-doc" :: "install-natdynlink" :: "install-toploop" - :: "opt" :: "optfiles" :: "printenv" + ("all" :: "archclean" :: "beautify" :: "byte" :: "clean" :: "cleanall" + :: "gallina" :: "gallinahtml" :: "html" :: "install" :: "install-doc" + :: "install-natdynlink" :: "install-toploop" :: "opt" :: "printenv" :: "quick" :: "uninstall" :: "userinstall" :: "validate" :: "vio2vo" :: (sds@(CList.map_filter (fun (n,_,is_phony,_) -> diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 991a3221f..a7c32e1d6 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -320,25 +320,19 @@ let treat_coq_file chan = List.fold_left (fun accu v -> mark_v_done from accu v) acc strl | Declare sl -> let declare suff dir s = - let base = escape (file_name s dir) in - match !option_dynlink with - | No -> [] - | Byte -> [base,suff] - | Opt -> [base,".cmxs"] - | Both -> [base,suff; base,".cmxs"] - | Variable -> - if suff=".cmo" then [base,"$(DYNOBJ)"] - else [base,"$(DYNLIB)"] + let base = file_name s dir in + let opt = if !option_natdynlk then " " ^ base ^ ".cmxs" else "" in + (escape base, suff ^ opt) in let decl acc str = let s = basename_noext str in if not (StrSet.mem s !deja_vu_ml) then let () = deja_vu_ml := StrSet.add s !deja_vu_ml in match search_mllib_known s with - | Some mldir -> (declare ".cma" mldir s) @ acc + | Some mldir -> (declare ".cma" mldir s) :: acc | None -> match search_ml_known s with - | Some mldir -> (declare ".cmo" mldir s) @ acc + | Some mldir -> (declare ".cmo" mldir s) :: acc | None -> acc else acc in @@ -455,7 +449,6 @@ let usage () = eprintf " -coqlib dir : set the coq standard library directory\n"; eprintf " -suffix s : \n"; eprintf " -slash : deprecated, no effect\n"; - eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed"; exit 1 let split_period = Str.split (Str.regexp (Str.quote ".")) @@ -483,22 +476,17 @@ let rec parse = function | "-slash" :: ll -> Printf.eprintf "warning: option -slash has no effect and is deprecated.\n"; parse ll - | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll - | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll - | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll - | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll - | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll | ("-h"|"--help"|"-help") :: _ -> usage () | f :: ll -> treat_file None f; parse ll | [] -> () let coqdep () = if Array.length Sys.argv < 2 then usage (); - if not Coq_config.has_natdynlink then option_dynlink := No; parse (List.tl (Array.to_list Sys.argv)); (* Add current dir with empty logical path if not set by options above. *) (try ignore (Coqdep_common.find_dir_logpath (Sys.getcwd())) with Not_found -> add_norec_dir_import add_known "." []); + if not Coq_config.has_natdynlink then option_natdynlk := false; (* NOTE: These directories are searched from last to first *) if !option_boot then begin add_rec_dir_import add_known "theories" ["Coq"]; diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index 25f62d2be..6fc826833 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -16,11 +16,7 @@ open Coqdep_common *) let rec parse = function - | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll - | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll - | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll - | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll - | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll + | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll | "-c" :: ll -> option_c := true; parse ll | "-boot" :: ll -> parse ll (* We're already in boot mode by default *) | "-mldep" :: ocamldep :: ll -> diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 8bf7fee4b..cc63c13d7 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -15,7 +15,7 @@ open Minisys behavior is the one of [coqdep -boot]. Its only dependencies are [Coqdep_lexer], [Unix] and [Minisys], and it should stay so. If it need someday some additional information, pass it via - options (see for instance [option_dynlink] below). + options (see for instance [option_natdynlk] below). *) module StrSet = Set.Make(String) @@ -26,11 +26,9 @@ module StrListMap = Map.Make(StrList) let stderr = Pervasives.stderr let stdout = Pervasives.stdout -type dynlink = Opt | Byte | Both | No | Variable - let option_c = ref false let option_noglob = ref false -let option_dynlink = ref Both +let option_natdynlk = ref true let option_boot = ref false let option_mldep = ref None @@ -382,16 +380,10 @@ let rec traite_fichier_Coq suffixe verbose f = end) strl | Declare sl -> let declare suff dir s = - let base = escape (file_name s dir) in - match !option_dynlink with - | No -> () - | Byte -> printf " %s%s" base suff - | Opt -> printf " %s.cmxs" base - | Both -> printf " %s%s %s.cmxs" base suff base - | Variable -> - printf " %s%s" base - (if suff=".cmo" then "$(DYNOBJ)" else "$(DYNLIB)") - in + let base = file_name s dir in + let opt = if !option_natdynlk then " "^base^".cmxs" else "" in + printf " %s%s%s" (escape base) suff opt + in let decl str = let s = basename_noext str in if not (StrSet.mem s !deja_vu_ml) then begin diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 205e99176..633c474ad 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -19,10 +19,7 @@ val find_dir_logpath: string -> string list val option_c : bool ref val option_noglob : bool ref val option_boot : bool ref - -type dynlink = Opt | Byte | Both | No | Variable - -val option_dynlink : dynlink ref +val option_natdynlk : bool ref val option_mldep : string option ref val norec_dirs : StrSet.t ref val suffixe : string ref diff --git a/tools/coqdoc/cdglobals.mli b/tools/coqdoc/cdglobals.mli deleted file mode 100644 index 2c9b3fb8e..000000000 --- a/tools/coqdoc/cdglobals.mli +++ /dev/null @@ -1,49 +0,0 @@ -type target_language = LaTeX | HTML | TeXmacs | Raw -val target_language : target_language ref -type output_t = StdOut | MultFiles | File of string -val output_dir : string ref -val out_to : output_t ref -val out_channel : out_channel ref -val ( / ) : string -> string -> string -val coqdoc_out : string -> string -val open_out_file : string -> unit -val close_out_file : unit -> unit -type glob_source_t = NoGlob | DotGlob | GlobFile of string -val glob_source : glob_source_t ref -val normalize_path : string -> string -val normalize_filename : string -> string * string -val guess_coqlib : unit -> string -val header_trailer : bool ref -val header_file : string ref -val header_file_spec : bool ref -val footer_file : string ref -val footer_file_spec : bool ref -val quiet : bool ref -val light : bool ref -val gallina : bool ref -val short : bool ref -val index : bool ref -val multi_index : bool ref -val index_name : string ref -val toc : bool ref -val page_title : string ref -val title : string ref -val externals : bool ref -val coqlib : string ref -val coqlib_path : string ref -val raw_comments : bool ref -val parse_comments : bool ref -val plain_comments : bool ref -val toc_depth : int option ref -val lib_name : string ref -val lib_subtitles : bool ref -val interpolate : bool ref -val inline_notmono : bool ref -val charset : string ref -val inputenc : string ref -val latin1 : bool ref -val utf8 : bool ref -val set_latin1 : unit -> unit -val set_utf8 : unit -> unit -type coq_module = string -type file = Vernac_file of string * coq_module | Latex_file of string -- cgit v1.2.3