aboutsummaryrefslogtreecommitdiffstats
path: root/configure
Commit message (Collapse)AuthorAgeFilesLines
* Remove install path bricolage for kvxv3.9_kvxCyril SIX2021-06-011-2/+0
|
* Add target ELFCyril SIX2021-06-011-2/+3
|
* Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-011-2/+3
|\
| * Increasing required OCaml version (Pervasives <-> Stdlib module renaming)Cyril SIX2021-05-041-2/+2
| |
| * Adding distinction between kvx-cos and kvx-mbr (for trapping loads)Cyril SIX2021-04-131-0/+1
| |
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-011-8/+9
| | | | | | | | cfrontend/C2C.ml
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-102/+86
|\ \ | |/ |/| | | | | | | | | | | | | PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed
| * 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
* | begin implementing selectDavid Monniaux2021-02-021-0/+1
| |
* | fix Makefile / configureDavid Monniaux2021-02-011-0/+6
| |
* | directory postpass_libSylvain Boulmé2021-01-071-3/+3
| |
* | recreate abstractbb/Sylvain Boulmé2021-01-071-2/+2
| |
* | cleaningSylvain Boulmé2021-01-071-1/+1
| |
* | Merge remote-tracking branch 'origin/aarch64-asmblockgenproof' into ↵Léo Gourdin2020-12-201-2/+2
|\ \ | | | | | | | | | aarch64-peephole
| * | intermediatet commit before builtinsLéo Gourdin2020-12-161-1/+1
| | |
| * | Removing the PseudoAsm IRLéo Gourdin2020-12-131-2/+2
| | |
* | | fix extraction of non-aarch64 targetsSylvain Boulmé2020-12-171-0/+1
| | |
* | | Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2020-12-171-75/+80
|\ \ \ | |/ / |/| |
| * | upgrade kvx backend to coq.8.12.2Sylvain Boulmé2020-12-161-1/+1
| | |
| * | Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-041-3/+2
| |\ \ | | | | | | | | | | | | | | | | | | | | Conflicts: Makefile configure
| * \ \ Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-73/+80
| |\ \ \ | | | |/ | | |/|
| | * | 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.
* | | | Ocaml peephole oracle and array datastruct instead of listsLéo Gourdin2020-12-081-1/+1
| | | |
* | | | a first working draft on ldp/stp peepholeLéo Gourdin2020-12-041-1/+1
| | | |
* | | | Merge branch 'kvx-test-prepass' of ↵David Monniaux2020-11-271-8/+6
|\ \ \ \ | | |_|/ | |/| | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into aarch64-prepass+postpass
| * | | fixing the move of the verified prepass scheduler into scheduling/ directorySylvain Boulmé2020-10-171-3/+1
| | | |
| * | | Merge remote-tracking branch 'origin/kvx-test-prepass' into mppa-RTLpathSE-verifCyril SIX2020-10-161-2/+4
| |\ \ \
| | * | | just missing OpWeights for AARCH64David Monniaux2020-09-161-0/+1
| | | | |
| | * | | starting to move common filesDavid Monniaux2020-09-161-2/+3
| | | | |
| * | | | refactoring of RTLpathSE_impl.v (split with _simu_specs)Sylvain Boulmé2020-10-131-1/+1
| |/ / /
| * | | Merge remote-tracking branch 'origin/kvx-work' into ↵David Monniaux2020-07-301-1/+1
| |\| | | | | | | | | | | | | | mppa-RTLpathSE-verif-hash-junk
generated by cgit (git 2.34.1) at 2024-07-04 02:47:16 +0000