From 8d41b4a80e6b1a944772a435e2a8eb54adc3048c Mon Sep 17 00:00:00 2001 From: notin Date: Thu, 13 Nov 2008 17:12:27 +0000 Subject: Tentative d'amélioration de la robustesse des Makefile générés par coq_makefile en présence de fichiers .ml : MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - ajout d'une option -config à coqtop qui affiche les informations de configuration (COQTOP, COQBIN, COQLIB, CAMLP4, CAMLP4LIB, CAMLBIN, LOCAL) - coq_makefile inclut un fichier Makefile.config qui contient les valeurs des variables sus-mentionnées git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11584 85f007b7-540e-0410-9357-904b9bb8a0f7 --- scripts/coqc.ml | 3 +++ tools/coq_makefile.ml4 | 43 ++++++++++++++++--------------------------- toplevel/coqtop.ml | 2 ++ toplevel/usage.ml | 15 +++++++++++++++ toplevel/usage.mli | 3 +++ 5 files changed, 39 insertions(+), 27 deletions(-) diff --git a/scripts/coqc.ml b/scripts/coqc.ml index e661455ca..aa09219bf 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -164,6 +164,9 @@ let parse_args () = try Sys.getenv "COQLIB" with Not_found -> Coq_config.coqlib in print_endline coqlib; exit 0 + + | ("-config" | "--config") :: _ -> Usage.print_config (); exit 0 + | ("-v"|"--version") :: _ -> Usage.version () | f :: rem -> diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index b88cae064..e2ea8250d 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -89,6 +89,8 @@ let is_genrule r = Str.string_match genrule r 0 let standard sds sps = + print "Makefile.config:\n"; + print "\t$(COQBIN)/coqtop -config > $@\n\n"; print "byte:\n"; print "\t$(MAKE) all \"OPT:=-byte\"\n\n"; print "opt:\n"; @@ -113,9 +115,9 @@ let standard sds sps = print "\n"; end; print "clean:\n"; - print "\trm -f *.cmo *.cmi *.cmx *.o $(VOFILES) $(VIFILES) $(GFILES) *~\n"; + print "\trm -f *.cmo *.cmi *.cmx *.o $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~\n"; print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) \ - $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)\n"; + $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d) Makefile.config\n"; if !some_mlfile then print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d)\n"; print "\t- rm -rf html\n"; @@ -135,7 +137,10 @@ let standard sds sps = sds; print "\n\n" -let includes () = +let header_includes () = + print "include Makefile.config\n.PHONY: Makefile.config\n" + +let footer_includes () = if !some_vfile then print "-include $(VFILES:.v=.v.d)\n.SECONDARY: $(VFILES:.v=.v.d)\n\n"; if !some_mlfile then print "-include $(MLFILES:.ml=.ml.d)\n.SECONDARY: $(MLFILES:.ml=.ml.d)\n\n" @@ -218,11 +223,10 @@ let dir_of_target t = let parameters () = print "# \n"; - print "# Compilation looks in the path for coqtop; set COQBIN if coqtop is not in path\n"; - print "# if .ml files have to be compiled, set CAMLBIN if ocamlc is not in path\n"; - print "# if .ml files have to be compiled, set CAMLP4BIN if camlp4/5 is not in path\n"; - print "# \n"; - print "# set COQTOP to a Coq source directory for compiling over Coq compiled sources\n"; + print "# This Makefile looks for coqtop in PATH and in COQBIN to create Makefile.config\n"; + print "# Once created, Make refers to this file to determine the important paths for Coq\n"; + print "# and Caml binaries. To change which Coq is used to compile your contribution,\n"; + print "# delete Makefile.config, and set COQBIN to the desired value.\n"; print "# \n\n" let include_dirs l = @@ -253,16 +257,8 @@ let include_dirs l = let str_i' = parse_includes inc_i' in let str_r = parse_includes inc_r in section "Libraries definitions."; - printf "CAMLP4:=%s\n" Coq_config.camlp4; - print "ifdef CAMLP4BIN\n"; - print " CAMLP4LIB:=$(shell $(CAMLP4BIN)/$(CAMLP4) -where 2> /dev/null)\n"; - print "else\n"; - print " CAMLP4LIB:=$(shell $(CAMLP4) -where 2> /dev/null)\n"; - print "endif\n"; print "OCAMLLIBS:=-I $(CAMLP4LIB) "; print_list "\\\n " str_i; print "\n"; - print "COQLIB:=$(shell $(COQBIN)coqtop -where 2> /dev/null)\n"; - print "ifdef COQTOP # set COQTOP for compiling from Coq sources\n"; - print " COQBIN:=$(COQTOP)/bin/\n"; + print "ifneq ($(LOCAL),0) # set COQTOP for compiling from Coq sources\n"; print " COQSRCLIBS:=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\ -I $(COQTOP)/library -I $(COQTOP)/parsing \\ -I $(COQTOP)/pretyping -I $(COQTOP)/interp \\ @@ -275,17 +271,9 @@ let include_dirs l = -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/romega \\ -I $(COQTOP)/contrib/rtauto -I $(COQTOP)/contrib/setoid_ring \\ -I $(COQTOP)/contrib/subtac -I $(COQTOP)/contrib/xml\n"; - print "else ifneq ($(strip $(COQLIB)),)\n"; - print " COQSRCLIBS:=-I $(COQLIB)\n"; print "else\n"; - print " $(error Cannot find coqtop in path; set variable COQBIN to the directory where coqtop is located)\n"; + print " COQSRCLIBS:=-I $(COQLIB)\n"; print "endif\n"; - if List.exists (function ML _ -> true | _ -> false) l then - begin - print "ifeq ($(strip $(CAMLP4LIB)),)\n"; - print " $(error Cannot find $(CAMLP4) in path; set variable CAMLP4BIN to the directory where $(CAMLP4) is located)\n"; - print "endif\n"; - end; print "COQLIBS:="; print_list "\\\n " str_i'; print " "; print_list "\\\n " str_r; print "\n"; print "COQDOCLIBS:="; print_list "\\\n " str_r; print "\n\n" @@ -504,6 +492,7 @@ let directories_deps l = let do_makefile args = let l = process_cmd_line args in banner (); + header_includes (); warning (); command_line args; parameters (); @@ -516,7 +505,7 @@ let do_makefile args = implicit (); standard sds sps; (* TEST directories_deps l; *) - includes (); + footer_includes (); warning (); if not (!output_channel == stdout) then close_out !output_channel; exit 0 diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 277bc8d09..2ad5117b9 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -276,6 +276,8 @@ let parse_args is_ide = | "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0 + | ("-config"|"--config") :: _ -> Usage.print_config (); exit 0 + | ("-quiet"|"-silent") :: rem -> Flags.make_silent true; parse rem | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 417a496f8..02fa69142 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -49,6 +49,7 @@ let print_usage_channel co command = -byte run the bytecode version of Coq -where print Coq's standard library location and exit + -config print Coq's configuration information and exit -v print Coq version and exit -q skip loading of rcfile @@ -84,3 +85,17 @@ options are: -bindir override the default directory where coqc looks for coqtop -image f specify an alternative executable for Coq -t keep temporary files\n\n" + +(* Print the configuration information *) + +let print_config () = + if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n"; + Printf.printf "COQBIN=%s/\n" Coq_config.bindir; + Printf.printf "COQLIB=%s/\n" Coq_config.coqlib; + Printf.printf "COQTOP=%s/\n" Coq_config.coqtop; + Printf.printf "CAMLBIN=%s/\n" Coq_config.camldir; + Printf.printf "CAMLP4=%s\n" Coq_config.camlp4; + Printf.printf "CAMLP4LIB=%s\n" Coq_config.camlp4lib + + + diff --git a/toplevel/usage.mli b/toplevel/usage.mli index 6c9ed474c..fb973e3ba 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -18,3 +18,6 @@ val print_usage : string -> unit (*s Prints the usage on the error output. *) val print_usage_coqtop : unit -> unit val print_usage_coqc : unit -> unit + +(*s Prints the configuration information *) +val print_config : unit -> unit -- cgit v1.2.3