aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Collapse)AuthorAgeFilesLines
* Update warning flags used to compile Flocq and MenhirlibXavier Leroy2023-03-101-2/+5
| | | | | | | | We prefer not to change these two "vendored" libraries. Deprecation warnings can only be addressed upstream. So let's silence them. Flocq no longer triggers the `compatibility-notation` warning, so let's not silence it.
* When installing the Coq development, also install coq-native generated filesXavier Leroy2023-02-201-1/+6
| | | | | | | | If the Coq version used supports native compilation, `.coq-native` directories are generated during the build, and they need to be installed along the `.vo` files. Fixes: #476
* Add `Declare Scope` where appropriate (#440)Xavier Leroy2022-09-191-4/+0
| | | | | | And re-enable the `undeclared-scope` warning. `Declare Scope` has been available since Coq 8.12, which is now the minimal Coq version supported.
* Check early that extraction did not run into unimplemented axiomsXavier Leroy2022-07-071-0/+5
| | | | | | | | This has been known to happen, e.g. when using Flocq 4.0. If we don't stop the build at this point, a `ccomp` executable is built that fails every time it is run. Closes: #438
* Update comment about `deprecated-hint-rewrite-without-locality` warningXavier Leroy2022-07-071-4/+0
| | | | Follow-up to 353669f8f
* Re-enable `deprecated-hint-rewrite-without-locality` warningXavier Leroy2022-07-051-2/+1
| | | | No longer triggered since commit df076edfe.
* Upgrade to Flocq 4.0.Guillaume Melquiond2022-04-251-3/+2
|
* Selectively turn some Coq 8.14 warnings offXavier Leroy2021-10-031-1/+11
| | | | | | | | | | | | Warning "deprecated hint rewrite without locality" cannot be addressed: the suggested fix (qualify with Global or Local or [#export]) is not supported by Coq 8.11 to 8.13 ! Warning "deprecated instance without locality" is turned off for generated file cparser/Parser.v only. Menhir needs to be changed so as to generate the `Global` modifier that would silence this warning.
* Add support to clightgen for generating Csyntax AST as .v filesXavier Leroy2021-09-221-3/+11
| | | | | | | | | 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-4/+4
| | | | | | | 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.
* Silence some new warnings of Coq 8.13Xavier Leroy2021-01-211-1/+17
| | | | | | | | Either because the code change that would silence the warning is not desirable, or because it would break compatibility with earlier versions of Coq. Explain the silenced warnings as comments in the Makefile.
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-1/+1
| | | | | | | | | | | Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
* Update Flocq to 3.4.0 (#383)Guillaume Melquiond2020-12-281-0/+1
|
* Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-211-7/+23
| | | | configure flags -use-external-Flocq and -use external-MenhirLib.
* Added missing semicolon.Bernhard Schommer2020-07-151-1/+1
|
* Bytecode-only build, continuedXavier Leroy2020-07-151-0/+9
| | | | | | | If ocamlopt is not available, use ocamlc instead of ocamlopt to build auxiliary tools (tools/modorder, tools/ndfun). This is a follow-up to commit 9af28924.
* Introduce additional "branch" build information.Bernhard Schommer2020-07-081-1/+4
|
* Preliminary support for Coq 8.12Xavier Leroy2020-06-211-1/+1
| | | | | | | 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.
* Install "compcert.config" file along the Coq developmentXavier Leroy2020-04-291-1/+18
| | | | | | | | The file contains various parameters about the target processor and ABI, useful for VST and possibly other users of CompCert as a Coq library. It is in "var=val" syntax so that it can be included directly from a Makefile or a shell script.
* Simplify the generation of driver/Version.mlBernhard Schommer2020-04-271-3/+8
| | | | Don't use sed, just echo the contents of the file.
* 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.
* Coq 8.10 compatibility: (temporarily) silence new warningXavier Leroy2019-08-051-0/+1
| | | | | | | | | | | | | The "undeclared-scope" warning fires when we use a "notation" scope before having declared it. This is a good thing, except that the "Declare Scope" vernacular that declares a scope was introduced in Coq 8.10 and is not available in earlier versions. Hence there is no way to avoid triggering the warning yet remain compatible with pre-8.10 Coq versions. This commit silences the warning. It will have to revisited when Coq 8.10 is the oldest version of Coq we support in CompCert.
* Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-171-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit adds mechanisms to - recognize certain built-in and run-time functions by name and signature; - associate semantics to these functions, as a partial function from list of values to values; - interpret external calls to these functions according to this semantics (pure function from values to values, memory unchanged, no observable events in the trace); - external calls to unknown built-in and run-time functions remain interpreted as generating observable events and possibly changing memory, like before. The description of the built-ins is split into a target-independent part (in common/Builtins0.v) and a target-specific part (in $ARCH/Builtins1.v). Instruction selection uses the new mechanism in order to - recognize some built-in functions and turn them into operations of the target processor. Currently, this is done for __builtin_sel and __builtin_fabs; more to come. - remove the axioms about int64 helper functions from the standard library. More precisely, the behavior of these functions is still axiomatized, but now it is specified using the more general machinery introduced in this commit, rather than ad-hoc axioms in backend/SplitLongproof. The only built-ins currently described are __builtin_fsqrt (for all platforms) and __builtin_fmin / __builtin_fmax (for x86). More built-ins will be added later.
* New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-051-11/+11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Type inference and type checking for CminorXavier Leroy2019-06-061-1/+1
| | | | | | | This module is similar to RTLtyping: it performs type inference and type checking, but on the Cminor intermediate representation rather than the RTL IR. For each function, it returns a mapping from variables to types. Its first use will be if-conversion optimization.
* Prepend $(DESTDIR) to the installation target (#169)Bernhard Schommer2019-05-171-12/+12
| | | | | | | | Following the gnu Makefile Conventions the variable $(DESTDIR) should be prepended to all installation commands. This allows staged installs.
* Rename Fappli_IEEE_extra.v into IEEE754_extra.vXavier Leroy2019-04-261-1/+1
| | | | | To match the new module names from version 3 of Flocq. Plus, it's shorter.
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-1/+1
| | | | | | | | | | The module Integers.Make contained lots of definitions and theorems about Z integers that were independent of the word size. These definitions and theorems are useful outside Integers.Make, but it felt unnatural to fetch them from modules Int or Int64. This commit moves the word-size-independent definitions and theorems to a new module, lib/Zbits.v, and fixes their uses in the code base.
* Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-271-11/+8
| | | | | | | | | | | | 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).
* Ignore and clean file .lia.cacheXavier Leroy2019-02-121-0/+1
| | | | This file is created by Coq when running some tactics
* Make the checker happy (#272)Vincent Laporte2019-02-121-5/+1
| | | Previously, the coqchk type- and proof-checker would take forever on some of CompCert's modules. This commit makes minimal changes to the problematic proofs so that all of CompCert can be checked with coqchk. Tested with Coq versions 8.8.2 and 8.9.0.
* Make generated file cparser/Parser.v read-onlyXavier Leroy2018-08-271-0/+2
| | | | | | | For consistency with other generated .v files, and because it protects against editing the generated file, see Github issue #248. Closes: #248
* Ensure compatibility with Menhir before and after version 20180530Xavier Leroy2018-06-061-1/+1
| | | | 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-2/+2
|
* Use the standalone coq2html tool to generate the HTML documentationXavier Leroy2018-06-011-10/+2
| | | | | coq2html is now a standalone project (https://github.com/xavierleroy/coq2html) packaged as coq-coq2html in OPAM-Coq.
* Install the VERSION file along the .vo filesBenoît Viguier2018-05-311-0/+1
| | | This is useful for the VST project and can be useful for others.
* Install Coq development (.vo files) if requested (#232)Xavier Leroy2018-05-301-1/+10
| | | | | | | | | .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
* Upgrade Flocq to version 2.6.1 from upstream (#71)Xavier Leroy2018-04-251-0/+3
| | | | | | | | | | | | | | | | We were previously at 2.5.2. Quoting the NEWS from upstream: Version 2.6.1: - ensured compatibility from Coq 8.4 to 8.8 Version 2.6.0: - ensured compatibility from Coq 8.4 to 8.7 - removed some hypotheses on some lemmas of Fcore_ulp - added lemmas to Fprop_plus_error - improved examples Also: in preparation for Coq 8.8, silence warning "compatibility-notation" when building Flocq, because this warning is on by default in 8.8, and Flocq triggers it a lot.
* Change Implicit Arguments to Arguments (#225)Jasper Hugunin2018-03-281-3/+0
| | | | | | | Implicit Arguments is deprecated in Coq since 8.6 or so. Some Implicit Arguments remained in Flocq but were recently changed to Arguments. Apply the same change to our local copy of Flocq. As a positive consequence, we no longer need to suppress the deprecation warnings while compiling Flocq.
* Removed no longer needed struct passing.Bernhard Schommer2018-02-261-2/+0
|
* Fix check-proof target of the Makefile after merge of Coq #6277.Pierre-Marie Pédrot2017-12-071-1/+1
| | | | We simply fully qualify the modules. This is backward compatible.
* Makefile: chmod a-w instead of chmod -wXavier Leroy2017-09-111-1/+1
| | | | | The latter, in conjunction with some values of the umask, gives weird messages "new permissions are ... not ...".
* Update the "make check-proof" entry for Coq 8.6Xavier Leroy2017-03-241-3/+2
| | | | `-admit Floats` is no longer needed, but Integers and SelectDivproof still need admitting.
* Turn warning "deprecated-implicit-arguments" off while compiling FlocqXavier Leroy2017-02-131-1/+4
| | | | Perhaps for reasons of backward compatibility with Coq 8.4, Flocq 2.5.2 still uses the "Implicit Arguments foo" idiom, which is deprecated in Coq 8.6.
* Also remove coq aux files.Bernhard Schommer2017-01-241-0/+1
|
* Replace 'decide equality' in x86/Op.v by custom tactics from lib/BoolEqual.vXavier Leroy2016-12-261-1/+1
| | | | | | | | Applied to the 92-constructor 'operation' type, 'decide equality' produces a huge transparent term that causes the VM compiler to generate huge code and exceeed a memory limit of Coq on 32-bit platforms. (The limit is OCaml's, really.) The lib/BoolEqual.v file defines alternative tactics to build decidable equalities where the transparent part of the definition is smaller (O(N^2) instead of O(N^3)). The proof parts are still huge (O(N^3)) but they are opaque. Fixes #151
* Merge pull request #145 from AbsInt/64Xavier Leroy2016-10-271-10/+26
|\ | | | | | | Support for 64-bit target processors + support for x86 in 64-bit mode
| * Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ↵Xavier Leroy2016-10-271-8/+23
| | | | | | | | | | | | | | | | | | | | | | | | -> x86/x86_32/x86_64 Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq. This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86. While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures. Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).
| * Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-2/+3
| | | | | | | | | | | | | | | | | | | | | | - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.
generated by cgit (git 2.34.1) at 2024-05-18 03:53:55 +0000