From 647cc8dc9699277cb1e77ae3b07c007186720d59 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 26 Dec 2016 16:55:06 +0100 Subject: 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 --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 1ec78fc2..ceaacb4b 100644 --- a/Makefile +++ b/Makefile @@ -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/) -- cgit