aboutsummaryrefslogtreecommitdiffstats
path: root/configure
Commit message (Collapse)AuthorAgeFilesLines
* Support Coq 8.16.0 and 8.16.1 in configure scriptXavier Leroy2023-03-101-2/+2
|
* configure: add -ignore-ocaml-version optionXavier Leroy2023-03-051-8/+11
| | | | | | Also: produce better "unsupported" message for OCaml 5. Fixes: #477
* 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
generated by cgit (git 2.34.1) at 2024-06-02 21:59:10 +0000