From 873c62128ea8aeb2a26384be2be09b9324b9ed9c Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 12 Feb 2019 19:52:15 +0100 Subject: Make the checker happy (#272) 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. --- Makefile | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 308b75fd..c1b8d982 100644 --- a/Makefile +++ b/Makefile @@ -279,12 +279,8 @@ distclean: check-admitted: $(FILES) @grep -w 'admit\|Admitted\|ADMITTED' $^ || echo "Nothing admitted." -# Problems with coqchk (coq 8.6): -# Integers.Int.Z_mod_modulus_range takes forever to check -# compcert.backend.SelectDivproof.divs_mul_shift_2 takes forever to check - check-proof: $(FILES) - $(COQCHK) -admit compcert.lib.Integers -admit compcert.backend.SelectDivproof compcert.driver.Complements + $(COQCHK) compcert.driver.Complements print-includes: @echo $(COQINCLUDES) -- cgit From 3881d799d23bcc0cbaaa9e6bfa82c5bc3b2030eb Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 12 Feb 2019 20:31:43 +0100 Subject: Ignore and clean file .lia.cache This file is created by Coq when running some tactics --- Makefile | 1 + 1 file changed, 1 insertion(+) (limited to 'Makefile') diff --git a/Makefile b/Makefile index c1b8d982..0247b688 100644 --- a/Makefile +++ b/Makefile @@ -268,6 +268,7 @@ clean: rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr rm -f tools/ndfun tools/modorder tools/*.cm? tools/*.o rm -f $(GENERATED) .depend + rm -f .lia.cache $(MAKE) -f Makefile.extr clean $(MAKE) -C runtime clean $(MAKE) -C test clean -- cgit