aboutsummaryrefslogtreecommitdiffstats
path: root/configure
Commit message (Collapse)AuthorAgeFilesLines
...
* | | | | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-11-131-9/+4
|\| | | | | | | |_|_|_|_|/ |/| | | | | | | | | | | mppa-work-upstream-merge
| * | | | | 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
| | |_|/ / | |/| | |
* | | | | [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-161-6/+34
|\| | | | | |_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: .gitignore backend/Lineartyping.v common/Values.v configure cparser/Machine.ml cparser/Machine.mli driver/Configuration.ml driver/Frontend.ml runtime/Makefile test/c/Makefile test/c/aes.c test/compression/Makefile test/regression/Makefile test/regression/extasm.c test/regression/floats-basics.c test/regression/floats.c Note : test/regression should be checked, didn't test it yet
| * | | 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
| | | |
* | | | Removing Coq 8.7.* in configure (not compatible with "3: {..}" directives)Cyril SIX2019-10-091-2/+2
| |_|/ |/| |
* | | Adding SIMU=k1-cluster -- in configureCyril SIX2019-09-201-0/+1
| |/ |/|
* | Fixing upstream merge buildCyril SIX2019-09-031-1/+1
| |
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-08-281-2/+2
|\ \ | | | | | | | | | mppa-work-upstream-merge
| * | Add support for Coq 8.10Xavier Leroy2019-08-051-2/+2
| |/
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-191-12/+6
|\| | | | | | | mppa-work-upstream-merge
| * 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.
* | Towards supporting the CompCert tests (not finished)Cyril SIX2019-06-141-0/+2
| |
* | Merge branch 'mppa-work' into mppa-abstractbb-devSylvain Boulmé2019-06-081-11/+30
|\ \
| * | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-031-5/+11
| |\| | | | | | | | | | mppa-if-conversion
| | * Coq 8.9.1 supportXavier Leroy2019-05-211-3/+3
| | | | | | | | | | | | It works fine with the current sources.
| | * Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-271-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Main changes to CompCert outside of Flocq are as follows: - Minimal supported version of Coq is now 8.7, due to Flocq requirements. - Most modifications are due to Z2R being dropped in favor of IZR and to the way Flocq now handles NaNs. - CompCert now correctly handles NaNs for the Risc-V architecture (hopefully).
| | * Harden configure against weird Menhir installationsXavier Leroy2019-03-251-2/+8
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As reported in #281, the Menhir packages in Fedora 29 and perhaps in other distributions can cause `menhir --suggest-menhirLib` to fail and return an empty path. This commit detects this situation and aborts configurations. Also, it hardens the generated Makefile against spaces and special characters in the path returned by `menhir --suggest-menhirLib`.
| * | fix variable issueDavid Monniaux2019-05-291-1/+1
| | |
| * | adaptation pour k1c-cosDavid Monniaux2019-05-281-6/+19
| | |
* | | extending bblock_simu_test with rewritingSylvain Boulmé2019-05-261-1/+1
|/ /
* | 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
| |
generated by cgit (git 2.34.1) at 2024-07-06 17:14:14 +0000