Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

first tests for (mm0 parser, mmu parser, mm0+mmu proof checker) #79

Open
wants to merge 15 commits into
base: master
Choose a base branch
from
Open

first tests for (mm0 parser, mmu parser, mm0+mmu proof checker) #79

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
2b486d2
first tests for (mm0 parser, mmu parser, mm0+mmu proof checker)
Apr 23, 2021
00b56ce
tweaking test setup
digama0 Apr 23, 2021
a1e58c8
newlines
digama0 Apr 23, 2021
90e6ec2
whitespace tests
Apr 23, 2021
389d9e4
tests for ids
Apr 23, 2021
f4bea2e
tests for math-strings
Apr 23, 2021
9eccd00
int tests
Apr 24, 2021
97d49c5
comment test
Apr 24, 2021
06b15a9
sort pass test
Apr 24, 2021
54f1424
fail test for sort with 2 modifiers
Apr 24, 2021
cfe043e
all bad-sort tests with regards to order of the modifiers
Apr 24, 2021
bccf813
out of order 2 modifiers bad-sort tests
Apr 24, 2021
43015b5
Merge branch 'master' of https://github.com/Lakedaemon/mm0
Apr 25, 2021
d4bb832
git (my lack of mastery of it) messed the deletion
Apr 25, 2021
af6aed7
moved 2 tests to run folder
Apr 25, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions tests/mm0_mmu/fail/bad-math-string1.mm0
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
-- --V one $ too many
delimiter $ $ $;
2 changes: 2 additions & 0 deletions tests/mm0_mmu/fail/bad-math-string2.mm0
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
-- --V one $ too many
delimiter $ $ $ $ $ ;
10 changes: 10 additions & 0 deletions tests/mm0_mmu/pass/math-string.mm0
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
-- math-string ::= '$' [^\$]* '$'
delimiter $ $;
delimiter $ NUL SOH STX ETX EOT ENQ ACK BEL BS HT LF VT FF CR SO SI
DLE DC1 DC2 DC3 DC4 NAK SYN ETB CAN EM SUB ESC FS GS RS US
! " # % & ' ( ) * + , - . /
0 1 2 3 4 5 6 7 8 9 : ; < = > ?
@ A B C D E F G H I J K L M N O
P Q R S T U V W X Y Z [ \ ] ^ _
` a b c d e f g h i j k l m n o
p q r s t u v w x y z { | } ~ DEL $;
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this delimiter list is terrifying. The multi-character delimiters are not necessarily supported on all verifiers (certainly not on any that I have written), so that would put this in the "not necessarily pass" category (I'm thinking of calling this run/ to mean "don't segfault but pass and fail are both okay")

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I might have to modify the spec to only allow printable ascii inside math strings, because low ascii is a vector for display bugs, which could be exploitable to produce misleading theorem statements.

2 changes: 1 addition & 1 deletion tests/mm0_mmu/pass/whitespace2.mm0
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
-- v-- this is a LINE FEED
-- v-- this is a NEWLINE '\n'
sort s
digama0 marked this conversation as resolved.
Show resolved Hide resolved
;
2 changes: 1 addition & 1 deletion tests/mm0_mmu/pass/whitespace2.mmu
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
-- v-- this is a LINE FEED
-- v-- this is a NEWLINE '\n'
(sort s
)