aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile.extr
Commit message (Collapse)AuthorAgeFilesLines
* Include `+unix` and `+str` for OCaml 5 compatibilityXavier Leroy2023-03-061-1/+3
| | | | | | | In OCaml 5, the Unix and Str libraries are installed in subdirectories of the standard library directory. In OCaml 4, the `-I +str` and `-I +unix` options have no effect.
* Add support to clightgen for generating Csyntax AST as .v filesXavier Leroy2021-09-221-1/+1
| | | | | | | | | As proposed in #404. This is presented as a new option `-clight` to the existing `clightgen` tool. Revise clightgen testing to test the Csyntax output in addition to the Clight output.
* 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/
* Handle the new warnings of OCaml 4.13Xavier Leroy2021-09-131-1/+1
| | | | | | | | | | | Warning 69 "mutable record field is never mutated": 3 occurrences in backend/IRC.ml removed the "mutable" qualifier on these fields Warning 70 "cannot find interface file" many .ml files have no .mli no strong motivation to add the .mli files turned off the warning in Makefile.extr
* 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.
* Do not use -warn-error when building from a release tarballXavier Leroy2020-11-141-2/+9
| | | | | Stopping on warnings is useful for development builds, but unhelpful for released software.
* Bytecode-only build (#243)Xavier Leroy2020-07-071-1/+15
| | | | | | If ocamlopt (the native-code OCaml compiler) is not available, fall back to building with ocamlc (the bytecode OCaml compiler). Fixes: #359
* Compatibility with OCaml 4.10 (#214)Xavier Leroy2020-02-061-2/+2
| | | | | | | | 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-1/+1
| | | | | | | | | | | | | | | | | 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
* New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-051-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Removed CMinor import. Bug 20992Bernhard Schommer2017-02-141-7/+3
|
* Add LINK_OPT and document it.Bernhard Schommer2017-02-011-2/+15
| | | | | | | The new Makefile variable LINK_OPT can be used to specify additional linker flags for different operating systems, like linking with setargv.obj under windows. Bug 20871
* Added simplified reader and printer for gnu @filesBernhard Schommer2016-07-201-1/+2
| | | | | | | | The functions expandargv and writeargv resemble the functions from the libiberity that are used by the gnu tools. Additionaly a new configuration is added in order to determine which kind of response files are supported for calls to other tools. Bug 18308
* Remove code that will is deprecated in ocaml 4.03Bernhard Schommer2016-06-211-3/+1
| | | | | | | | Most of the code can be String.uppercase usages can either be replaced by a more specialized version of coqstring_of_camlstring (which is also slightly more effecient) or by specialized checks that reject wrong code earlier. Bug 19187
* Moved shared frontend code in own file.Bernhard Schommer2016-05-241-1/+1
| | | | | | | Clightgen and CompCert share the code for preprocessing as well as parsing C files. The code as well as command line switches is moved in the new module Frontend. Bug 18768
* Split dependency generation.Bernhard Schommer2016-05-131-1/+2
| | | | | | GNU make under windows seems to have a restriction to 8192 characters for commandline arguments. The dependency generation of compcert is too large. Thus we split it into two steps.
* Compatibility with newer ocaml versions. Bug 18313.Bernhard Schommer2016-03-311-1/+5
|
* Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-151-1/+1
| | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* Upgrade ocaml version needed and enable more warnings.Bernhard Schommer2016-03-101-3/+3
| | | | | | | | | | | Since the menhir version we use requires ocaml>4.02 we can also upgrade the required ocaml version to >4.02 and remove the deprecate String functions. Also we now activate all warnings except for 4,9 und 27 for regular code plus a bunch of warnings for the generated code. 4 and 9 are not really usefull and 27 is deactivated since until the usage string is printed in a way that requires no newline. Bug 18394.
* Added warning for strict-sequences.Bernhard Schommer2016-01-211-1/+1
|
* Removed the last remains of cchecklink.Bernhard Schommer2016-01-211-2/+0
|
* Ignore *.cmt(i) files and allow global COMPFLAGS.Bernhard Schommer2015-12-071-4/+2
| | | | | | | Instead of using = to set the COMPFLAGS use += which allows it to specify custom compiler flags in for example the Makefile.config. Also remove *.cmt(i) files and add them to the .gitignore file. Bug 17742
* Tentative fix for issue #70 (menhirLib recompilation problems)Xavier Leroy2015-11-131-2/+2
| | | | Don't pass $(MENHIR_INCLUDES) to ocamldep.
* Merge remote branch 'upstream/master' into cleanFrançois Pottier2015-10-231-53/+3
|\ | | | | | | | | Conflicts: Makefile.extr
| * Merge branch 'clean' of https://github.com/fpottier/CompCert into fpottier-cleanBernhard Schommer2015-10-201-6/+9
| |\ | | | | | | | | | | | | Conflicts: Makefile.extr
| * | Removal of cchecklink, superseded by AbsInt's Valex tool.Xavier Leroy2015-10-121-53/+3
| | |
* | | Added a few cleanup commands in [make clean].François Pottier2015-10-231-1/+2
| | |
* | | Install the new system for reporting syntax errors.François Pottier2015-10-231-2/+7
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This requires the development version of Menhir, to be released soon. In summary: handcrafted.messages is new. It contains a mapping of erroneous sentences to error messages, together with a lot of comments. Makefile.extr is new. It contains a rule to generate cparser/pre_parser_messages.ml based on this mapping. cparser/ErrorReports.{ml,mli} are new. They construct syntax error messages, based on the compiled mapping. cparser/Lexer.mll is modified. The last two tokens that have been read are stored in a buffer. ErrorReports is called to construct a syntax error message. cparser/GNUmakefile is new. It offers several commands for working on the pre-parser. cparser/deLexer.ml is new. It is a script (it is not linked into CompCert). It translates the symbolic name of a token to an example of this token in concrete C syntax. It is used by [make -C cparser concrete] to produce the .c files in tests/generated/. cparser/tests/generated/Makefile is new. It runs ccomp, clang and gcc on each of the generated C files, so as to allow a comparison of the error messages.
* | | Makefile.extr: [make clean] removes .automaton files.François Pottier2015-10-231-0/+1
| |/ |/|
* | Added [Makefile.menhir], which gives a choice between Menhir's "code" and ↵François Pottier2015-10-161-7/+10
| | | | | | | | | | | | | | | | | | | | "table" back-ends when compiling CompCert. For now, MENHIR_TABLE is set to false, so CompCert is not affected. Setting MENHIR_TABLE to true builds CompCert using Menhir's table back-end. This causes a small but repeatable slowdown on "make test", about 2% (roughly 1 second out of 40). I have tested building ccomp and ccomp.byte. I have tested with an ocamlfind-installed menhir and with a manually-installed menhir.
* | Add -la 1 to Menhir's invocation, to see statistics and warnings.François Pottier2015-10-071-1/+1
| |
* | Pass --no-stdlib and -v to menhir when compiling pre_parser.mly.François Pottier2015-10-071-1/+1
|/ | | | | | | Passing --no-stdlib ensures that there is no dependency on Menhir's standard library. Passing -v, which is equivalent to --explain --dump, requests the generation of pre_parser.automaton, a description of the automaton.
* Erase incomplete file .depend.extr if "make depend" fails.Xavier Leroy2015-08-211-3/+2
|
* Merge branch 'master' into dwarfBernhard Schommer2015-03-101-13/+12
|\
| * Removed unused target cleansource.Bernhard Schommer2015-03-051-4/+0
| |
| * Removed leftover references to recdepend.Xavier Leroy2015-02-281-6/+5
| |
| * Removed the recdepend again and replaced it by a builtin Make function.Bernhard Schommer2015-02-271-8/+6
| |
| * Updated the recdepend tool to avoid printing of ./ at the begining and ↵Bernhard Schommer2015-02-251-2/+4
| | | | | | | | printing duplicated -I flags.
| * Added a small ocamlfile that calls ocamlfind recursivly over a given directory.Bernhard Schommer2015-02-241-5/+7
| |
| * Removed the Unix from the libraries for cchecklink.Bernhard Schommer2015-02-201-2/+3
| |
| * Merge branch 'no-shell' of github.com:AbsInt/CompCert into compcert_windowsBernhard Schommer2015-02-191-2/+3
| |\
| | * Merge branch 'master' into no-shellBernhard Schommer2015-02-191-2/+6
| | |\
| | * | Use Unix.create_process instead of Sys.command (continued).Xavier Leroy2014-12-291-2/+3
| | | |
| * | | Removed the linker flag again.Bernhard Schommer2015-01-201-2/+2
| | |/ | |/|
* | | Merge branch 'master' into dwarfBernhard Schommer2015-01-201-2/+6
|\| |
| * | Replaced 8 spaces by tabs.Bernhard Schommer2015-01-161-1/+1
| | |
| * | Added new target to just remove the cm[iox] files and the build executables.Bernhard Schommer2015-01-161-0/+4
| | |
| * | Added variable to the Makefile to specify additional linker commands and ↵Bernhard Schommer2015-01-151-2/+2
| |/ | | | | | | changed the configure script to deactivated the checklink build if needed.
* / Merge branch 'master' into dwarfBernhard Schommer2015-01-121-1/+1
|/ | | | | Conflicts: powerpc/PrintAsm.ml
* Minor bug fixes in configure and Makefile.extrXavier Leroy2014-12-171-2/+3
|
generated by cgit (git 2.34.1) at 2024-05-18 07:35:29 +0000