aboutsummaryrefslogtreecommitdiffstats
path: root/configure
Commit message (Collapse)AuthorAgeFilesLines
* Remove support for 32-bit CygwinXavier Leroy2022-12-081-9/+0
| | | | | Cygwin 32 bits has reached end of life, and Cygwin >= 3.4 will be 64-bit only. (https://cygwin.com/pipermail/cygwin-announce/2022-November/010777.html)
* configure: add option -sharedir to specify where to put compcert.ini (#460)Xavier Leroy2022-11-141-5/+32
| | | | | | Make sure that it's one of the three locations where the ccomp executable looks for compcert.ini. Closes: #450
* No need to set -std=c99 on the GNU C preprocessor command lineXavier Leroy2022-09-231-12/+12
| | | | The correct -std option is now added by ccomp itself.
* configure: recognize riscv32 and riscv64 for RISC-V targets (#448)Brad Smith2022-08-291-2/+3
|
* Support Coq 8.15.2Xavier Leroy2022-06-251-2/+2
|
* Harden the configure script against \r\n end of linesXavier Leroy2022-06-201-6/+6
| | | | Fixes: #434
* Support Coq 8.15.1Xavier Leroy2022-04-251-2/+2
|
* Make Coq 8.12.0 the minimal version.Guillaume Melquiond2022-04-251-2/+2
| | | | Otherwise, BinarySingleNaN.Bleb_correct cannot be proved.
* Support Coq 8.15.0Xavier Leroy2022-01-311-2/+2
|
* Support Coq 8.14.1Xavier Leroy2021-11-261-2/+2
|
* Explicitly remove __SIZEOF_INT128__ macro definition. (#419)roconnor-blockstream2021-10-161-4/+4
| | | | | | | | CompCert does not support 128-bit integers, but the gcc and clang preprocessors do include support as part of its 'built-in'. A common way of testing for 128-bit integer support is to check to see if `__SIZEOF_INT128__` is defined. Eliminating this macro prevents software from believing that 128-bit integers are supported.
* Add Coq 8.14.0 to the supported versions of CoqXavier Leroy2021-10-031-3/+3
|
* Refactor clightgenXavier Leroy2021-09-221-2/+2
| | | | | | | Split reusable parts of ExportClight.ml off, into ExportBase.ml and ExportCtypes.ml. Rename exportclight/ directory to export/
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
| | | | | | The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate.
* MacOS: add a #define __DARWIN_OS_INLINEXavier Leroy2021-04-271-2/+2
| | | | | Seems necessary for the standard headers of a recent version of XCode. The actual definition in the standard headers is only for GNUC.
* Support Coq 8.13.2Xavier Leroy2021-04-271-2/+2
|
* Bump minimal Coq version to 8.9.0Xavier Leroy2021-04-191-2/+2
| | | | This is required to have List.repeat in the standard library (next commit).
* Coq 8.13.1 is supportedXavier Leroy2021-03-091-2/+2
| | | | Closes: #389
* "macosx" is now called "macos"Xavier Leroy2021-01-181-8/+8
| | | | | The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos".
* macOS: turn #warning offXavier Leroy2021-01-181-2/+2
| | | | | The standard includes print irrelevant warnings using `#warning`. The warnings can be restored by passing `-W#warning` to `ccomp`.
* Coq 8.13.0 is supportedXavier Leroy2021-01-141-3/+3
| | | | However it produces new warnings that should be investigated later.
* configure: simplify the final printing of the configurationXavier Leroy2020-12-281-9/+8
| | | | | Factor out the substitution of `$prefix` for `\$(PREFIX)` using a shell function `expandprefix`.
* configure: add -mandir option (#382)Daniel Dickman2020-12-281-1/+7
| | | | | To control where man pages are installed. The default `/usr/local/share/man` is good for Linux but BSD prefers `/usr/local/man`.
* AArch64: macOS portXavier Leroy2020-12-261-0/+13
| | | | | This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors.
* configure: use `$make` instead of `make`Xavier Leroy2020-12-251-1/+1
| | | | | | To make sure it works if `gmake` is required. Fixes: #381
* configure script revised and simplifiedXavier Leroy2020-12-241-83/+43
| | | | | | | | Start from reasonable defaults before updating them per-target. Print more details in the final configuration summary. Update the "manual" mode.
* configure: support Coq 8.12.2Xavier Leroy2020-12-241-2/+2
|
* Configure the correct archiver to build runtime/libcompcert.aXavier Leroy2020-12-241-1/+7
| | | | | | | | | - Use `${toolprefix}ar` instead of `ar` so as to match the choice of C compiler (as proposed by Michael Soegtrop in PR #380) - Use the Diab archiver `dar` if configured for powerpc-eabi-diab Closes: #380
* Support Coq 8.12.1Xavier Leroy2020-11-141-2/+2
|
* Support Cygwin 64 bitsXavier Leroy2020-10-051-0/+13
| | | | | | - Add support for the Win64 ABI to the x86_64 port - Update vararg support to handle Win64 conventions - Configure support for x86_64-cygwin64
* Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-211-42/+44
| | | | configure flags -use-external-Flocq and -use external-MenhirLib.
* Remove support for x86-32 under macOSXavier Leroy2020-07-291-24/+0
| | | | | | | 32-bit executables cannot be built since XCode 10.0 (sep 2018). 32-bit executables cannot be executed since MacOS 10.15 (oct 2019). Better remove x86-32 support and fail at configuration time instead of at the end of the build.
* Revised detection of menhirLib directory, continued (#365)Xavier Leroy2020-07-151-4/+4
| | | | | | | This is a follow-up to commit 3b1f3dd5, which was wrong in that errors in a shell pipeline were not correctly detected. Fixes: #363
* Bytecode-only build (#243)Xavier Leroy2020-07-071-3/+14
| | | | | | If ocamlopt (the native-code OCaml compiler) is not available, fall back to building with ocamlc (the bytecode OCaml compiler). Fixes: #359
* Revised detection of menhirLib directory (#248)Xavier Leroy2020-07-071-2/+6
| | | | | Use `ocamlfind query menhirLib` in preference to `menhir --suggest-menhirLib`. Fixes: #363
* Preliminary support for Coq 8.12Xavier Leroy2020-06-211-3/+3
| | | | | | | Based on testing with beta-1 release. The deprecation warning about the "omega" tactic is ignored while we decide when to switch to "lia" instead.
* Compatibility with coq 8.11.2Bernhard Schommer2020-06-081-1/+1
| | | | Updated configure script to also allow coq version 8.11.2
* Support for coq 8.11.1.Bernhard Schommer2020-04-201-2/+2
| | | | Update configure script.
* Compatibility with OCaml 4.10 (#214)Xavier Leroy2020-02-061-4/+4
| | | | | | | | debug/DwarfPrinter.mli: unused functor parameter trigger warning 69, replace by non-dependent functor type. Makefile.extr: turn warning 69 (unused functor parameter) off for extracted code configure: accept OCaml versions above 4.09 configure: update messages for unsupported versions of OCaml and Coq
* Revised menhirLib autoconfiguration (#331)Xavier Leroy2020-02-051-3/+3
| | | | | | | | | | | | | | | | | Since Menhir version 20200123, we need to link with menhirLib.cmxa instead of menhirLib.cmx. This commit chooses automatically the file to link with: menhirLib.cmxa if it exists in the menhirLib installation directory, menhirLib.cmx otherwise. To reliably find the installation directory, configure was changed to record the menhirLib directory in Makefile.config, variable MENHIR_DIR, instead of a pre-cooked command-line option MENHIR_INCLUDES. Makefile.extr was adapted accordingly. Fixes: #329 Closes: #330
* Support Coq 8.11.0 (#212)Xavier Leroy2020-02-051-1/+1
| | | | Update configure. Ignore and clean up .vok and .vos files, which Coq 8.11.0 generates.
* Allow Coq 8.10.2.Bernhard Schommer2019-12-031-1/+1
|
* Raise minimal required versions for OCaml and Coq (#203)Bernhard Schommer2019-10-311-9/+4
| | | At least OCaml 4.05 is now required as well as Coq 8.8.
* Add support for Coq 8.10.1Xavier Leroy2019-10-281-2/+2
|
* Fix configure for coq 8.10.0Michael Schmidt2019-10-131-2/+2
|
* AArch64 portXavier Leroy2019-08-081-4/+34
| | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* Add support for Coq 8.10Xavier Leroy2019-08-071-2/+2
|
* Make configure resistant to Windows EOL and paths (#305)MSoegtropIMC2019-07-081-1/+1
| | | | | | | Commit 1df887f breaks compilation on some Windows environments, those where the output of `menhir --suggest-menhirLib` contains `\r\n` end-of-lines or backslashes in paths. The fix is to filter the output. Closes: #304 Changes in configure broke Windows build
* New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-051-11/+5
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | What's new: 1. A rewrite of the Coq interpreter of Menhir automaton, with dependent types removing the need for runtime checks for the well-formedness of the LR stack. This seem to cause some speedup on the parsing time (~10% for lexing + parsing). 2. Thanks to 1., it is now possible to avoid the use of int31 for comparing symbols: Since this is only used for validation, positives are enough. 3. Speedup of Validation: on my machine, the time needed for compiling Parser.v goes from about 2 minutes to about 1 minute. This seem to be related to a performance bug in the completeness validator and to the use of positive instead of int31. 3. Menhir now generates a dedicated inductive type for (semantic-value-carrying) tokens (in addition to the already existing inductive type for (non-semantic-value-carrying) terminals. The end result is that the OCaml support code for the parser no longer contain calls to Obj.magic. The bad side of this change is that the formal specification of the parser is perhaps harder to read. 4. The parser and its library are now free of axioms (I used to use axiom K and proof irrelevance for easing proofs involving dependent types). 5. Use of a dedicated custom negative coinductive type for the input stream of tokens, instead of Coq stdlib's `Stream`. `Stream` is a positive coinductive type, which are now deprecated by Coq. 6. The fuel of the parser is now specified using its logarithm instead of its actual value. This makes it possible to give large fuel values instead of using the `let rec fuel = S fuel` hack. 7. Some refactoring in the lexer, the parser and the Cabs syntax tree. The corresponding changes in Menhir have been released as part of version 20190626. The `MenhirLib` directory is identical to the content of the `src` directory of the corresponding `coq-menhirlib` opam package except that: - In order to try to make CompCert compatible with several Menhir versions without updates, we do not check the version of menhir is compatible with the version of coq-menhirlib. Hence the `Version.v` file is not present in CompCert's copy. - Build-system related files have been removed.
* Coq 8.9.1 supportXavier Leroy2019-05-211-3/+3
| | | | It works fine with the current sources.
generated by cgit (git 2.34.1) at 2024-06-02 20:37:21 +0000