diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-03 14:44:46 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-03 14:44:46 +0000 |
| commit | e19ab99ea5b440dad9f80a57d18637f4d2d49811 (patch) | |
| tree | 3f9edf049dfc78c266a0afd4d68f2f2248c65239 | |
| parent | 95483a55c228a0c3d9628a8b4e6cc45c84b8c894 (diff) | |
Compilation sous windows
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10171 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.build | 10 | ||||
| -rw-r--r-- | config/Makefile.template | 3 | ||||
| -rwxr-xr-x | configure | 19 |
3 files changed, 19 insertions, 13 deletions
diff --git a/Makefile.build b/Makefile.build index d8a834e27..fb36ff9b3 100644 --- a/Makefile.build +++ b/Makefile.build @@ -75,7 +75,7 @@ OCAMLOPT += $(CAMLFLAGS) BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) $(USERFLAGS) -DEPFLAGS=$(LOCALINCLUDES) +DEPFLAGS= -slash $(LOCALINCLUDES) CAMLP4EXTENDFLAGS=-I . #grammar dependencies are now in camlp4use statements CAMLP4DEPS=sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*\*)@\1@p' @@ -122,12 +122,6 @@ endif CINCLUDES= -I $(CAMLHLIB) -ifeq ($(CAMLVERSION),OCAML307) - CFLAGS=-fno-defer-pop -Wall -Wno-unused -DOCAML_307 -else - CFLAGS=-fno-defer-pop -Wall -Wno-unused -endif - # libcoqrun.a $(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) @@ -867,7 +861,7 @@ endif %.c.d: %.c | $(GENHFILES) $(SHOW)'CCDEP $<' - $(HIDE)$(CC) -MM -MQ "$@" -MQ "$(<:.c=.o)" $(CFLAGS) $< > $@ \ + $(HIDE)$(CC) -MM -MQ "$@" -MQ "$(<:.c=.o)" $(CFLAGS) -isystem $(CAMLHLIB) $< > $@ \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) .SECONDARY: $(GENFILES) diff --git a/config/Makefile.template b/config/Makefile.template index 4e2cc42b0..f99c7cfbc 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -73,6 +73,9 @@ CAMLDEBUG=COQDEBUGFLAG # User compilation flag USERFLAGS= +# Flags for GCC +CFLAGS=CCOMPILEFLAGS + # Compilation profile flag CAMLTIMEPROF=COQPROFILEFLAG @@ -85,6 +85,7 @@ coq_debug_flag= coq_profile_flag= coq_annotate_flag= best_compiler=opt +cflags="-fno-defer-pop -Wall -Wno-unused" gcc_exec=gcc ar_exec=ar @@ -360,13 +361,19 @@ if [ "$best_compiler" = "opt" ] ; then fi fi - # For coqmktop & bytecode compiler case $ARCH in - win32) # Awful trick to get around ^M character at the end of CAMLLIB - CAMLLIB="C:\OCaml\lib";; - *) CAMLLIB=`"$CAMLC" -where` + win32) # Awfull trick to get around a ^M problem at the end of CAMLLIB + CAMLLIB=`"$CAMLC" -where | sed -e 's/^\(.*\)$/\1/'` ;; + *) + CAMLLIB=`"$CAMLC" -where` +esac + +# We need to set va special flag for OCaml 3.07 +case $CAMLVERSION in + 3.07*) + cflags="$cflags -DOCAML_307";; esac # Camlp4 / Camlp5 configuration @@ -404,7 +411,8 @@ case $ARCH in esac;; alpha) OSDEPLIBS="-cclib -lunix";; win32) OS="Win32" - OSDEPLIBS="-cclib -lunix";; + OSDEPLIBS="-cclib -lunix" + cflags="-mno-cygwin $cflags";; *) OSDEPLIBS="-cclib -lunix" esac @@ -732,6 +740,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \ -e "s|COQDEBUGFLAG|$coq_debug_flag|" \ -e "s|COQPROFILEFLAG|$coq_profile_flag|" \ -e "s|CAMLANNOTATEFLAG|$coq_annotate_flag|" \ + -e "s|CCOMPILEFLAGS|$cflags|" \ -e "s|BESTCOMPILER|$best_compiler|" \ -e "s|EXECUTEEXTENSION|$EXE|" \ -e "s|BYTECAMLC|$bytecamlc|" \ |