From 7a467d78f8740c4bce6d514529b84b89cb4867e7 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 11 Mar 2019 18:05:44 -0400 Subject: [PATCH] work around coq#9744 in Bytedump, test in Makefile thanks @JasonGross --- bedrock2/Makefile | 6 ++++++ bedrock2/src/Bytedump.v | Bin 17150 -> 17227 bytes bedrock2/src/BytedumpTest.golden.txt | 17 ++++++++++++++++ bedrock2/src/BytedumpTest.v | 29 +++++++++++++++++++++++++++ 4 files changed, 52 insertions(+) create mode 100644 bedrock2/src/BytedumpTest.golden.txt create mode 100644 bedrock2/src/BytedumpTest.v diff --git a/bedrock2/Makefile b/bedrock2/Makefile index 377f22040..2c06a9176 100644 --- a/bedrock2/Makefile +++ b/bedrock2/Makefile @@ -19,12 +19,18 @@ _CoqProject: all: Makefile.coq.all $(VS) $(MAKE) -f Makefile.coq.all + $(MAKE) src/BytedumpTest.out COQ_MAKEFILE := $(COQBIN)coq_makefile -f _CoqProject INSTALLDEFAULTROOT = bedrock2 $(COQMF_ARGS) Makefile.coq.all: force _CoqProject $(COQ_MAKEFILE) $(VS) -o Makefile.coq.all +src/BytedumpTest.out: src/BytedumpTest.v src/BytedumpTest.golden.txt + coqc -q $(shell cat _CoqProject | grep -v ^-arg) $< | head --bytes -1 | hexdump -C > src/BytedumpTest.out.tmp + diff -u src/BytedumpTest.golden.txt src/BytedumpTest.out.tmp + mv src/BytedumpTest.out.tmp src/BytedumpTest.out + force: clean:: Makefile.coq.all diff --git a/bedrock2/src/Bytedump.v b/bedrock2/src/Bytedump.v index ea3fa6be25d6d89d3f69e12d3e00cc8e624b1ad5..2fb84d523109cfb8274e2c4a0ecf1ddbaec8fe60 100644 GIT binary patch delta 134 zcmey@%6Phsaf3C}SR<;Tn4$1j>#R^H4C8-LD3VE41nhF~Ec{!B|1x1;8 zC7F5YItqy;3OT7|sW}S9ntBQvS_i%K!un4UD<8Gy%Q>5}g15 diff --git a/bedrock2/src/BytedumpTest.golden.txt b/bedrock2/src/BytedumpTest.golden.txt new file mode 100644 index 000000000..0cb1d6cdf --- /dev/null +++ b/bedrock2/src/BytedumpTest.golden.txt @@ -0,0 +1,17 @@ +00000000 00 01 02 03 04 05 06 07 08 09 0a 0b 0c 0d 0e 0f |................| +00000010 10 11 12 13 14 15 16 17 18 19 1a 1b 1c 1d 1e 1f |................| +00000020 20 21 22 23 24 25 26 27 28 29 2a 2b 2c 2d 2e 2f | !"#$%&'()*+,-./| +00000030 30 31 32 33 34 35 36 37 38 39 3a 3b 3c 3d 3e 3f |0123456789:;<=>?| +00000040 40 41 42 43 44 45 46 47 48 49 4a 4b 4c 4d 4e 4f |@ABCDEFGHIJKLMNO| +00000050 50 51 52 53 54 55 56 57 58 59 5a 5b 5c 5d 5e 5f |PQRSTUVWXYZ[\]^_| +00000060 60 61 62 63 64 65 66 67 68 69 6a 6b 6c 6d 6e 6f |`abcdefghijklmno| +00000070 70 71 72 73 74 75 76 77 78 79 7a 7b 7c 7d 7e 7f |pqrstuvwxyz{|}~.| +00000080 80 81 82 83 84 85 86 87 88 89 8a 8b 8c 8d 8e 8f |................| +00000090 90 91 92 93 94 95 96 97 98 99 9a 9b 9c 9d 9e 9f |................| +000000a0 a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 aa ab ac ad ae af |................| +000000b0 b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 ba bb bc bd be bf |................| +000000c0 c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 ca cb cc cd ce cf |................| +000000d0 d0 d1 d2 d3 d4 d5 d6 d7 d8 d9 da db dc dd de df |................| +000000e0 e0 e1 e2 e3 e4 e5 e6 e7 e8 e9 ea eb ec ed ee ef |................| +000000f0 f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 fa fb fc fd fe ff |................| +00000100 diff --git a/bedrock2/src/BytedumpTest.v b/bedrock2/src/BytedumpTest.v new file mode 100644 index 000000000..0d17b56b8 --- /dev/null +++ b/bedrock2/src/BytedumpTest.v @@ -0,0 +1,29 @@ +Require Import Coq.ZArith.BinInt Coq.Lists.List. Import Z. +Require Import bedrock2.Byte bedrock2.Bytedump. +Local Open Scope bytedump_scope. +Goal False. + let cc := constr:(repeat x40 (256*256)) in + let cc := eval cbv in cc in + idtac cc. +Abort. + +(* expected output: *) +(* +00000000 00 01 02 03 04 05 06 07 08 09 0a 0b 0c 0d 0e 0f |................| +00000010 10 11 12 13 14 15 16 17 18 19 1a 1b 1c 1d 1e 1f |................| +00000020 20 21 22 23 24 25 26 27 28 29 2a 2b 2c 2d 2e 2f | !X#$%&'()*+,-./| (* X means doublequote here *) +00000030 30 31 32 33 34 35 36 37 38 39 3a 3b 3c 3d 3e 3f |0123456789:;<=>?| +00000040 40 41 42 43 44 45 46 47 48 49 4a 4b 4c 4d 4e 4f |@ABCDEFGHIJKLMNO| +00000050 50 51 52 53 54 55 56 57 58 59 5a 5b 5c 5d 5e 5f |PQRSTUVWXYZ[\]^_| +00000060 60 61 62 63 64 65 66 67 68 69 6a 6b 6c 6d 6e 6f |`abcdefghijklmno| +00000070 70 71 72 73 74 75 76 77 78 79 7a 7b 7c 7d 7e 7f |pqrstuvwxyz{|}~.| +00000080 80 81 82 83 84 85 86 87 88 89 8a 8b 8c 8d 8e 8f |................| +00000090 90 91 92 93 94 95 96 97 98 99 9a 9b 9c 9d 9e 9f |................| +000000a0 a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 aa ab ac ad ae af |................| +000000b0 b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 ba bb bc bd be bf |................| +000000c0 c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 ca cb cc cd ce cf |................| +000000d0 d0 d1 d2 d3 d4 d5 d6 d7 d8 d9 da db dc dd de df |................| +000000e0 e0 e1 e2 e3 e4 e5 e6 e7 e8 e9 ea eb ec ed ee ef |................| +000000f0 f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 fa fb fc fd fe ff |................| +00000100 +*)