diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-12-26 16:55:06 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-12-26 16:55:06 +0100 |
| commit | 647cc8dc9699277cb1e77ae3b07c007186720d59 (patch) | |
| tree | a37eba4eb015f8b093793858c8f25589fd816af8 /Makefile | |
| parent | e65eeecf7f34076cbfad6876ec21623ad25e9cf7 (diff) | |
| download | compcert-647cc8dc9699277cb1e77ae3b07c007186720d59.tar.gz compcert-647cc8dc9699277cb1e77ae3b07c007186720d59.zip | |
Replace 'decide equality' in x86/Op.v by custom tactics from lib/BoolEqual.v
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
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -58,7 +58,7 @@ FLOCQ=\ VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ Iteration.v Integers.v Archi.v Fappli_IEEE_extra.v Floats.v \ Parmov.v UnionFind.v Wfsimpl.v \ - Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v + Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v # Parts common to the front-ends and the back-end (in common/) |