diff options
| author | Vincent Laporte <vbgl@users.noreply.github.com> | 2019-02-12 19:52:15 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-02-12 19:52:15 +0100 |
| commit | 873c62128ea8aeb2a26384be2be09b9324b9ed9c (patch) | |
| tree | 2694dc9aa9028568557aa84f10cdcc893b53fafe /Makefile | |
| parent | 0b3193b0019373305aec293362956bdb24cbb9a0 (diff) | |
| download | compcert-873c62128ea8aeb2a26384be2be09b9324b9ed9c.tar.gz compcert-873c62128ea8aeb2a26384be2be09b9324b9ed9c.zip | |
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.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 6 |
1 files changed, 1 insertions, 5 deletions
@@ -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) |