Comments seem to interrupt twelf output somehow

jcreedcmu / twelf-mac

Other

0 stars 1 forks source link

Comments seem to interrupt twelf output somehow #15

Closed jcreedcmu closed 3 months ago

jcreedcmu commented 3 months ago

Steps to Reproduce

Evaluate the signature:
```
a : type.
% comment
b : type.
```
Observe that Twelf replies
```
a : type.
%% OK %%
```

@agoode first found this trying to run classical-s5, which yielded no output at all except for %% OK %%, because it begins, quite naturally for literate twelf, with comments.

Discussion

~The mechanism for how this happens is very unclear.~ See comment below.

jcreedcmu commented 3 months ago

It's not the output, it's the input.

In the case where we see

a : type.
% comment
b : type.

what twelf sees is the string "a : type.\r%comment\rb: type.". Since twelf is from unix-land, it perceives that we have one declaration "a : type.", followed by some whitespace "\r", followed by a single-line comment "%comment\rb: type.".

The fix is to transliterate \r to \n before sending input to twelf.

jcreedcmu commented 3 months ago

Ah, this closes #13 as well.