Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

configure 26.3 KB
Newer Older
1
2
#!/bin/sh

3
4
5
6
7
8
9
10
#######################################################################
#                                                                     #
#              The Compcert verified compiler                         #
#                                                                     #
#          Xavier Leroy, INRIA Paris-Rocquencourt                     #
#                                                                     #
#  Copyright Institut National de Recherche en Informatique et en     #
#  Automatique.  All rights reserved.  This file is distributed       #
11
12
13
14
15
#  under the terms of the GNU Lesser General Public License as        #
#  published by the Free Software Foundation, either version 2.1 of   #
#  the License, or (at your option) any later version.                #
#  This file is also distributed under the terms of the               #
#  INRIA Non-Commercial License Agreement.                            #
16
17
18
#                                                                     #
#######################################################################

19
prefix='/usr/local'
20
21
bindir='$(PREFIX)/bin'
libdir='$(PREFIX)/lib/compcert'
22
mandir='$(PREFIX)/share/man'
23
coqdevdir='$(PREFIX)/lib/compcert/coq'
xleroy's avatar
xleroy committed
24
toolprefix=''
25
target=''
xleroy's avatar
xleroy committed
26
has_runtime_lib=true
27
has_standard_headers=true
28
clightgen=false
29
install_coqdev=false
30
ignore_coq_version=false
31
32
library_Flocq=local
library_MenhirLib=local
33

xleroy's avatar
xleroy committed
34
usage='Usage: ./configure [options] target
35
36
37
38
For help on options and targets, do: ./configure -help
'

help='Usage: ./configure [options] target
39
40

Supported targets:
41
42
43
  ppc-eabi             (PowerPC, EABI with GNU/Unix tools)
  ppc-eabi-diab        (PowerPC, EABI with Diab tools)
  ppc-linux            (PowerPC, Linux)
44
45
46
47
48
49
50
51
  arm-eabi             (ARM, EABI, little endian)
  arm-linux            (ARM, EABI, little endian)
  arm-eabihf           (ARM, EABI using hardware FP registers, little endian)
  arm-hardfloat        (ARM, EABI using hardware FP registers, little endian)
  armeb-eabi           (ARM, EABI, big endian)
  armeb-linux          (ARM, EABI, big endian)
  armeb-eabihf         (ARM, EABI using hardware FP registers, big endian)
  armeb-hardfloat      (ARM, EABI using hardware FP registers, big endian)
52
53
54
  x86_32-linux         (x86 32 bits, Linux)
  x86_32-bsd           (x86 32 bits, BSD)
  x86_32-cygwin        (x86 32 bits, Cygwin environment under Windows)
55
  x86_64-linux         (x86 64 bits, Linux)
56
  x86_64-bsd           (x86 64 bits, BSD)
Xavier Leroy's avatar
Xavier Leroy committed
57
  x86_64-macos         (x86 64 bits, MacOS X)
Xavier Leroy's avatar
Xavier Leroy committed
58
  x86_64-cygwin        (x86 64 bits, Cygwin environment under Windows)
59
60
  rv32-linux           (RISC-V 32 bits, Linux)
  rv64-linux           (RISC-V 64 bits, Linux)
Cyril SIX's avatar
Cyril SIX committed
61
62
63
  kvx-mbr              (Kalray KV3, bare runtime)
  kvx-elf              (Kalray KV3, ELF)
  kvx-cos              (Kalray KV3, ClusterOS)
Xavier Leroy's avatar
Xavier Leroy committed
64
  aarch64-linux        (AArch64, i.e. ARMv8 in 64-bit mode, Linux)
Xavier Leroy's avatar
Xavier Leroy committed
65
  aarch64-macos        (AArch64, i.e. Apple silicon, MacOS)
66
  manual               (edit configuration file by hand)
67

68
69
For x86 targets, the "x86_32-" prefix can also be written "ia32-" or "i386-".
For x86 targets, the "x86_64-" prefix can also be written "amd64-".
Xavier Leroy's avatar
Xavier Leroy committed
70
For AArch64 targets, the "aarch64-" prefix can also be written "arm64-".
71

72
For PowerPC targets, the "ppc-" prefix can be refined into:
73
74
  ppc64-               PowerPC 64 bits
  e5500-               Freescale e5500 core (PowerPC 64 bit, EREF extensions)
75

76
For ARM targets, the "arm-" or "armeb-" prefix can be refined into:
77
78
  armv6-               ARMv6   + VFPv2       (Thumb mode not supported)
  armv6t2-             ARMv6T2 + VFPv2
79
  armv7a-              ARMv7-A + VFPv3-d16   (default for arm-)
80
81
82
  armv7r-              ARMv7-R + VFPv3-d16
  armv7m-              ARMv7-M + VFPv3-d16

83
84
  armebv6-             ARMv6   + VFPv2       (Thumb mode not supported)
  armebv6t2-           ARMv6T2 + VFPv2
85
86
87
  armebv7a-            ARMv7-A + VFPv3-d16   (default for armeb-)
  armebv7r-            ARMv7-R + VFPv3-d16
  armebv7m-            ARMv7-M + VFPv3-d16
88

89
Options:
90
91
92
  -prefix <dir>        Install in <dir>/bin and <dir>/lib/compcert
  -bindir <dir>        Install binaries in <dir>
  -libdir <dir>        Install libraries in <dir>
93
  -mandir <dir>        Install man pages in <dir>
94
  -coqdevdir <dir>     Install Coq development (.vo files) in <dir>
95
  -toolprefix <pref>   Prefix names of tools ("gcc", etc) with <pref>
96
97
  -use-external-Flocq  Use an already-installed Flocq library
  -use-external-MenhirLib  Use an already-installed MenhirLib library
98
  -no-runtime-lib      Do not compile nor install the runtime support library
99
  -no-standard-headers Do not install nor use the standard .h headers
100
101
  -clightgen           Also compile and install the clightgen tool
  -install-coqdev      Also install the Coq development (implied by -clightgen)
102
  -ignore-coq-version  Accept to use experimental or unsupported versions of Coq
103
'
104

105
106
107
108
#
# Remove Leftover Makefile.config (if any)  (GPR#244)
#
rm -f Makefile.config
109

110
111
112
#
# Parse Command-Line Arguments
#
113
114
while : ; do
  case "$1" in
115
116
    "")
        break;;
117
    -prefix|--prefix)
xleroy's avatar
xleroy committed
118
        prefix="$2"; shift;;
119
    -bindir|--bindir)
xleroy's avatar
xleroy committed
120
        bindir="$2"; shift;;
121
    -libdir|--libdir)
xleroy's avatar
xleroy committed
122
        libdir="$2"; shift;;
123
124
    -mandir|--mandir)
        mandir="$2"; shift;;
125
126
    -coqdevdir|--coqdevdir)
        coqdevdir="$2"; install_coqdev=true; shift;;
xleroy's avatar
xleroy committed
127
128
    -toolprefix|--toolprefix)
        toolprefix="$2"; shift;;
xleroy's avatar
xleroy committed
129
    -no-runtime-lib)
130
        has_runtime_lib=false;;
131
132
    -no-standard-headers)
        has_standard_headers=false;;
133
    -clightgen)
134
135
        clightgen=true
        install_coqdev=true;;
136
137
    -ignore-coq-version|--ignore-coq-version)
        ignore_coq_version=true;;
138
139
    -install-coqdev|--install-coqdev|-install-coq-dev|--install-coq-dev)
        install_coqdev=true;;
140
141
142
143
    -use-external-Flocq|--use-external-Flocq)
        library_Flocq=external;;
    -use-external-MenhirLib|--use-external-MenhirLib)
        library_MenhirLib=external;;
144
145
146
147
148
149
    -help|--help)
        echo "$help"; exit 0;;
    -*)
        echo "Error: unknown option '$1'." 1>&2
        echo "$usage" 1>&2
        exit 2;;
150
151
152
    *)
        if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi
        target="$1";;
153
154
155
156
  esac
  shift
done

157

158
159
160
161
162
#
# Extract Architecture, Model and Default Endianness
#
case "$target" in
  arm-*|armv7a-*)
163
      arch="arm"; model="armv7a"; endianness="little"; bitsize=32;;
164
  armv6-*)
165
      arch="arm"; model="armv6"; endianness="little"; bitsize=32;;
166
167
  armv6t2-*)
      arch="arm"; model="armv6t2"; endianness="little"; bitsize=32;;
168
  armv7r-*)
169
      arch="arm"; model="armv7r"; endianness="little"; bitsize=32;;
170
  armv7m-*)
171
      arch="arm"; model="armv7m"; endianness="little"; bitsize=32;;
172
  armeb-*|armebv7a-*)
173
      arch="arm"; model="armv7a"; endianness="big"; bitsize=32;;
174
  armebv6-*)
175
      arch="arm"; model="armv6"; endianness="big"; bitsize=32;;
176
177
  armebv6t2-*)
      arch="arm"; model="armv6t2"; endianness="big"; bitsize=32;;
178
  armebv7r-*)
179
      arch="arm"; model="armv7r"; endianness="big"; bitsize=32;;
180
  armebv7m-*)
181
      arch="arm"; model="armv7m"; endianness="big"; bitsize=32;;
182
  x86_32-*|ia32-*|i386-*)
183
      arch="x86"; model="32sse2"; endianness="little"; bitsize=32;;
184
  x86_64-*|amd64-*)
185
      arch="x86"; model="64"; endianness="little"; bitsize=64;;
186
  powerpc-*|ppc-*)
187
      arch="powerpc"; model="ppc32"; endianness="big"; bitsize=32;;
188
  powerpc64-*|ppc64-*)
189
      arch="powerpc"; model="ppc64"; endianness="big"; bitsize=32;;
190
  e5500-*)
191
      arch="powerpc"; model="e5500"; endianness="big"; bitsize=32;;
192
193
194
195
  rv32-*)
      arch="riscV"; model="32"; endianness="little"; bitsize=32;;
  rv64-*)
      arch="riscV"; model="64"; endianness="little"; bitsize=64;;
David Monniaux's avatar
David Monniaux committed
196
197
  kvx-*)
      arch="kvx"; model="64"; endianness="little"; bitsize=64;;
Xavier Leroy's avatar
Xavier Leroy committed
198
199
  aarch64-*|arm64-*)
      arch="aarch64"; model="default"; endianness="little"; bitsize=64;;
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
  manual)
      ;;
  "")
      echo "Error: no target architecture specified." 1>&2
      echo "$usage" 1>&2
      exit 2
      ;;
  *)
      echo "Error: unknown target architecture: '$target'." 1>&2
      echo "$usage" 1>&2
      exit 2
      ;;
esac

target=${target#[a-zA-Z0-9]*-}


# Per-target configuration
218
219
220
221
# We start with reasonable defaults,
# then redefine the required parameters for each target,
# then check for missing parameters and derive values for them.

222
asm_supports_cfi=""
223
224
225
226
cc="${toolprefix}gcc"
cc_options=""
casm="${toolprefix}gcc"
casm_options="-c"
227
casmruntime=""
228
clinker="${toolprefix}gcc"
229
clinker_options=""
230
231
232
clinker_needs_no_pie=true
cprepro="${toolprefix}gcc"
cprepro_options="-E"
233
archiver="${toolprefix}ar rcs"
234
235
libmath="-lm"
responsefile="gnu"
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275

#
# ARM Target Configuration
#
if test "$arch" = "arm"; then

  case "$target" in
    eabi|linux)
        abi="eabi"
        ;;
    eabihf|hf|hardfloat)
        abi="hardfloat"
        ;;
    *)
        echo "Error: invalid eabi/system '$target' for architecture ARM." 1>&2
        echo "$usage" 1>&2
        exit 2;;
  esac

  cprepro_options="-std=c99 -U__GNUC__ '-D__REDIRECT(name,proto,alias)=name proto' '-D__REDIRECT_NTH(name,proto,alias)=name proto' -E"
  system="linux"
fi


#
# PowerPC Target Configuration
#
if test "$arch" = "powerpc"; then

  case "$target" in
    eabi|eabi-diab|linux)
        ;;
    *)
        echo "Error: invalid eabi/system '$target' for architecture PowerPC." 1>&2
        echo "$usage" 1>&2
        exit 2;;
  esac

  case "$target" in
    linux)
276
        abi="linux"
277
278
        ;;
    *)
279
        abi="eabi"
280
281
282
283
284
285
        ;;
  esac

  case "$target" in
    eabi-diab)
        asm_supports_cfi=false
286
        casm="${toolprefix}das"
287
        casm_options="-Xalign-value"
288
        cc="${toolprefix}dcc"
289
        clinker_needs_no_pie=false
290
        clinker="${toolprefix}dcc"
291
292
        cprepro="${toolprefix}dcc"
        cprepro_options="-E -D__GNUC__"
293
        archiver="${toolprefix}dar -q"
294
        libmath="-lm"
295
        system="diab"
296
        responsefile="diab"
Bernhard Schommer's avatar
Bernhard Schommer committed
297
        ;;
298
299
    *)
        casmruntime="${toolprefix}gcc -c -Wa,-mregnames"
300
        cprepro_options="-std=c99 -U__GNUC__ -E"
301
302
303
304
305
306
307
        system="linux"
        ;;
  esac
fi


#
308
# x86 (32 bits) Target Configuration
309
#
310
if test "$arch" = "x86" -a "$bitsize" = "32"; then
311
312
313
314

  case "$target" in
    bsd)
        abi="standard"
315
        cc_options="-m32"
316
317
318
319
320
321
322
        casm_options="-m32 -c"
        clinker_options="-m32"
        cprepro_options="-std=c99 -m32 -U__GNUC__ -E"
        system="bsd"
        ;;
    cygwin)
        abi="standard"
323
        cc_options="-m32"
324
325
        casm_options="-m32 -c"
        clinker_options="-m32"
326
        cprepro_options="-std=c99 -m32 -U__GNUC__ '-D__attribute__(x)=' -E"
327
328
329
330
        system="cygwin"
        ;;
    linux)
        abi="standard"
331
        cc_options="-m32"
332
333
334
335
336
337
        casm_options="-m32 -c"
        clinker_options="-m32"
        cprepro_options="-std=c99 -m32 -U__GNUC__ -E"
        system="linux"
        ;;
    *)
338
        echo "Error: invalid eabi/system '$target' for architecture IA32/X86_32." 1>&2
xleroy's avatar
xleroy committed
339
340
        echo "$usage" 1>&2
        exit 2;;
341
342
  esac
fi
343

344
#
Michael Schmidt's avatar
Michael Schmidt committed
345
# x86 (64 bits) Target Configuration
346
#
347
if test "$arch" = "x86" -a "$bitsize" = "64"; then
348
349

  case "$target" in
350
351
    bsd)
        abi="standard"
352
        cc_options="-m64"
353
354
355
356
357
        casm_options="-m64 -c"
        clinker_options="-m64"
        cprepro_options="-std=c99 -m64 -U__GNUC__ -E"
        system="bsd"
        ;;
358
359
    linux)
        abi="standard"
360
        cc_options="-m64"
361
362
363
364
365
        casm_options="-m64 -c"
        clinker_options="-m64"
        cprepro_options="-std=c99 -m64 -U__GNUC__ -E"
        system="linux"
        ;;
Xavier Leroy's avatar
Xavier Leroy committed
366
367
    macos|macosx)
        abi="macos"
368
        cc_options="-arch x86_64"
Xavier Leroy's avatar
Xavier Leroy committed
369
        casm_options="-arch x86_64 -c"
370
        clinker_options="-arch x86_64"
371
        clinker_needs_no_pie=false
372
        cprepro_options="-std=c99 -arch x86_64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E"
Xavier Leroy's avatar
Xavier Leroy committed
373
        libmath=""
Xavier Leroy's avatar
Xavier Leroy committed
374
        system="macos"
Xavier Leroy's avatar
Xavier Leroy committed
375
        ;;
Xavier Leroy's avatar
Xavier Leroy committed
376
377
    cygwin)
        abi="standard"
378
        cc_options="-m64"
Xavier Leroy's avatar
Xavier Leroy committed
379
380
381
382
383
        casm_options="-m64 -c"
        clinker_options="-m64"
        cprepro_options="-std=c99 -m64 -U__GNUC__ '-D__attribute__(x)=' -E"
        system="cygwin"
        ;;
384
385
    *)
        echo "Error: invalid eabi/system '$target' for architecture X86_64." 1>&2
xleroy's avatar
xleroy committed
386
387
        echo "$usage" 1>&2
        exit 2;;
388
389
  esac
fi
390

391

392
393
394
395
396
397
398
399
400
401
#
# RISC-V Target Configuration
#
if test "$arch" = "riscV"; then
  if test "$model" = "64"; then
    model_options="-march=rv64imafd -mabi=lp64d"
  else
    model_options="-march=rv32imafd -mabi=ilp32d"
  fi
  abi="standard"
402
  cc_options="$model_options"
403
404
405
406
407
408
  casm_options="$model_options -c"
  clinker_options="$model_options"
  cprepro_options="$model_options -std=c99 -U__GNUC__ -E"
  system="linux"
fi

409
#
David Monniaux's avatar
David Monniaux committed
410
# KVX Target Configuration
411
#
David Monniaux's avatar
David Monniaux committed
412
if test "$arch" = "kvx"; then
413
414
  #model_options="-march=rv64imafd -mabi=lp64d"
  # FIXME - maybe later add it for NodeOS & cie
Cyril SIX's avatar
Cyril SIX committed
415
416
  #model_options=-m64
  model_options=
417
  abi="standard"
David Monniaux's avatar
David Monniaux committed
418
419
420
421
422
423
424
  if test "$target" = "mbr";
  then os="mbr";
  elif test "$target" = "cos";
  then os="cos";
  elif test "$target" = "elf";
  then os="elf";
  else
David Monniaux's avatar
David Monniaux committed
425
      echo "Unknown KVX backend"
David Monniaux's avatar
David Monniaux committed
426
427
428
      exit 1
  fi
  osupper=`echo $os|tr a-z A-Z`
David Monniaux's avatar
David Monniaux committed
429
  k1base="kvx-$os"
430
  casm="$k1base-as"
431
  casm_options="$model_options"
David Monniaux's avatar
David Monniaux committed
432
433
  cc="$k1base-gcc $model_options"
  clinker="$k1base-gcc"
434
435
436
  bindir="$HOME/.usr/bin"
  libdir="$HOME/.usr/lib"
  clinker_options="$model_options -L$libdir -Wl,-rpath=$libdir"
David Monniaux's avatar
David Monniaux committed
437
  cprepro="$k1base-gcc"
David Monniaux's avatar
David Monniaux committed
438
  cprepro_options="$model_options -D __KVX_${osupper}__ -std=c99 -E -include ccomp_kvx_fixes.h"
439
440
441
442
  libmath="-lm"
  system="linux"
fi

Xavier Leroy's avatar
Xavier Leroy committed
443
444
445
446
447
448
449
450
451
#
# AArch64 (ARMv8 64 bits) Target Configuration
#
if test "$arch" = "aarch64"; then
  case "$target" in
    linux)
        abi="standard"
        cprepro_options="-std=c99 -U__GNUC__ -E"
        system="linux";;
Xavier Leroy's avatar
Xavier Leroy committed
452
    macos|macosx)
Xavier Leroy's avatar
Xavier Leroy committed
453
454
455
456
457
458
459
        abi="apple"
        casm="${toolprefix}cc"
        casm_options="-c -arch arm64"
        cc="${toolprefix}cc -arch arm64"
        clinker="${toolprefix}cc"
        clinker_needs_no_pie=false
        cprepro="${toolprefix}cc"
460
        cprepro_options="-std=c99 -arch arm64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E"
Xavier Leroy's avatar
Xavier Leroy committed
461
        libmath=""
Xavier Leroy's avatar
Xavier Leroy committed
462
        system="macos"
Xavier Leroy's avatar
Xavier Leroy committed
463
        ;;
Xavier Leroy's avatar
Xavier Leroy committed
464
465
466
467
468
469
470
    *)
        echo "Error: invalid eabi/system '$target' for architecture AArch64." 1>&2
        echo "$usage" 1>&2
        exit 2;;
  esac
fi

471

472
473
474
475
476
#
# Finalize Target Configuration
#
if test -z "$casmruntime"; then casmruntime="$casm $casm_options"; fi

477

478
479
480
481
482
483
484
485
486
487
488
489
# Invoke a C compiler, e.g. to check for availability of command-line options
testcompiler () {
    tmpsrc="${TMPDIR:-/tmp}/compcert-configure-$$.c"
    rm -f "$tmpsrc"
    tmpout="${TMPDIR:-/tmp}/compcert-configure-$$.out"
    rm -f "$tmpout"
    cat >> "$tmpsrc" <<EOF
int main (void)
{
   return 0;
}
EOF
490
    errout=$("$@" -o "$tmpout" "$tmpsrc" 2>&1 >/dev/null)
491
    retcode=$?
492
    errcount=$(echo "${errout}" | grep -ciE "(unknown|unsupported|unrecognized).*(option|argument)")
493
    rm -f "$tmpsrc" "$tmpout"
494
495
496
497
    # Test failed or error is logged to stderr
    if [ "${retcode}" != "0" ] || [ "${errcount}" != "0" ]; then return 1; fi
    # OK and no error was logged
    return 0
498
499
}

500

501
502
503
#
# Test Assembler Support for CFI Directives
#
504
if test "$target" != "manual" && test -z "$asm_supports_cfi"; then
xleroy's avatar
xleroy committed
505
  echo "Testing assembler support for CFI directives... " | tr -d '\n'
506
507
508
  tmpsrc="${TMPDIR:-/tmp}/compcert-configure-$$.s"
  rm -f "$tmpsrc"
  cat >> "$tmpsrc" <<EOF
509
testfun:
510
511
512
513
514
  .file 1 "testfun.c"
  .loc 1 1
  .cfi_startproc
  .cfi_adjust_cfa_offset 16
  .cfi_endproc
515
EOF
516
  if $casm $casm_options -o /dev/null "$tmpsrc" 2>/dev/null
xleroy's avatar
xleroy committed
517
518
  then echo "yes"; asm_supports_cfi=true
  else echo "no";  asm_supports_cfi=false
519
  fi
520
  rm -f "$tmpsrc"
521
522
fi

xleroy's avatar
xleroy committed
523

524
#
525
# Test Availability of Option '-no-pie' or '-nopie'
526
527
#
if ($clinker_needs_no_pie) then
528
  echo "Testing linker support for '-no-pie' / '-nopie' option... " | tr -d '\n'
529
  if testcompiler ${cc} -no-pie;
530
531
532
  then echo "yes, '-no-pie'"; clinker_options="${clinker_options} -no-pie"
  elif testcompiler ${cc} -nopie;
  then echo "yes, '-nopie'"; clinker_options="${clinker_options} -nopie"
533
534
535
536
537
  else echo "no"; clinker_needs_no_pie=false
  fi
fi


538
539
540
#
# Test Availability of Required Tools
#
xleroy's avatar
xleroy committed
541
542
543
missingtools=false

echo "Testing Coq... " | tr -d '\n'
544
coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')
xleroy's avatar
xleroy committed
545
case "$coq_ver" in
546
  8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0|8.12.1|8.12.2|8.13.0|8.13.1|8.13.2)
xleroy's avatar
xleroy committed
547
        echo "version $coq_ver -- good!";;
548
  ?*)
xleroy's avatar
xleroy committed
549
        echo "version $coq_ver -- UNSUPPORTED"
550
551
552
        if $ignore_coq_version; then
            echo "Warning: this version of Coq is unsupported, proceed at your own risks."
        else
553
            echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.13.2"
554
555
            missingtools=true
        fi;;
556
  "")
xleroy's avatar
xleroy committed
557
        echo "NOT FOUND"
Xavier Leroy's avatar
Xavier Leroy committed
558
        echo "Error: make sure Coq version 8.12.2 is installed."
xleroy's avatar
xleroy committed
559
560
561
562
        missingtools=true;;
esac

echo "Testing OCaml... " | tr -d '\n'
Xavier Leroy's avatar
Xavier Leroy committed
563
ocaml_ver=`ocamlc -version 2>/dev/null`
xleroy's avatar
xleroy committed
564
case "$ocaml_ver" in
565
  4.00.*|4.01.*| 4.02.*|4.03.*|4.04.*|4.05.*)
566
        echo "version $ocaml_ver -- UNSUPPORTED"
567
        echo "Error: CompCert requires OCaml version 4.06 or later."
568
        missingtools=true;;
569
  4.*)
xleroy's avatar
xleroy committed
570
571
572
        echo "version $ocaml_ver -- good!";;
  ?.*)
        echo "version $ocaml_ver -- UNSUPPORTED"
573
        echo "Error: CompCert requires OCaml version 4.05 or later."
xleroy's avatar
xleroy committed
574
575
576
        missingtools=true;;
  *)
        echo "NOT FOUND"
577
        echo "Error: make sure OCaml version 4.05 or later is installed."
xleroy's avatar
xleroy committed
578
579
580
        missingtools=true;;
esac

Xavier Leroy's avatar
Xavier Leroy committed
581
582
583
584
585
586
587
588
589
590
echo "Testing OCaml native-code compiler..." | tr -d '\n'
ocamlopt_ver=`ocamlopt -version 2>/dev/null`
if test "$ocamlopt_ver" = "$ocaml_ver"; then
  echo "yes"
  ocaml_native_comp=true
else
  echo "no, will build to bytecode only"
  ocaml_native_comp=false
fi

591
echo "Testing OCaml .opt compilers... " | tr -d '\n'
Xavier Leroy's avatar
Xavier Leroy committed
592
593
ocamlopt_opt_ver=`ocamlopt.opt -version 2>/dev/null`
if test "$ocamlopt_opt_ver" = "$ocaml_ver"; then
594
595
596
597
598
599
600
  echo "yes"
  ocaml_opt_comp=true
else
  echo "no, will do without"
  ocaml_opt_comp=false
fi

601
MENHIR_REQUIRED=20190626
xleroy's avatar
xleroy committed
602
echo "Testing Menhir... " | tr -d '\n'
603
menhir_ver=`menhir --version 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'`
xleroy's avatar
xleroy committed
604
case "$menhir_ver" in
605
  20[0-9][0-9][0-9][0-9][0-9][0-9])
606
      if test "$menhir_ver" -ge $MENHIR_REQUIRED; then
607
          echo "version $menhir_ver -- good!"
608
609
          menhir_dir=$(ocamlfind query menhirLib 2>/dev/null) || \
          menhir_dir=$(menhir --suggest-menhirLib) || \
610
          menhir_dir=""
611
          menhir_dir=$(echo "$menhir_dir" | tr -d '\r' | tr '\\' '/')
612
          if test ! -d "$menhir_dir"; then
613
614
615
616
617
              echo "Error: cannot determine the location of the Menhir API library."
              echo "This can be due to an incorrect Menhir package."
              echo "Consider using the OPAM package for Menhir."
              missingtools=true
          fi
618
      else
619
          echo "version $menhir_ver -- UNSUPPORTED"
620
          echo "Error: CompCert requires a version greater or equal to $MENHIR_REQUIRED."
621
          missingtools=true
622
      fi;;
xleroy's avatar
xleroy committed
623
624
  *)
        echo "NOT FOUND"
625
        echo "Error: make sure Menhir version $MENHIR_REQUIRED or later is installed."
xleroy's avatar
xleroy committed
626
627
628
        missingtools=true;;
esac

629
echo "Testing GNU make... " | tr -d '\n'
630
631
make=''
for mk in make gmake gnumake; do
Xavier Leroy's avatar
Xavier Leroy committed
632
  make_ver=`$mk -v 2>/dev/null | head -1 | sed -n -e 's/^GNU Make //p'`
633
634
635
636
637
638
639
  case "$make_ver" in
    3.8*|3.9*|[4-9].*)
        echo "version $make_ver (command '$mk') -- good!"
        make="$mk"
        break;;
  esac
done
640
if test -z "$make"; then
641
642
643
644
645
  echo "NOT FOUND"
  echo "Error: make sure GNU Make version 3.80 or later is installed."
  missingtools=true
fi

xleroy's avatar
xleroy committed
646
647
648
649
650
if $missingtools; then
  echo "One or several required tools are missing or too old.  Aborting."
  exit 2
fi

651
652
653
#
# Generate Makefile.config
#
654
655
sharedir="$(dirname "$bindir")"/share

656
657
658
659
660
rm -f Makefile.config
cat > Makefile.config <<EOF
PREFIX=$prefix
BINDIR=$bindir
LIBDIR=$libdir
661
MANDIR=$mandir
662
SHAREDIR=$sharedir
663
COQDEVDIR=$coqdevdir
Xavier Leroy's avatar
Xavier Leroy committed
664
OCAML_NATIVE_COMP=$ocaml_native_comp
665
OCAML_OPT_COMP=$ocaml_opt_comp
666
MENHIR_DIR=$menhir_dir
667
668
COMPFLAGS=-bin-annot
EOF
xleroy's avatar
xleroy committed
669
670
671

if test "$target" != "manual"; then
cat >> Makefile.config <<EOF
672
ABI=$abi
673
674
ARCH=$arch
ASM_SUPPORTS_CFI=$asm_supports_cfi
675
BITSIZE=$bitsize
676
CASM=$casm
677
CASM_OPTIONS=$casm_options
678
CASMRUNTIME=$casmruntime
679
CC=$cc $cc_options
680
CLIGHTGEN=$clightgen
681
CLINKER=$clinker
682
CLINKER_OPTIONS=$clinker_options
683
684
CPREPRO=$cprepro
CPREPRO_OPTIONS=$cprepro_options
685
ARCHIVER=$archiver
686
ENDIANNESS=$endianness
687
HAS_RUNTIME_LIB=$has_runtime_lib
688
HAS_STANDARD_HEADERS=$has_standard_headers
689
INSTALL_COQDEV=$install_coqdev
690
691
LIBMATH=$libmath
MODEL=$model
692
OS=${os:-unspecified}
693
SYSTEM=$system
694
RESPONSEFILE=$responsefile
695
696
LIBRARY_FLOCQ=$library_Flocq
LIBRARY_MENHIRLIB=$library_MenhirLib
697
EOF
xleroy's avatar
xleroy committed
698
699
700
701
702
703
else
cat >> Makefile.config <<'EOF'

# Target architecture
# ARCH=powerpc
# ARCH=arm
704
# ARCH=x86
Xavier Leroy's avatar
Xavier Leroy committed
705
706
# ARCH=riscV
# ARCH=aarch6
xleroy's avatar
xleroy committed
707
708
ARCH=

709
# Hardware variant
710
711
712
713
# MODEL=ppc32       # for plain PowerPC
# MODEL=ppc64       # for PowerPC with 64-bit instructions
# MODEL=e5500       # for Freescale e5500 PowerPC variant
# MODEL=armv6       # for ARM
714
# MODEL=armv6t2     # for ARM
715
716
717
# MODEL=armv7a      # for ARM
# MODEL=armv7r      # for ARM
# MODEL=armv7m      # for ARM
718
719
# MODEL=32sse2      # for x86 in 32-bit mode
# MODEL=64          # for x86 in 64-bit mode
Xavier Leroy's avatar
Xavier Leroy committed
720
# MODEL=default     # for others
721
722
MODEL=

xleroy's avatar
xleroy committed
723
# Target ABI
724
725
726
# ABI=eabi          # for PowerPC / Linux and other SVR4 or EABI platforms
# ABI=eabi          # for ARM
# ABI=hardfloat     # for ARM
Xavier Leroy's avatar
Xavier Leroy committed
727
# ABI=standard      # for others
728
ABI=
xleroy's avatar
xleroy committed
729

730
# Target bit width
Xavier Leroy's avatar
Xavier Leroy committed
731
# BITSIZE=64        # for x86 in 64-bit mode, RiscV in 64-bit mode, AArch64
732
733
734
# BITSIZE=32        # otherwise
BITSIZE=

735
736
# Target endianness
# ENDIANNESS=big     # for ARM or PowerPC
Xavier Leroy's avatar
Xavier Leroy committed
737
# ENDIANNESS=little  # for ARM or x86 or RiscV or AArch64
738
739
ENDIANNESS=

xleroy's avatar
xleroy committed
740
# Target operating system and development environment
741
#
xleroy's avatar
xleroy committed
742
743
744
# Possible choices for PowerPC:
# SYSTEM=linux
# SYSTEM=diab
745
#
Xavier Leroy's avatar
Xavier Leroy committed
746
# Possible choices for ARM, AArch64, RiscV:
xleroy's avatar
xleroy committed
747
# SYSTEM=linux
748
#
749
# Possible choices for x86:
750
751
# SYSTEM=linux
# SYSTEM=bsd
Xavier Leroy's avatar
Xavier Leroy committed
752
# SYSTEM=macos
753
# SYSTEM=cygwin
xleroy's avatar
xleroy committed
754
755
SYSTEM=

756
757
# C compiler (for testing only)
CC=cc
xleroy's avatar
xleroy committed
758

759
760
761
# Assembler for assembling compiled files
CASM=cc
CASM_OPTIONS=-c
xleroy's avatar
xleroy committed
762

763
# Assembler for assembling runtime library files
764
CASMRUNTIME=$(CASM) $(CASM_OPTIONS)
765

xleroy's avatar
xleroy committed
766
# Linker
767
768
769
770
771
772
CLINKER=cc
CLINKER_OPTIONS=-no-pie

# Preprocessor for .c files
CPREPRO=cc
CPREPRO_OPTIONS=-std c99 -U__GNUC__ -E
xleroy's avatar
xleroy committed
773

774
775
# Archiver to build .a libraries
ARCHIVER=ar rcs
xleroy's avatar
xleroy committed
776

777
# Math library. Set to empty under macOS
xleroy's avatar
xleroy committed
778
779
LIBMATH=-lm

780
# Turn on/off the installation and use of the runtime support library
781
HAS_RUNTIME_LIB=true
782

783
784
785
# Turn on/off the installation and use of the standard header files
HAS_STANDARD_HEADERS=true

786
787
788
789
# Whether the assembler $(CASM) supports .cfi debug directives
ASM_SUPPORTS_CFI=false
#ASM_SUPPORTS_CFI=true

790
791
792
# Turn on/off compilation of clightgen
CLIGHTGEN=false

793
794
# Whether the other tools support responsefiles in GNU syntax or Diab syntax
RESPONSEFILE=gnu  # diab
795

796
797
798
# Whether to use the local copies of Flocq and MenhirLib
LIBRARY_FLOCQ=local      # external
LIBRARY_MENHIRLIB=local  # external
xleroy's avatar
xleroy committed
799
800
EOF
fi
801

802
if [ "$arch" = "aarch64" ]; then # for aarch64 scheduling
Sylvain Boulmé's avatar
Sylvain Boulmé committed
803
cat >> Makefile.config <<EOF
Sylvain Boulmé's avatar
Sylvain Boulmé committed
804
ARCHDIRS=$arch scheduling/abstractbb scheduling/postpass_lib
Léo Gourdin's avatar
Léo Gourdin committed
805
BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList.v \\
806
    Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asm.v Asmblockprops.v\\
807
    ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\
808
    Asmblockdeps.v\\
809
810
811
812
    AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v\\
    ImpConfig.v ImpCore.v ImpExtern.v ImpHCons.v ImpIO.v ImpLoops.v ImpMonads.v ImpPrelude.v
    # TODO: UPDATE THIS
    # DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v
813
EXTRA_EXTRACTION=   Asmgen.Asmgen_expand.loadimm32 Asmgen.Asmgen_expand.addimm64 Asmgen.Asmgen_expand.storeptr
Sylvain Boulmé's avatar
Sylvain Boulmé committed
814
815
816
EOF
fi

David Monniaux's avatar
David Monniaux committed
817
if [ "$arch" = "kvx" ]; then
818
cat >> Makefile.config <<EOF
Sylvain Boulmé's avatar
Sylvain Boulmé committed
819
ARCHDIRS=$arch scheduling/abstractbb scheduling/postpass_lib
David Monniaux's avatar
David Monniaux committed
820
821
822
EXECUTE=kvx-cluster --syscall=libstd_scalls.so --
CFLAGS= -D __KVX_COS__
SIMU=kvx-cluster -- 
Sylvain Boulmé's avatar
Sylvain Boulmé committed
823
BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\
824
    Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\
825
    ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\
Cyril SIX's avatar
Cyril SIX committed
826
    Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\
827
    AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v
828
829
830
EOF
fi

David Monniaux's avatar
David Monniaux committed
831
832
if [ "$arch" = "riscV" ] ; then
cat >> Makefile.config <<EOF
David Monniaux's avatar
David Monniaux committed
833
EXTRA_EXTRACTION=Asm.ireg_eq Asm.ireg0_eq
David Monniaux's avatar
David Monniaux committed
834
835
836
837
BACKENDLIB=Asmgenproof0.v Asmgenproof1.v ExtValues.v
EOF
fi

838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
#
# Generate Merlin and CoqProject files to simplify development
#
cat > .merlin <<EOF
S lib
S common
S $arch
S backend
S cfrontend
S driver
S debug
S exportclight
S cparser
S extraction

B lib
B common
B $arch
B backend
B cfrontend
B driver
B debug
B exportclight
B cparser
B extraction
EOF

865
$make CoqProject
866

867
868
869
870
#
# Clean up target-dependent files to force their recompilation
#
rm -f .depend $arch/Archi.vo ${arch}_${bitsize}/Archi.vo runtime/*.o
871

872
873
874
#
# Summarize Configuration
#
xleroy's avatar
xleroy committed
875
876
877
if test "$target" = "manual"; then
cat <<EOF

xleroy's avatar
xleroy committed
878
Please finish the configuration by editing file ./Makefile.config.
xleroy's avatar
xleroy committed
879
880
881
882

EOF
else

883
884
885
expandprefix() {
  echo "$1" | sed -e "s|\\\$(PREFIX)|$prefix|"
}
xleroy's avatar
xleroy committed
886

887
888
889
cat <<EOF

CompCert configuration:
xleroy's avatar
xleroy committed
890
    Target architecture........... $arch
891
892
    Hardware model................ $model
    Application binary interface.. $abi
893
    Endianness.................... $endianness
xleroy's avatar
xleroy committed