aboutsummaryrefslogtreecommitdiffstats
path: root/configure
Commit message (Collapse)AuthorAgeFilesLines
* oubli DecBoolOps.vDavid Monniaux2019-05-061-1/+1
|
* Fixing Coq dependenciesCyril SIX2019-05-031-1/+1
|
* cleaner: put all the special types, defines etc. in one header fileDavid Monniaux2019-04-111-1/+1
|
* Integrating Asmvliw.v in the proof chainCyril SIX2019-03-201-1/+1
|
* Merge branch 'master' into mppa_postpassCyril SIX2019-03-131-5/+6
|\ | | | | | | | | | | Conflicts: .gitignore runtime/include/stdbool.h
| * Maximum supported Menhir version (#275)Xavier Leroy2019-02-261-1/+1
| | | | | | | | | | Follow-up to commit fc9bc643. The latest Menhir version compatible with the current code base is actually 20181113.
| * Maximum supported Menhir version (#275)Jacques-Henri Jourdan2019-02-251-2/+3
| | | | | | The Coq backend of Menhir will soon enjoy a large refactoring, making it incompatible with the version of MenhirLib currently in CompCert. This commit adds a check in configure to make sure that the version of Menhir is not more modern than the current one (20181026).
| * Add support for Coq 8.9.0Xavier Leroy2019-02-041-3/+3
| | | | | | | | No other changes are needed to support 8.9.0.
* | Plugged Asmblockdeps into PostpassSchedulingCyril SIX2019-02-251-0/+1
| |
* | Added AbstractBasicBlock files to the Coq build processCyril SIX2019-02-131-4/+6
| |
* | pour ne plus être embêtés avec le int128David Monniaux2019-01-301-1/+1
| |
* | no __SIZEOF_INT128__David Monniaux2019-01-301-1/+1
| | | | | | | | J'avais fait une erreur, les __SSE__ c'était quand je compilais sur x86.
* | Rajouté -U__SSE__ -U__SSE2__ dans le ./configure pour le K1Cyril SIX2019-01-301-1/+1
| |
* | configure: improve preprocessor optionsSylvain Boulmé2019-01-181-1/+1
| |
* | fix oubli dans configureSylvain Boulmé2019-01-181-1/+1
| |
* | BROKEN - works for x86, not for k1 anymoreCyril SIX2018-11-261-0/+3
| |
* | Moved some files to mppa_k1c/lib ; reworked configure and Makefile to allow thatCyril SIX2018-11-261-0/+6
| |
* | Merge tag 'v3.4' into mppa_k1cCyril SIX2018-11-211-8/+51
|\| | | | | | | | | Conflicts: .gitignore
| * Tentatively support Coq 8.8.2Xavier Leroy2018-09-121-2/+2
| | | | | | | | | | It's not out yet, but based on the state of the v8.8 branch of Coq, it is very likely to be compatible with CompCert.
| * Improve reporting of configuration errorsXavier Leroy2018-08-281-0/+10
| | | | | | | | | | | | | | | | | | | | | | | | The full "usage" text is so long that the actual error message scrolls off the screen. With this commit, instead, a short (3-line) error message is printed, with a suggestion to do `./configure -help`. The whole "usage" text is printed by `./configure -help`. Also: better error message for unknown options (arguments starting with `-`).
| * Remove leftover Makefile.config before configurationXavier Leroy2018-08-281-0/+4
| | | | | | | | | | | | | | So that if an error occurs during configuration, there is no Makefile.config file and "make" will fail. Closes: #244
| * Support Coq 8.8.1 (#242)Xavier Leroy2018-07-101-3/+3
| |
| * Ensure compatibility with Menhir before and after version 20180530Xavier Leroy2018-06-061-3/+9
| | | | | | | | Inspired by and adapted from pull request #235 by Benoît Viguier.
| * Fix menhirLib namespaces, following changes in Menhir version 20180530Jacques-Henri Jourdan2018-06-061-1/+1
| |
| * Install Coq development (.vo files) if requested (#232)Xavier Leroy2018-05-301-3/+26
| | | | | | | | | | | | | | | | | | .vo files are installed if configure options -install-coqdev or -clightgen or -coqdevdir are given. Installation directory is $(PREFIX)/lib/compcert/coq by default and can be changed by configure option -coqdevdir. Closes: #227
| * Support Coq version 8.8.0Xavier Leroy2018-04-251-3/+3
| |
* | Fixing k1-gcc becoming k1-mbr-gccCyril SIX2018-11-091-5/+6
| |
* | Fixed CompCert library inclusion. Indirect fix for udivd and umoddCyril SIX2018-06-261-1/+3
| |
* | MPPA - Fixed -m64 missingCyril SIX2018-04-261-1/+1
| |
* | Hook for MPPA_K1c (generates Risc-V code for now)Cyril SIX2018-04-041-0/+22
|/
* Support Coq 8.7.2Xavier Leroy2018-02-191-3/+3
|
* Removed struct passing/return from ConfigurationsBernhard Schommer2018-02-161-40/+0
|
* Rename abi for ppc-linux targets.Bernhard Schommer2018-02-161-2/+2
|
* Fix typo in commentMichael Schmidt2018-02-161-1/+1
|
* Add support for x86_64 BSD (#56)Xavier Leroy2018-02-091-3/+19
|
* Configure check for PIE (#55)Michael Schmidt2018-02-081-5/+12
| | | | | When checking for -no-pie and -nopie, evaluate gcc output for error message like 'unknown argument'. (Relying on the error code is not enough.)
* Removed superfluous check.Bernhard Schommer2018-02-061-4/+0
|
* Improved message recommending an OCaml version to useXavier Leroy2018-01-131-1/+1
|
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-051-0/+3
| | | | | | | | | | | Some files are dual-licensed (GPL + noncommercial license), as marked redundantly in the license headers of those files, and in the LICENSE file. OVer the years those two markings got inconsistent. This commit updates the LICENSE file and the license headers of some files so that they agree on which files are dual-licensed. Some build-related files were dual-licensed but some others were not. Fixed by dual-licensing configure, Makefile.menhir, extraction/extraction.v, */extractionMachdep.v Moved lib/Json* to backend/ because there is no need to dual-license those files, yet lib/* is dual-licensed. Plus: JsonAST did not really belong in lib/ anyway, as it depends on AST which is not in lib/
* Coq 8.7.1 supportXavier Leroy2017-12-181-3/+3
| | | | It is compatible with 8.7.0 and 8.6.1, no changes required to the Coq sources of CompCert.
* Coq 8.7.0 supportXavier Leroy2017-10-201-3/+3
| | | | | | configure: accept Coq 8.7.0 and 8.6.1. (Coq 8.6 became incompatible with commit b4f59c4.) Changelog: updated.
* Take advantage of ARMv6T2/ARMv7 instructions even if not in Thumb2 mode (#203)Gergö Barany2017-09-181-2/+9
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Clarify that ARMv6 is in fact ARMv6T2 The ARMv6 comes in two flavors depending on the version of the Thumb instruction set supported: ARMv6 for the original Thumb, ARMv6T2 for Thumb2. CompCert only supports Thumb2, so its ARMv6 architecture should really be called ARMv6T2. This makes a difference: the GNU assembler rejects most of the instructions CompCert generates for ARMv6 with "-mthumb" if the architecture is specified as ".arch armv6" as opposed to ".arch armv6t2". This patch fixes the architecture specification in the target printer and the internal name of the architecture. It does not change the configure script's flags to avoid breaking changes. * Always use ARM movw/movt to load large immediates These move-immediate instructions used to be only emitted in Thumb mode, not in ARM mode. As far as I understand ARM's documentation, these instructions are available in *both* modes in ARMv6T2 and above. This should cover all of CompCert's ARM targets. Tested for ARMv6 and ARMv7, both with and without Thumb2. The behavior is now identical to Clang, and the GNU assembler accepts these instructions in all configurations. * Separate ARMv6 and ARMv6T2; no movw/movt on ARMv6 - define separate architecture models for ARMv6 and ARMv6T2 - introduce `Archi.move_imm` parameter on ARM to identify models with `movw`/`movt` move-immediate instructions (all except ARMv6, in both ARM and Thumb mode) * Fixes for support for architectures with Thumb2 - rename relevant parameter to `Archi.thumb2_support` - on ARMv6 without Thumb2, silently accept -marm flag (but not -mthumb) - allow generation of `sbfx` in ARM mode if Thumb2 is supported
* configure for x86-32/Cygwin: ignore __attribute__Xavier Leroy2017-09-111-1/+1
| | | | Even with __GNUC__ undefined, the standard header files contain bizarre __attribute__ declarations that CompCert fails to parse.
* configure: Wording and formatting of the Skylake/OCaml warningXavier Leroy2017-08-181-2/+3
|
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2017-07-311-1/+3
|\
| * Mention rv32- and rv64- configurations in the help messageXavier Leroy2017-07-311-0/+2
| | | | | | | | These are the configurations for the new RISC-V port.
| * Accept Coq version 8.6.1 as supportedXavier Leroy2017-07-311-1/+1
| | | | | | | | 8.6.1 works just fine with the current CompCert.
* | Warning for Skylake/Kabylake systems.Bernhard Schommer2017-07-311-0/+4
|/
* use TMPDIR also for asm-cfi testMichael Schmidt2017-07-271-5/+5
|
* generalize test for compiler optionsMichael Schmidt2017-07-271-15/+22
|
generated by cgit (git 2.34.1) at 2024-07-06 18:03:57 +0000