aboutsummaryrefslogtreecommitdiffstats
path: root/configure
Commit message (Collapse)AuthorAgeFilesLines
* Removed folders from .merlin.Bernhard Schommer2016-11-091-4/+0
|
* Added ${arch}_${bitsize} for x86 to .merlinBernhard Schommer2016-11-091-1/+4
|
* allow Cow version 8.5pl3Michael Schmidt2016-11-041-1/+1
|
* Merge pull request #145 from AbsInt/64Xavier Leroy2016-10-271-28/+86
|\ | | | | | | Support for 64-bit target processors + support for x86 in 64-bit mode
| * Documentation updates to mention 64-bit mode and x86_64 portXavier Leroy2016-10-271-5/+8
| |
| * Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ↵Xavier Leroy2016-10-271-25/+33
| | | | | | | | | | | | | | | | | | | | | | | | -> x86/x86_32/x86_64 Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq. This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86. While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures. Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).
| * configure for ia32-macosx: update for MacOS 10.12Xavier Leroy2016-10-131-1/+1
| |
| * x86-64 MacOS X supportXavier Leroy2016-10-111-0/+16
| | | | | | | | | | - Avoid absolute addressing for labels, use RIP-relative addressing - Different, RIP-relative implementation of jump tables
| * Support for 64-bit architectures: x86 in 64-bit modeXavier Leroy2016-10-011-4/+35
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit enriches the IA32 port so that it supports x86 processors in 64-bit mode as well as in 32-bit mode, depending on the value of Archi.ptr64, which itself is set from the configuration model. To activate x86-64 bit support, configure with "x86_64-linux". Main steps: - Enrich Op.v and Asm.v with 64-bit operations - SelectLong: in 64-bit mode, use 64-bit operations directly; in 32-bit mode, fall back on the old implementation based on pairs of 32-bit integers - Conventions1: support x86-64 ABI in addition to the 32-bit ABI. - Add support for the new 64-bit operations everywhere. - runtime/x86_64: implementation of the supporting library appropriate for x86 in 64-bit mode To do: - More optimizations are possible on 64-bit integer arithmetic operations. - Could add new chunks to load, say, an unsigned byte into a 64-bit long (currently we load as a 32-bit int then zero-extend). - Implements the wrong ABI for struct passing.
* | Merge pull request #147 from m-schmidt/masterXavier Leroy2016-10-241-0/+1
|\ \ | | | | | | Add a man page
| * | Add a man-pageMichael Schmidt2016-10-141-0/+1
| | |
* | | Query menhir for location of menhir lib in config.Bernhard Schommer2016-10-181-1/+3
|/ / | | | | | | | | | | Since the menhir version required supports the --suggest-menhirLib flag we can query it already in the configure script simplifying the Makefile.menhir
* / Added configure switch for merlin.Bernhard Schommer2016-10-061-0/+35
|/ | | | | | The new configure switch generates a .merlin file and adds the -bin-annot flag to the compile options. Bug 20081
* undefine _Nullable to add some compatibility with macOS 10.12 SDKMichael Schmidt2016-09-231-1/+1
|
* fix merge conflictsMichael Schmidt2016-08-171-0/+6
|\
| * Added support for quoting for diab backend.Bernhard Schommer2016-07-211-1/+1
| | | | | | | | | | | | The diab data compiler has different quoting conventions compared to the gnu tools. Bug 18308.
| * Added simplified reader and printer for gnu @filesBernhard Schommer2016-07-201-0/+6
| | | | | | | | | | | | | | | | The functions expandargv and writeargv resemble the functions from the libiberity that are used by the gnu tools. Additionaly a new configuration is added in order to determine which kind of response files are supported for calls to other tools. Bug 18308
* | update help text in configure scriptMichael Schmidt2016-08-081-13/+14
| |
* | port fix for configure from m-schmidt/EndiannessPlaygroundMichael Schmidt2016-08-071-0/+5
| |
* | Changed configure target for arm big endian.Bernhard Schommer2016-08-051-27/+12
| | | | | | | | | | | | Instead of an addition -little or -big at the end the configure script now accepts armeb* for the big endian arm targets. Bug 19418
* | Implement support for big endian arm targets.Bernhard Schommer2016-08-051-204/+307
|/ | | | | | | | Adds support for the big endian arm targets by making the target endianess flag configurable, adding support for the big endian calling conventions, rewriting memory access patterns and adding big endian versions of the runtime functions. Bug 19418
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-3/+3
| | | | | Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
* Added back ;;Bernhard Schommer2016-06-281-0/+1
|
* Activate advanced debug information for arm, ia32.Bernhard Schommer2016-06-281-4/+0
| | | | | | The configuration advanced debug is removed and now full debug information is also generated for ia32 and arm. Bug 17609
* Respect COQBIN in configure script.Bernhard Schommer2016-05-131-1/+1
|
* configure: bump Menhir required version to 20160303Xavier Leroy2016-05-111-1/+1
| | | | Earlier versions of Menhir run into "string too long" errors in Coq when building on a 32-bit platform.
* fix typo 'clinker_option' in configure for OSXMichael Schmidt2016-05-101-2/+2
|
* fix typo in commentMichael Schmidt2016-05-101-1/+1
|
* fix typo 'clinker_option' in configure for OSXMichael Schmidt2016-05-101-6/+10
|
* configure: fix test for CFI directivesXavier Leroy2016-03-211-1/+1
| | | | The test was failing as a consequence of the split casm -> casm / casm_options.
* Merge branch 'master' into cleanupBernhard Schommer2016-03-211-0/+1
|\
| * Add -Xalign-value to enforce correct alignment.Bernhard Schommer2016-03-181-2/+3
| | | | | | | | | | | | The diab compiler seems to interpret the alignment as power of two instead of the value. Bug 18490
* | Revert "Add the -Xalign-value options for diab."Bernhard Schommer2016-03-181-1/+0
| | | | | | | | This reverts commit 771d8576fbae8bd48f6bc80c74722ce1c7cc5259.
* | Add the -Xalign-value options for diab.Bernhard Schommer2016-03-181-0/+1
| | | | | | | | | | | | The default of the diab compiler is to interpret the alignment as power of two. Bug 18490.
* | Upgrade ocaml version needed and enable more warnings.Bernhard Schommer2016-03-101-5/+9
|/ | | | | | | | | | | Since the menhir version we use requires ocaml>4.02 we can also upgrade the required ocaml version to >4.02 and remove the deprecate String functions. Also we now activate all warnings except for 4,9 und 27 for regular code plus a bunch of warnings for the generated code. 4 and 9 are not really usefull and 27 is deactivated since until the usage string is printed in a way that requires no newline. Bug 18394.
* Split up tools and options.Bernhard Schommer2016-02-251-19/+42
| | | | | | Added additional configuration entries to seperate tools from options in the .ini files. Internally they are just concatenated in Configuration.ml which allows it to still use old .ini files.
* Added configuration to enable clightgen build.Bernhard Schommer2015-12-281-0/+8
| | | | The new configuration option -clightgen activates the build of clightgen.
* Change one line in [Lexer.mll] to obey API change in Menhir 20151110.François Pottier2015-11-101-1/+1
| | | | Update configure to require Menhir 20151110.
* Merge remote branch 'upstream/master' into cleanFrançois Pottier2015-10-231-50/+36
|\ | | | | | | | | Conflicts: Makefile.extr
| * Removal of cchecklink, superseded by AbsInt's Valex tool.Xavier Leroy2015-10-121-26/+6
| |
| * Merge branch 'master' into ppc64Xavier Leroy2015-10-111-1/+2
| |\ | | | | | | | | | Resolved conflicts in:configure powerpc/Asmexpand.ml
| * | Use PowerPC 64 bits instructions (when available) for int<->FP conversions.Xavier Leroy2015-09-131-26/+32
| | | | | | | | | | | | | | | | | | Also: implement __builtin_isel on non-EREF platforms with a branch-free instruction sequence. Also: extend ./configure so that it recognizes "ppc64-" and "e5500-" platforms in addition to "ppc-".
* | | Updated [configure] to require today's Menhir.François Pottier2015-10-231-3/+4
| |/ |/|
* | Activate the advanced debug for the gcc build.Bernhard Schommer2015-10-031-1/+2
|/
* Better define the __GNUC__ macro which avoids the inclusion of va_list ↵Bernhard Schommer2015-07-071-1/+1
| | | | header and set the __VA_LIST macro if it is not defined.
* Added an define to avoid the inclusion of the diab va_list header which ↵Bernhard Schommer2015-07-071-1/+1
| | | | defined the incompatible vararg type.
* Provide and use compiler-dependent standard headers.Xavier Leroy2015-04-251-1/+11
| | | | | | | | | | | | This branch provides implementations of the following standard headers: <float.h> <stdarg.h> <stdbool.h> <stddef.h> <varargs.h> These are the headers that are provided by GCC and Clang, as opposed to being provided by Glibc and similar C standard libraries. Configuration flag "-no-standard-headers" deactivates the installation and use of these headers. Lightly tested so far (IA32 Linux).
* Merge branch 'master' into dwarfBernhard Schommer2015-04-141-6/+6
|\
| * When using gcc as a preprocessor, put it in C99 mode.Xavier Leroy2015-04-101-6/+6
| | | | | | | | As opposed to the default "gnu99" mode, the C99 mode turns off a number of GNU-isms in standard header files like those of glibc.
* | Merge branch 'master' into dwarfBernhard Schommer2015-03-311-2/+34
|\| | | | | | | | | | | Conflicts: Makefile driver/Driver.ml
generated by cgit (git 2.34.1) at 2024-06-28 22:14:59 +0000