~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to configure

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
 
1
#!/bin/bash
 
2
 
 
3
##################################
 
4
#
 
5
#  Configuration script for Coq
 
6
 
7
##################################
 
8
 
 
9
VERSION=8.2pl1
 
10
VOMAGIC=08200
 
11
STATEMAGIC=58200
 
12
DATE=`LANG=C date +"%B %Y"`
 
13
 
 
14
# Create the bin/ directory if non-existent
 
15
test -d bin || mkdir bin
 
16
 
 
17
# a local which command for sh
 
18
which () {
 
19
IFS=":" # set words separator in PATH to be ':' (it allows spaces in dirnames)
 
20
for i in $PATH; do
 
21
  if test -z "$i"; then i=.; fi 
 
22
  if [ -f "$i/$1" ] ; then
 
23
        IFS=" "
 
24
        echo "$i/$1"
 
25
        break
 
26
  fi
 
27
done
 
28
}
 
29
 
 
30
usage () {
 
31
    printf "Available options for configure are:\n"
 
32
    echo "-help"
 
33
    printf "\tDisplays this help page\n"
 
34
    echo "-prefix <dir>"
 
35
    printf "\tSet installation directory to <dir>\n"
 
36
    echo "-local"
 
37
    printf "\tSet installation directory to the current source tree\n"
 
38
    echo "-coqrunbyteflags"
 
39
    printf "\tSet link flags for VM-dependent bytecode (coqtop)\n"
 
40
    echo "-coqtoolsbyteflags"
 
41
    printf "\tSet link flags for VM-independant bytecode (coqdep, coqdoc, ...)\n"
 
42
    echo "-custom"
 
43
    printf "\tGenerate all bytecode executables with -custom (not recommended)\n"
 
44
    echo "-src"
 
45
    printf "\tSpecifies the source directory\n"
 
46
    echo "-bindir"
 
47
    echo "-libdir"
 
48
    echo "-mandir"
 
49
    echo "-docdir"
 
50
    printf "\tSpecifies where to install bin/lib/man/doc files resp.\n"
 
51
    echo "-emacslib"
 
52
    echo "-emacs"
 
53
    printf "\tSpecifies where emacs files are to be installed\n"
 
54
    echo "-coqdocdir"
 
55
    printf "\tSpecifies where Coqdoc style files are to be installed\n"
 
56
    echo "-camldir"
 
57
    printf "\tSpecifies the path to the OCaml library\n"
 
58
    echo "-lablgtkdir"
 
59
    printf "\tSpecifies the path to the Lablgtk library\n"
 
60
    echo "-camlp5dir"
 
61
    printf "\tSpecifies where to look for the Camlp5 library and tells to use it\n"
 
62
    echo "-arch"
 
63
    printf "\tSpecifies the architecture\n"
 
64
    echo "-opt"
 
65
    printf "\tSpecifies whether or not to use OCaml *.opt optimized compilers\n"
 
66
    echo "-fsets (all|basic)"
 
67
    echo "-reals (all|basic)"
 
68
    printf "\tSpecifies whether or not to compile full FSets/Reals library\n"
 
69
    echo "-coqide (opt|byte|no)"
 
70
    printf "\tSpecifies whether or not to compile Coqide\n"
 
71
    echo "-browser <command>"
 
72
    printf "\tUse <command> to open URL %%s\n"
 
73
    echo "-with-doc (yes|no)"
 
74
    printf "\tSpecifies whether or not to compile the documentation\n"
 
75
    echo "-with-geoproof (yes|no)"
 
76
    printf "\tSpecifies whether or not to use Geoproof binding\n"
 
77
    echo "-with-cc <file>"
 
78
    echo "-with-ar <file>"
 
79
    echo "-with-ranlib <file>"
 
80
    printf "\tTells configure where to find gcc/ar/ranlib executables\n"
 
81
    echo "-byte-only"
 
82
    printf "\tCompiles only bytecode version of Coq\n"
 
83
    echo "-debug"
 
84
    printf "\tAdd debugging information in the Coq executables\n"
 
85
    echo "-profile"
 
86
    printf "\tAdd profiling information in the Coq executables\n"
 
87
    echo "-annotate"
 
88
    printf "\tCompiles Coq with -dtypes option\n"
 
89
}
 
90
 
 
91
 
 
92
# Default OCaml binaries
 
93
bytecamlc=ocamlc
 
94
nativecamlc=ocamlopt
 
95
ocamlmklibexec=ocamlmklib
 
96
ocamlexec=ocaml
 
97
ocamldepexec=ocamldep
 
98
ocamldocexec=ocamldoc
 
99
ocamllexexec=ocamllex
 
100
ocamlyaccexec=ocamlyacc
 
101
ocamlmktopexec=ocamlmktop
 
102
camlp4oexec=camlp4o
 
103
 
 
104
 
 
105
coq_debug_flag=
 
106
coq_debug_flag_opt=
 
107
coq_profile_flag=
 
108
coq_annotate_flag=
 
109
best_compiler=opt
 
110
cflags="-fno-defer-pop -Wall -Wno-unused"
 
111
 
 
112
gcc_exec=gcc
 
113
ar_exec=ar
 
114
ranlib_exec=ranlib
 
115
 
 
116
local=false
 
117
coqrunbyteflags_spec=no
 
118
coqtoolsbyteflags_spec=no
 
119
custom_spec=no
 
120
src_spec=no
 
121
prefix_spec=no
 
122
bindir_spec=no
 
123
libdir_spec=no
 
124
mandir_spec=no
 
125
docdir_spec=no
 
126
emacslib_spec=no
 
127
emacs_spec=no
 
128
camldir_spec=no
 
129
lablgtkdir_spec=no
 
130
coqdocdir_spec=no
 
131
fsets=all
 
132
reals=all
 
133
arch_spec=no
 
134
coqide_spec=no
 
135
browser_spec=no
 
136
wwwcoq_spec=no
 
137
with_geoproof=false
 
138
with_doc=all
 
139
with_doc_spec=no
 
140
 
 
141
COQSRC=`pwd`
 
142
 
 
143
# Parse command-line arguments
 
144
 
 
145
while : ; do
 
146
  case "$1" in
 
147
    "") break;;
 
148
    -help|--help) usage
 
149
                  exit;;
 
150
    -prefix|--prefix) prefix_spec=yes
 
151
                      prefix="$2"
 
152
                      shift;;
 
153
    -local|--local) local=true;;
 
154
    -coqrunbyteflags|--coqrunbyteflags) coqrunbyteflags_spec=yes
 
155
                                        coqrunbyteflags="$2"
 
156
                                        shift;;
 
157
    -coqtoolsbyteflags|--coqtoolsbyteflags) coqtoolsbyteflags_spec=yes
 
158
                                            coqtoolsbyteflags="$2"
 
159
                                            shift;;
 
160
    -custom|--custom) custom_spec=yes
 
161
                      shift;;
 
162
    -src|--src) src_spec=yes
 
163
                COQSRC="$2"
 
164
                shift;;
 
165
    -bindir|--bindir) bindir_spec=yes
 
166
                      bindir="$2"
 
167
                      shift;;
 
168
    -libdir|--libdir) libdir_spec=yes
 
169
                      libdir="$2"
 
170
                      shift;;
 
171
    -mandir|--mandir) mandir_spec=yes
 
172
                      mandir="$2"
 
173
                      shift;;
 
174
    -docdir|--docdir) docdir_spec=yes
 
175
                      docdir="$2"
 
176
                      shift;;
 
177
    -emacslib|--emacslib) emacslib_spec=yes
 
178
                          emacslib="$2"
 
179
                          shift;;
 
180
    -emacs |--emacs) emacs_spec=yes
 
181
                     emacs="$2"
 
182
                     shift;;
 
183
    -coqdocdir|--coqdocdir) coqdocdir_spec=yes
 
184
                      coqdocdir="$2"
 
185
                      shift;;
 
186
    -camldir|--camldir) camldir_spec=yes
 
187
                        camldir="$2"
 
188
                        shift;;
 
189
    -lablgtkdir|--lablgtkdir) lablgtkdir_spec=yes
 
190
                        lablgtkdir="$2"
 
191
                        shift;;
 
192
    -camlp5dir|--camlp5dir)
 
193
                        camlp5dir="$2"
 
194
                        shift;;
 
195
    -arch|--arch) arch_spec=yes
 
196
                  arch=$2
 
197
                  shift;;
 
198
    -opt|--opt) bytecamlc=ocamlc.opt
 
199
                camlp4oexec=camlp4o  # can't add .opt since dyn load'll be required
 
200
                nativecamlc=ocamlopt.opt;;
 
201
    -fsets|--fsets) case "$2" in
 
202
                        yes|all) fsets=all;;
 
203
                        *) fsets=basic
 
204
                    esac
 
205
                    shift;;
 
206
    -reals|--reals) case "$2" in
 
207
                        yes|all) reals=all;;
 
208
                        *) reals=basic
 
209
                    esac
 
210
                    shift;;
 
211
    -coqide|--coqide) coqide_spec=yes
 
212
                      case "$2" in
 
213
                          byte|opt) COQIDE=$2;;
 
214
                          *) COQIDE=no
 
215
                      esac
 
216
                      shift;;
 
217
    -browser|--browser) browser_spec=yes
 
218
                      BROWSER=$2
 
219
                      shift;;
 
220
    -coqwebsite|--coqwebsite) wwwcoq_spec=yes
 
221
                      WWWCOQ=$2
 
222
                      shift;;
 
223
    -with-doc|--with-doc) with_doc_spec=yes
 
224
                      case "$2" in
 
225
                          yes|all) with_doc=all;;
 
226
                          *) with_doc=no
 
227
                      esac
 
228
                      shift;;
 
229
    -with-geoproof|--with-geoproof) 
 
230
          case $2 in
 
231
              yes) with_geoproof=true;;
 
232
              no) with_geoproof=false;;
 
233
          esac
 
234
          shift;;
 
235
    -with-cc|-with-gcc|--with-cc|--with-gcc) 
 
236
          gcc_spec=yes
 
237
          gcc_exec=$2
 
238
          shift;;
 
239
    -with-ar|--with-ar) 
 
240
          ar_spec=yes
 
241
          ar_exec=$2
 
242
          shift;;
 
243
    -with-ranlib|--with-ranlib) 
 
244
          ranlib_spec=yes
 
245
          ranlib_exec=$2
 
246
          shift;;
 
247
    -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;;
 
248
    -debug|--debug) coq_debug_flag=-g;;
 
249
    -profile|--profile) coq_profile_flag=-p;;
 
250
    -annotate|--annotate) coq_annotate_flag=-dtypes;;
 
251
    *) echo "Unknown option \"$1\"." 1>&2; usage; exit 2;;
 
252
  esac
 
253
  shift
 
254
done
 
255
 
 
256
if [ $prefix_spec = yes -a $local = true ] ; then
 
257
  echo "Options -prefix and -local are incompatible"
 
258
  echo "Configure script failed!"
 
259
  exit 1
 
260
fi
 
261
 
 
262
# compile date
 
263
DATEPGM=`which date`
 
264
case $DATEPGM in
 
265
    "") echo "I can't find the program \"date\" in your path."
 
266
        echo "Please give me the current date"
 
267
        read COMPILEDATE;;
 
268
    *)  COMPILEDATE=`date +"%h %d %Y %H:%M:%S"`;;
 
269
esac
 
270
 
 
271
# Architecture
 
272
 
 
273
case $arch_spec in
 
274
    no) 
 
275
    # First we test if we are running a Cygwin system
 
276
    if [ `uname -s | cut -c -6` = "CYGWIN" ] ; then
 
277
        ARCH="win32"
 
278
    else
 
279
        # If not, we determine the architecture
 
280
        if test -x /bin/arch ; then
 
281
            ARCH=`/bin/arch`
 
282
        elif test -x /usr/bin/arch ; then
 
283
            ARCH=`/usr/bin/arch`
 
284
        elif test -x /usr/ucb/arch ; then
 
285
            ARCH=`/usr/ucb/arch`
 
286
        elif test -x /bin/uname ; then
 
287
            ARCH=`/bin/uname -s`
 
288
        elif test -x /usr/bin/uname ; then
 
289
            ARCH=`/usr/bin/uname -s`
 
290
        else
 
291
            echo "I can not automatically find the name of your architecture"
 
292
            printf "%s"\
 
293
                "Give me a name, please [win32 for Win95, Win98 or WinNT]: "
 
294
            read ARCH
 
295
        fi
 
296
    fi;;
 
297
    yes) ARCH=$arch
 
298
esac
 
299
 
 
300
# executable extension
 
301
 
 
302
case $ARCH in
 
303
    win32) 
 
304
      EXE=".exe"
 
305
      DLLEXT=".dll";;
 
306
    *) EXE=""
 
307
       DLLEXT=".so"
 
308
esac
 
309
 
 
310
# Is the source tree checked out from a recognised
 
311
# version control system ?
 
312
if test -e .svn/entries ; then 
 
313
    checkedout=svn
 
314
elif [ -d '{arch}' ]; then
 
315
    checkedout=gnuarch
 
316
elif [ -z "${GIT_DIR}" ] && [ -d .git ] || [ -d "${GIT_DIR}" ]; then
 
317
    checkedout=git
 
318
else
 
319
    checkedout=0
 
320
fi
 
321
 
 
322
# make command
 
323
 
 
324
MAKE=`which make`
 
325
if [ "$MAKE" != "" ]; then
 
326
  MAKEVERSION=`$MAKE -v | head -1`
 
327
  case $MAKEVERSION in
 
328
    "GNU Make 3.81") 
 
329
      echo "You have GNU Make 3.81. Good!";;
 
330
    *)
 
331
      OK="no"
 
332
      if [ -x ./make ]; then
 
333
          MAKEVERSION=`./make -v | head -1`
 
334
          if [ "$MAKEVERSION" == "GNU Make 3.81" ]; then OK="yes"; fi
 
335
      fi
 
336
      if [ $OK = "no" ]; then
 
337
          echo "GNU Make >= 3.81 is needed"
 
338
          echo "Make 3.81 can be downloaded from ftp://ftp.gnu.org/gnu/make/make-3.81.tar.gz"
 
339
          echo "then locally installed on a Unix-style system by issuing:"
 
340
          echo "  tar xzvf make-3.81.tar.gz"
 
341
          echo "  cd make-3.81"
 
342
          echo "  ./configure"
 
343
          echo "  make"
 
344
          echo "  mv make .."
 
345
          echo "  cd .."
 
346
          echo "Restart then the configure script and later use ./make instead of make"
 
347
          exit 1
 
348
      else
 
349
          echo "You have locally installed GNU Make 3.81. Good!"
 
350
      fi
 
351
  esac
 
352
else
 
353
  echo "Cannot find GNU Make 3.81"
 
354
fi
 
355
 
 
356
# Browser command
 
357
 
 
358
if [ "$browser_spec" = "no" ]; then
 
359
    case $ARCH in
 
360
        win32) BROWSER='C:\PROGRA~1\INTERN~1\IEXPLORE %s' ;;
 
361
        *) BROWSER='firefox -remote "OpenURL(%s,new-tab)" || firefox %s &' ;;
 
362
    esac
 
363
fi
 
364
 
 
365
if [ "$wwwcoq_spec" = "no" ]; then
 
366
    WWWCOQ="http://www.lix.polytechnique.fr/coq/"
 
367
fi
 
368
 
 
369
#########################################
 
370
# Objective Caml programs
 
371
 
 
372
case $camldir_spec in
 
373
    no) CAMLC=`which $bytecamlc`
 
374
        case "$CAMLC" in
 
375
            "") echo "$bytecamlc is not present in your path!"
 
376
                echo "Give me manually the path to the $bytecamlc executable [/usr/local/bin by default]: "
 
377
                read CAMLC
 
378
                
 
379
                case "$CAMLC" in
 
380
                    "") CAMLC=/usr/local/bin/$bytecamlc;;
 
381
                    */ocamlc|*/ocamlc.opt) true;;
 
382
                    */) CAMLC="${CAMLC}"$bytecamlc;;
 
383
                    *) CAMLC="${CAMLC}"/$bytecamlc;;
 
384
                esac
 
385
        esac
 
386
        CAMLBIN=`dirname "$CAMLC"`;;
 
387
    yes) CAMLC=$camldir/$bytecamlc
 
388
        
 
389
         CAMLBIN=`dirname "$CAMLC"`
 
390
         bytecamlc="$CAMLC"
 
391
         nativecamlc=$CAMLBIN/$nativecamlc
 
392
         ocamlexec=$CAMLBIN/ocaml
 
393
         ocamldepexec=$CAMLBIN/ocamldep
 
394
         ocamldocexec=$CAMLBIN/ocamldoc
 
395
         ocamllexexec=$CAMLBIN/ocamllex
 
396
         ocamlyaccexec=$CAMLBIN/ocamlyacc
 
397
         ocamlmktopexec=$CAMLBIN/ocamlmktop
 
398
         ocamlmklibexec=$CAMLBIN/ocamlmklib
 
399
         camlp4oexec=$CAMLBIN/camlp4o
 
400
esac
 
401
 
 
402
if test ! -f "$CAMLC" ; then
 
403
    echo "I can not find the executable '$CAMLC'! (Have you installed it?)"
 
404
    echo "Configuration script failed!"
 
405
    exit 1
 
406
fi
 
407
 
 
408
# Under Windows, OCaml only understands Windows filenames (C:\...)
 
409
case $ARCH in
 
410
    win32) CAMLBIN=`cygpath -m ${CAMLBIN}`;;
 
411
esac
 
412
 
 
413
# this fixes a camlp4 bug under FreeBSD
 
414
# ("native-code program cannot do a dynamic load")
 
415
if [ `uname -s` = "FreeBSD" ]; then camlp4oexec=$camlp4oexec.byte; fi
 
416
 
 
417
CAMLVERSION=`"$bytecamlc" -version`
 
418
 
 
419
case $CAMLVERSION in
 
420
    1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.08.0)
 
421
        echo "Your version of Objective-Caml is $CAMLVERSION."
 
422
        if [ "$CAMLVERSION" = "3.08.0" ] ; then
 
423
            echo "You need Objective-Caml 3.07 or later (to the exception of 3.08.0)!"
 
424
        else
 
425
            echo "You need Objective-Caml 3.07 or later!"
 
426
        fi
 
427
        echo "Configuration script failed!"
 
428
        exit 1;;
 
429
    3.07*|3.08*)
 
430
        echo "You have Objective-Caml $CAMLVERSION. Good!";;
 
431
    ?*)
 
432
        CAMLP4COMPAT="-loc loc" 
 
433
        echo "You have Objective-Caml $CAMLVERSION. Good!";;
 
434
    *)
 
435
        echo "I found the Objective-Caml compiler but cannot find its version number!"
 
436
        echo "Is it installed properly?"
 
437
        echo "Configuration script failed!"
 
438
        exit 1;;
 
439
esac
 
440
 
 
441
CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"`
 
442
 
 
443
# For coqmktop & bytecode compiler
 
444
 
 
445
case $ARCH in
 
446
    win32) # Awfull trick to get around a ^M problem at the end of CAMLLIB
 
447
      CAMLLIB=`"$CAMLC" -where | sed -e 's/^\(.*\)$/\1/'` ;;
 
448
    *)
 
449
      CAMLLIB=`"$CAMLC" -where`
 
450
esac
 
451
 
 
452
# We need to set va special flag for OCaml 3.07
 
453
case  $CAMLVERSION in 
 
454
        3.07*)
 
455
          cflags="$cflags -DOCAML_307";;
 
456
esac
 
457
 
 
458
if [ "$coq_debug_flag" = "-g" ]; then
 
459
    case $CAMLTAG in
 
460
        OCAML31*)
 
461
            # Compilation debug flag
 
462
            coq_debug_flag_opt="-g"
 
463
            ;;
 
464
    esac
 
465
fi
 
466
 
 
467
# Native dynlink
 
468
if test -f `"$CAMLC" -where`/dynlink.cmxa; then
 
469
    HASNATDYNLINK=true
 
470
else
 
471
    HASNATDYNLINK=false
 
472
fi
 
473
 
 
474
# Camlp4 / Camlp5 configuration
 
475
 
 
476
if [ "$camlp5dir" != "" ]; then
 
477
    CAMLP4=camlp5
 
478
    CAMLP4LIB=$camlp5dir
 
479
    if [ ! -f $camlp5dir/camlp5.cma ]; then
 
480
        echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)"
 
481
        echo "Configuration script failed!"
 
482
        exit 1
 
483
    fi
 
484
    camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
 
485
    if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then 
 
486
        echo "Error: Camlp5 found, but in strict mode!"
 
487
        echo "Please compile Camlp5 in transitional mode."
 
488
        exit 1
 
489
    fi
 
490
else
 
491
    case $CAMLTAG in
 
492
        OCAML31*)
 
493
            if [ -x "${CAMLLIB}/camlp5" ]; then
 
494
                CAMLP4LIB=+camlp5
 
495
            elif [ -x "${CAMLLIB}/site-lib/camlp5" ]; then
 
496
                CAMLP4LIB=+site-lib/camlp5
 
497
            else
 
498
                echo "Objective Caml $CAMLVERSION found but no Camlp5 installed."
 
499
                echo "Configuration script failed!"
 
500
                exit 1
 
501
            fi
 
502
            CAMLP4=camlp5
 
503
            camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
 
504
            if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then
 
505
                echo "Error: Camlp5 found, but in strict mode!"
 
506
                echo "Please compile Camlp5 in transitional mode."
 
507
                exit 1
 
508
            fi
 
509
            ;;
 
510
        *)
 
511
            CAMLP4=camlp4
 
512
            CAMLP4LIB=+camlp4
 
513
            ;;
 
514
    esac
 
515
fi
 
516
 
 
517
if [ "$CAMLP4" = "camlp5" ] && `$camlp4oexec -v 2>&1 | grep -q 5.00`; then
 
518
    echo "Camlp5 version 5.00 not supported: versions 4.0x or >= 5.01 are OK."
 
519
    echo "Configuration script failed!"
 
520
    exit 1
 
521
fi
 
522
 
 
523
 
 
524
case $CAMLP4LIB in
 
525
    +*) FULLCAMLP4LIB=$CAMLLIB/`echo $CAMLP4LIB | cut -b 2-`;;
 
526
    *)  FULLCAMLP4LIB=$CAMLP4LIB;;
 
527
esac
 
528
 
 
529
# Assume that camlp(4|5) binaries are at the same place as ocaml ones
 
530
# (this should become configurable some day) 
 
531
CAMLP4BIN=${CAMLBIN}
 
532
 
 
533
# do we have a native compiler: test of ocamlopt and its version
 
534
 
 
535
if [ "$best_compiler" = "opt" ] ; then
 
536
  if test -e "$nativecamlc" || test -e "`which $nativecamlc`"; then
 
537
      CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
 
538
      if [ "`uname -s`" = "Darwin" -a "$ARCH" = "i386" ]; then
 
539
          case $CAMLOPTVERSION in
 
540
              3.09.3|3.1?*) ;;
 
541
              *) echo "Native compilation on MacOS X Pentium requires Objective-Caml >= 3.09.3,"
 
542
                 best_compiler=byte
 
543
                 echo "only the bytecode version of Coq will be available."
 
544
          esac
 
545
      elif [ ! -f $FULLCAMLP4LIB/gramlib.cmxa ]; then
 
546
          best_compiler=byte
 
547
          echo "Cannot find native-code $CAMLP4,"
 
548
          echo "only the bytecode version of Coq will be available."
 
549
      else
 
550
        if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then
 
551
          echo "Native and bytecode compilers do not have the same version!"
 
552
        fi
 
553
        echo "You have native-code compilation. Good!"
 
554
      fi
 
555
  else
 
556
      best_compiler=byte
 
557
      echo "You have only bytecode compilation."
 
558
  fi
 
559
fi
 
560
 
 
561
# OS dependent libraries
 
562
 
 
563
case $ARCH in
 
564
  sun4*) OS=`uname -r`
 
565
        case $OS in
 
566
           5*) OS="Sun Solaris $OS"
 
567
               OSDEPLIBS="-cclib -lunix -cclib -lnsl -cclib -lsocket";;
 
568
           *) OS="Sun OS $OS"
 
569
              OSDEPLIBS="-cclib -lunix"
 
570
        esac;;
 
571
  alpha) OSDEPLIBS="-cclib -lunix";;
 
572
  win32) OS="Win32" 
 
573
         OSDEPLIBS="-cclib -lunix"
 
574
         cflags="-mno-cygwin $cflags";;
 
575
  *) OSDEPLIBS="-cclib -lunix"
 
576
esac
 
577
 
 
578
# lablgtk2 and CoqIDE
 
579
 
 
580
# -byte-only should imply -coqide byte, unless the user decides otherwise
 
581
 
 
582
if [ "$best_compiler" = "byte" -a "$coqide_spec" = "no" ]; then 
 
583
    coqide_spec=yes
 
584
    COQIDE=byte
 
585
fi
 
586
 
 
587
# Which coqide is asked ? which one is possible ?
 
588
 
 
589
if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then 
 
590
    echo "CoqIde disabled as requested."
 
591
else
 
592
    case $lablgtkdir_spec in
 
593
        no) 
 
594
            if [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then
 
595
                lablgtkdir=${CAMLLIB}/lablgtk2
 
596
            elif [ -f "${CAMLLIB}/site-lib/lablgtk2/glib.mli" ]; then
 
597
                lablgtkdir=${CAMLLIB}/site-lib/lablgtk2
 
598
            fi;;
 
599
        yes)
 
600
            if [ ! -f "$lablgtkdir/glib.mli" ]; then
 
601
                echo "Incorrect LablGtk2 library (glib.mli not found)."
 
602
                echo "Configuration script failed!"
 
603
                exit 1
 
604
            fi;;
 
605
    esac
 
606
    if [ "$lablgtkdir" = "" ]; then
 
607
        echo "LablGtk2 not found: CoqIde will not be available."
 
608
        COQIDE=no
 
609
    elif [ -z "`grep -w convert_with_fallback "$lablgtkdir/glib.mli"`" ]; then
 
610
        echo "LablGtk2 found but too old: CoqIde will not be available."
 
611
        COQIDE=no;
 
612
    elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then 
 
613
        echo "LablGtk2 found, bytecode CoqIde will be used as requested."
 
614
        COQIDE=byte
 
615
    elif [ ! -f "${CAMLLIB}/threads/threads.cmxa" ]; then 
 
616
        echo "LablGtk2 found, no native threads: bytecode CoqIde will be available."
 
617
        COQIDE=byte
 
618
    else 
 
619
        echo "LablGtk2 found, native threads: native CoqIde will be available."
 
620
        COQIDE=opt
 
621
    fi
 
622
fi
 
623
 
 
624
case $COQIDE in
 
625
    byte|opt)
 
626
        case $lablgtkdir_spec in
 
627
            no)  LABLGTKLIB=+lablgtk2                   # Pour le message
 
628
                 LABLGTKINCLUDES="-I $LABLGTKLIB";;     # Pour le makefile
 
629
            yes) LABLGTKLIB="$lablgtkdir"               # Pour le message
 
630
                 LABLGTKINCLUDES="-I \"$LABLGTKLIB\"";; # Pour le makefile
 
631
        esac;;
 
632
    no) LABLGTKINCLUDES="";;
 
633
esac
 
634
 
 
635
# Tell on windows if ocaml understands cygwin or windows path formats
 
636
 
 
637
#"$CAMLC" -o config/giveostype config/giveostype.ml
 
638
#CAMLOSTYPE=`config/giveostype`
 
639
#rm config/giveostype
 
640
 
 
641
# strip command
 
642
 
 
643
case $ARCH in
 
644
    win32)
 
645
        # true -> strip : it exists under cygwin !
 
646
        STRIPCOMMAND="strip";; 
 
647
    *)
 
648
    if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ] ||
 
649
       [ "`uname -s`" = "Darwin" -a "$HASNATDYNLINK" = "true" ]
 
650
    then
 
651
        STRIPCOMMAND="true"
 
652
    else
 
653
        STRIPCOMMAND="strip"
 
654
    fi
 
655
esac
 
656
 
 
657
# mktexlsr
 
658
#MKTEXLSR=`which mktexlsr`
 
659
#case $MKTEXLSR in
 
660
#    "") MKTEXLSR=true;;
 
661
#esac
 
662
 
 
663
# "
 
664
### Test if documentation can be compiled (latex, hevea)
 
665
 
 
666
if test "$with_doc" = "all" 
 
667
then
 
668
    if test "`which latex`" = ""
 
669
    then 
 
670
        echo "latex was not found; documentation will not be available"
 
671
        with_doc=no
 
672
    else
 
673
        if test "`which hevea`" = ""
 
674
        then
 
675
            with_doc=no
 
676
            echo "hevea was not found: documentation will not be available"
 
677
        fi
 
678
    fi
 
679
fi
 
680
 
 
681
###########################################
 
682
# bindir, libdir, mandir, docdir, etc.
 
683
 
 
684
case $src_spec in
 
685
  no) COQTOP=${COQSRC}
 
686
esac
 
687
 
 
688
# OCaml only understand Windows filenames (C:\...)
 
689
case $ARCH in
 
690
    win32) COQTOP=`cygpath -m ${COQTOP}`
 
691
esac
 
692
 
 
693
case $ARCH in
 
694
  win32)
 
695
         bindir_def='C:\coq\bin'
 
696
         libdir_def='C:\coq\lib'
 
697
         mandir_def='C:\coq\man'
 
698
         docdir_def='C:\coq\doc'
 
699
         emacslib_def='C:\coq\emacs'
 
700
         coqdocdir_def='C:\coq\latex';;
 
701
  *)
 
702
         bindir_def=/usr/local/bin
 
703
         libdir_def=/usr/local/lib/coq
 
704
         mandir_def=/usr/local/man
 
705
         docdir_def=/usr/local/share/doc/coq
 
706
         emacslib_def=/usr/local/share/emacs/site-lisp
 
707
         coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;;
 
708
esac
 
709
 
 
710
emacs_def=emacs
 
711
 
 
712
case $bindir_spec/$prefix_spec/$local in
 
713
    yes/*/*) BINDIR=$bindir ;;
 
714
    */yes/*) BINDIR=$prefix/bin ;;
 
715
    */*/true) BINDIR=$COQTOP/bin ;;
 
716
    *) printf "Where should I install the Coq binaries [$bindir_def]? "
 
717
        read BINDIR
 
718
        case $BINDIR in
 
719
            "") BINDIR=$bindir_def;;
 
720
            *) true;;
 
721
        esac;;
 
722
esac
 
723
 
 
724
case $libdir_spec/$prefix_spec/$local in
 
725
    yes/*/*) LIBDIR=$libdir;;
 
726
    */yes/*)
 
727
        case $ARCH in
 
728
          win32) LIBDIR=$prefix ;;
 
729
          *)  LIBDIR=$prefix/lib/coq ;;
 
730
        esac ;;
 
731
    */*/true) LIBDIR=$COQTOP ;;
 
732
    *)  printf "Where should I install the Coq library [$libdir_def]? "
 
733
        read LIBDIR
 
734
        case $LIBDIR in
 
735
            "") LIBDIR=$libdir_def;;
 
736
            *) true;;
 
737
        esac;;
 
738
esac
 
739
 
 
740
case $mandir_spec/$prefix_spec/$local in
 
741
    yes/*/*) MANDIR=$mandir;;
 
742
    */yes/*) MANDIR=$prefix/man ;;
 
743
    */*/true) MANDIR=$COQTOP/man ;;
 
744
    *)  printf "Where should I install the Coq man pages [$mandir_def]? "
 
745
        read MANDIR
 
746
        case $MANDIR in
 
747
            "") MANDIR=$mandir_def;;
 
748
            *) true;;
 
749
        esac;;
 
750
esac
 
751
 
 
752
case $docdir_spec/$prefix_spec/$local in
 
753
    yes/*/*) DOCDIR=$docdir;;
 
754
    */yes/*) DOCDIR=$prefix/share/doc/coq ;;
 
755
    */*/true) DOCDIR=$COQTOP/man ;;
 
756
    *)  printf "Where should I install the Coq documentation [$docdir_def]? "
 
757
        read DOCDIR
 
758
        case $DOCDIR in
 
759
            "") DOCDIR=$docdir_def;;
 
760
            *) true;;
 
761
        esac;;
 
762
esac
 
763
 
 
764
case $emacslib_spec/$prefix_spec/$local in
 
765
    yes/*/*) EMACSLIB=$emacslib;;
 
766
    */yes/*)
 
767
        case $ARCH in
 
768
          win32) EMACSLIB=$prefix/emacs ;;
 
769
          *)  EMACSLIB=$prefix/share/emacs/site-lisp ;;
 
770
        esac ;;
 
771
    */*/true) EMACSLIB=$COQTOP/tools/emacs ;;
 
772
    *) printf "Where should I install the Coq Emacs mode [$emacslib_def]? "
 
773
        read EMACSLIB
 
774
        case $EMACSLIB in
 
775
            "") EMACSLIB=$emacslib_def;;
 
776
            *) true;;
 
777
        esac;;
 
778
esac
 
779
 
 
780
case $coqdocdir_spec/$prefix_spec/$local in
 
781
    yes/*/*) COQDOCDIR=$coqdocdir;;
 
782
    */yes/*)
 
783
        case $ARCH in
 
784
          win32) COQDOCDIR=$prefix/latex ;;
 
785
          *)  COQDOCDIR=$prefix/share/emacs/site-lisp ;;
 
786
        esac ;;
 
787
    */*/true) COQDOCDIR=$COQTOP/tools/coqdoc ;;
 
788
    *) printf "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def]? "
 
789
        read COQDOCDIR
 
790
        case $COQDOCDIR in
 
791
            "") COQDOCDIR=$coqdocdir_def;;
 
792
            *) true;;
 
793
        esac;;
 
794
esac
 
795
 
 
796
# Determine if we enable -custom by default (Windows and MacOS)
 
797
CUSTOM_OS=no
 
798
if [ "$ARCH" = "win32" ] || [ "`uname -s`" = "Darwin" ]; then
 
799
    CUSTOM_OS=yes
 
800
fi
 
801
 
 
802
BUILDLDPATH="# you might want to set CAML_LD_LIBRARY_PATH by hand!"
 
803
case $coqrunbyteflags_spec/$local/$custom_spec/$CUSTOM_OS in
 
804
    yes/*/*/*) COQRUNBYTEFLAGS="$coqrunbyteflags";;
 
805
    */*/yes/*|*/*/*/yes) COQRUNBYTEFLAGS="-custom";;
 
806
    */true/*/*) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$COQTOP'/kernel/byterun";;
 
807
    *)
 
808
        COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$LIBDIR'"
 
809
        BUILDLDPATH="export CAML_LD_LIBRARY_PATH='$COQTOP'/kernel/byterun";;
 
810
esac
 
811
case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in
 
812
    yes/*/*) COQTOOLSBYTEFLAGS="$coqtoolsbyteflags";;
 
813
    */yes/*|*/*/yes) COQTOOLSBYTEFLAGS="-custom";;
 
814
    *) COQTOOLSBYTEFLAGS="";;
 
815
esac
 
816
 
 
817
# case $emacs_spec in
 
818
#     no) printf "Which Emacs command should I use to compile coq.el [$emacs_def]? "
 
819
#         read EMACS
 
820
        
 
821
#       case $EMACS in
 
822
#           "") EMACS=$emacs_def;;
 
823
#           *) true;;
 
824
#       esac;;
 
825
#     yes) EMACS=$emacs;;
 
826
# esac
 
827
 
 
828
###########################################
 
829
# Summary of the configuration
 
830
 
 
831
echo ""
 
832
echo "  Coq top directory                 : $COQTOP"
 
833
echo "  Architecture                      : $ARCH"
 
834
if test ! -z "$OS" ; then
 
835
  echo "  Operating system                  : $OS"
 
836
fi
 
837
echo "  Coq VM bytecode link flags        : $COQRUNBYTEFLAGS"
 
838
echo "  Coq tools bytecode link flags     : $COQTOOLSBYTEFLAGS"
 
839
echo "  OS dependent libraries            : $OSDEPLIBS"
 
840
echo "  Objective-Caml/Camlp4 version     : $CAMLVERSION"
 
841
echo "  Objective-Caml/Camlp4 binaries in : $CAMLBIN"
 
842
echo "  Objective-Caml library in         : $CAMLLIB"
 
843
echo "  Camlp4 library in                 : $CAMLP4LIB"
 
844
if test "$COQIDE" != "no"; then
 
845
echo "  Lablgtk2 library in               : $LABLGTKLIB"
 
846
fi
 
847
if test "$fsets" = "all"; then
 
848
echo "  FSets theory                      : All"
 
849
else
 
850
echo "  FSets theory                      : Basic"
 
851
fi
 
852
if test "$reals" = "all"; then
 
853
echo "  Reals theory                      : All"
 
854
else
 
855
echo "  Reals theory                      : Basic"
 
856
fi
 
857
if test "$with_doc" = "all"; then
 
858
echo "  Documentation                     : All"
 
859
else
 
860
echo "  Documentation                     : None"
 
861
fi
 
862
echo "  CoqIde                            : $COQIDE"
 
863
echo "  Web browser                       : $BROWSER"
 
864
echo "  Coq web site                      : $WWWCOQ"
 
865
echo ""
 
866
 
 
867
echo "  Paths for true installation:"
 
868
echo "    binaries      will be copied in $BINDIR"
 
869
echo "    library       will be copied in $LIBDIR"
 
870
echo "    man pages     will be copied in $MANDIR"
 
871
echo "    documentation will be copied in $DOCDIR"
 
872
echo "    emacs mode    will be copied in $EMACSLIB"
 
873
echo ""
 
874
 
 
875
#####################################################
 
876
# Building the $COQTOP/config/coq_config.ml file
 
877
#####################################################
 
878
 
 
879
# An escaped version of a variable
 
880
escape_var () {
 
881
"$ocamlexec" 2>&1 1>/dev/null <<EOF
 
882
  prerr_endline(String.escaped(Sys.getenv"$VAR"));;
 
883
EOF
 
884
}
 
885
 
 
886
# Escaped version of browser command
 
887
export BROWSER
 
888
ESCBROWSER=`VAR=BROWSER escape_var`
 
889
 
 
890
# damned backslashes under M$Windows
 
891
case $ARCH in
 
892
    win32)
 
893
        ESCCOQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'`
 
894
        ESCBINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
 
895
        ESCSRCDIR=`cygpath -m $COQSRC |sed -e 's|\\\|\\\\\\\|g'`
 
896
        ESCLIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
 
897
        ESCCAMLDIR=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'`
 
898
        ESCCAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'`
 
899
        ESCMANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
 
900
        ESCDOCDIR=`echo $DOCDIR |sed -e 's|\\\|\\\\\\\|g'`
 
901
        ESCEMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
 
902
        ESCCOQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'`
 
903
        ESCCAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'`
 
904
        ESCCAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'`
 
905
        ESCLABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'`
 
906
        ESCCOQRUNBYTEFLAGS=`echo $COQRUNBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
 
907
        ESCCOQTOOLSBYTEFLAGS=`echo $COQTOOLSBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
 
908
        ESCBUILDLDPATH=`echo $BUILDLDPATH |sed -e 's|\\\|\\\\\\\|g'`
 
909
;;
 
910
    *)
 
911
        ESCCOQTOP="$COQTOP"
 
912
        ESCBINDIR="$BINDIR"
 
913
        ESCSRCDIR="$COQSRC"
 
914
        ESCLIBDIR="$LIBDIR"
 
915
        ESCCAMLDIR="$CAMLBIN"
 
916
        ESCCAMLLIB="$CAMLLIB"
 
917
        ESCMANDIR="$MANDIR"
 
918
        ESCDOCDIR="$DOCDIR"
 
919
        ESCEMACSLIB="$EMACSLIB"
 
920
        ESCCOQDOCDIR="$COQDOCDIR"
 
921
        ESCCAMLP4BIN="$CAMLP4BIN"
 
922
        ESCCAMLP4LIB="$CAMLP4LIB"
 
923
        ESCLABLGTKINCLUDES="$LABLGTKINCLUDES"
 
924
        ESCCOQRUNBYTEFLAGS="$COQRUNBYTEFLAGS"
 
925
        ESCCOQTOOLSBYTEFLAGS="$COQTOOLSBYTEFLAGS"
 
926
        ;;
 
927
esac
 
928
 
 
929
mlconfig_file="$COQSRC/config/coq_config.ml"
 
930
rm -f "$mlconfig_file"
 
931
cat << END_OF_COQ_CONFIG > $mlconfig_file
 
932
(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
 
933
 
 
934
let local = $local
 
935
let coqrunbyteflags = "$ESCCOQRUNBYTEFLAGS"
 
936
let coqlib = "$ESCLIBDIR"
 
937
let coqsrc = "$ESCSRCDIR"
 
938
let camlbin = "$ESCCAMLDIR"
 
939
let camllib = "$ESCCAMLLIB"
 
940
let camlp4 = "$CAMLP4"
 
941
let camlp4bin = "$ESCCAMLP4BIN"
 
942
let camlp4lib = "$ESCCAMLP4LIB"
 
943
let best = "$best_compiler"
 
944
let arch = "$ARCH"
 
945
let has_natdynlink = $HASNATDYNLINK
 
946
let osdeplibs = "$OSDEPLIBS"
 
947
let version = "$VERSION"
 
948
let caml_version = "$CAMLVERSION"
 
949
let date = "$DATE"
 
950
let compile_date = "$COMPILEDATE"
 
951
let vo_magic_number = $VOMAGIC
 
952
let state_magic_number = $STATEMAGIC
 
953
let exec_extension = "$EXE"
 
954
let with_geoproof = ref $with_geoproof
 
955
let browser = "$ESCBROWSER"
 
956
let wwwcoq = "$WWWCOQ"
 
957
let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/"
 
958
let wwwstdlib = wwwcoq ^ "distrib/" ^ version ^ "/stdlib/"
 
959
 
 
960
END_OF_COQ_CONFIG
 
961
 
 
962
# to be sure printf is found on windows when spaces occur in PATH variable
 
963
PRINTF=`which printf`
 
964
 
 
965
# Subdirectories of theories/ added in coq_config.ml
 
966
subdirs () {
 
967
    (cd $1; find * \( -name .svn -prune \) -o \( -type d -exec $PRINTF "\"%s\";\n" {} \; \) | grep -v correctness >> "$mlconfig_file")
 
968
}
 
969
 
 
970
echo "let theories_dirs = [" >> "$mlconfig_file"
 
971
subdirs theories
 
972
echo "]" >> "$mlconfig_file"
 
973
 
 
974
echo "let contrib_dirs = [" >> "$mlconfig_file"
 
975
subdirs contrib
 
976
echo "]" >> "$mlconfig_file"
 
977
 
 
978
chmod a-w "$mlconfig_file"
 
979
 
 
980
 
 
981
###############################################
 
982
# Building the $COQTOP/config/Makefile file
 
983
###############################################
 
984
 
 
985
rm -f "$COQSRC/config/Makefile"
 
986
 
 
987
sed -e "s|LOCALINSTALLATION|$local|" \
 
988
    -e "s|XCOQRUNBYTEFLAGS|$ESCCOQRUNBYTEFLAGS|" \
 
989
    -e "s|XCOQTOOLSBYTEFLAGS|$ESCCOQTOOLSBYTEFLAGS|" \
 
990
    -e "s|COQSRCDIRECTORY|$COQSRC|" \
 
991
    -e "s|COQVERSION|$VERSION|" \
 
992
    -e "s|BINDIRDIRECTORY|$ESCBINDIR|" \
 
993
    -e "s|COQLIBDIRECTORY|$ESCLIBDIR|" \
 
994
    -e "s|BUILDLDPATH=|$ESCBUILDLDPATH|" \
 
995
    -e "s|MANDIRDIRECTORY|$ESCMANDIR|" \
 
996
    -e "s|DOCDIRDIRECTORY|$ESCDOCDIR|" \
 
997
    -e "s|EMACSLIBDIRECTORY|$ESCEMACSLIB|" \
 
998
    -e "s|EMACSCOMMAND|$EMACS|" \
 
999
    -e "s|COQDOCDIRECTORY|$ESCCOQDOCDIR|" \
 
1000
    -e "s|MKTEXLSRCOMMAND|$MKTEXLSR|" \
 
1001
    -e "s|ARCHITECTURE|$ARCH|" \
 
1002
    -e "s|OSDEPENDENTLIBS|$OSDEPLIBS|" \
 
1003
    -e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
 
1004
    -e "s|CAMLLIBDIRECTORY|$ESCCAMLLIB|" \
 
1005
    -e "s|CAMLTAG|$CAMLTAG|" \
 
1006
    -e "s|CAMLP4BINDIRECTORY|$ESCCAMLP4BIN|" \
 
1007
    -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
 
1008
    -e "s|CAMLP4TOOL|$camlp4oexec|" \
 
1009
    -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \
 
1010
    -e "s|LABLGTKINCLUDES|$ESCLABLGTKINCLUDES|" \
 
1011
    -e "s|COQDEBUGFLAGOPT|$coq_debug_flag_opt|" \
 
1012
    -e "s|COQDEBUGFLAG|$coq_debug_flag|" \
 
1013
    -e "s|COQPROFILEFLAG|$coq_profile_flag|" \
 
1014
    -e "s|CAMLANNOTATEFLAG|$coq_annotate_flag|" \
 
1015
    -e "s|CCOMPILEFLAGS|$cflags|" \
 
1016
    -e "s|BESTCOMPILER|$best_compiler|" \
 
1017
    -e "s|DLLEXTENSION|$DLLEXT|" \
 
1018
    -e "s|EXECUTEEXTENSION|$EXE|" \
 
1019
    -e "s|BYTECAMLC|$bytecamlc|" \
 
1020
    -e "s|OCAMLMKLIBEXEC|$ocamlmklibexec|" \
 
1021
    -e "s|NATIVECAMLC|$nativecamlc|" \
 
1022
    -e "s|OCAMLEXEC|$ocamlexec|" \
 
1023
    -e "s|OCAMLDEPEXEC|$ocamldepexec|" \
 
1024
    -e "s|OCAMLDOCEXEC|$ocamldocexec|" \
 
1025
    -e "s|OCAMLLEXEXEC|$ocamllexexec|" \
 
1026
    -e "s|OCAMLYACCEXEC|$ocamlyaccexec|" \
 
1027
    -e "s|CAMLMKTOPEXEC|$ocamlmktopexec|" \
 
1028
    -e "s|CCEXEC|$gcc_exec|" \
 
1029
    -e "s|AREXEC|$ar_exec|" \
 
1030
    -e "s|RANLIBEXEC|$ranlib_exec|" \
 
1031
    -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
 
1032
    -e "s|FSETSOPT|$fsets|" \
 
1033
    -e "s|REALSOPT|$reals|" \
 
1034
    -e "s|COQIDEOPT|$COQIDE|" \
 
1035
    -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \
 
1036
    -e "s|WITHDOCOPT|$with_doc|" \
 
1037
    -e "s|HASNATIVEDYNLINK|$HASNATDYNLINK|" \
 
1038
      "$COQSRC/config/Makefile.template" > "$COQSRC/config/Makefile"
 
1039
 
 
1040
chmod a-w "$COQSRC/config/Makefile"
 
1041
 
 
1042
##################################################
 
1043
# Building the $COQTOP/dev/ocamldebug-coq file
 
1044
##################################################
 
1045
 
 
1046
OCAMLDEBUGCOQ=$COQSRC/dev/ocamldebug-coq
 
1047
 
 
1048
if test "$coq_debug_flag" = "-g" ; then
 
1049
  rm -f $OCAMLDEBUGCOQ
 
1050
  sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
 
1051
      -e "s|COQLIBDIRECTORY|$LIBDIR|" \
 
1052
      -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
 
1053
      -e "s|CAMLP4LIBDIRECTORY|$FULLCAMLP4LIB|"\
 
1054
      $OCAMLDEBUGCOQ.template > $OCAMLDEBUGCOQ
 
1055
  chmod a-w,a+x $OCAMLDEBUGCOQ
 
1056
fi
 
1057
 
 
1058
####################################################
 
1059
# Fixing lablgtk types (before/after 2.6.0) 
 
1060
####################################################
 
1061
 
 
1062
if [ ! "$COQIDE" = "no" ]; then 
 
1063
    if grep "class view " "$lablgtkdir/gText.mli" | grep -q "\[>" ; then
 
1064
       if grep -q "?accepts_tab:bool" "$lablgtkdir/gText.mli" ; then
 
1065
        cp -f ide/undo_lablgtk_ge212.mli ide/undo.mli
 
1066
       else
 
1067
        cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli
 
1068
       fi
 
1069
    else
 
1070
        cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli
 
1071
    fi
 
1072
fi  
 
1073
 
 
1074
##################################################
 
1075
# The end
 
1076
####################################################
 
1077
 
 
1078
echo "If anything in the above is wrong, please restart './configure'"
 
1079
echo
 
1080
echo "*Warning* To compile the system for a new architecture"
 
1081
echo "          don't forget to do a 'make archclean' before './configure'."
 
1082
 
 
1083
# $Id: configure 12219 2009-07-01 09:58:00Z notin $