Multiline comments in ipkg files.

[stephen-smith]

The Idris 2 documentation says that ipkg files support multiline comments, but when I attempt to use them I get the error: [ fatal ] Failed to parse .ipkg file: (followed by the absolute pathname of the ipkg file).

Minimal working:

package multiline
version = 0.1.0
authors = "Boyd Stephen Smith Jr."
modules = Multiline
sourcedir = "src"

Minimal failure:

package multiline
version = 0.1.0
authors = "Boyd Stephen Smith Jr."
{-
 -}
modules = Multiline
sourcedir = "src"

[stefan-hoeck]

Can vanilla Idris parse multiline comments?

[stephen-smith]

To my surprise: No, at least not version 0.7.0-53f448c0d.

% idris2 --build okasaki-pfds.ipkg
Uncaught error: Error: Can't recognise token.

"okasaki-pfds.ipkg":3:1--3:2
 1 | package okasaki-pfds
 2 | 
 3 | {-
     ^

So, I guess this is more of an Idris2 documentation bug.

[mattpolzin]

Multi line comments are supported and have at least at times worked so this is a compiler bug rather than a documentation bug. Worth fixing I’m guessing at least for idr files if not ipkg files. Of course if we can’t fix it for ipkg files then we absolutely should fix the docs.

[stephen-smith]

Worth fixing I’m guessing at least for idr files if not ipkg files

Multiline commens worth perfectly fine in .idr files:

% idris2 -c Queue.idr
1/1: Building Queue (Queue.idr)
bss@monster % cat Queue.idr
module Queue

{-
- Testing multiline
- -}

%default total
...

This is just about ipkg files, which seem to only handle comments in the lexer, and only using the Parser.Lexer.Common.comment form which is only good for single-line comments (though it does refuse to match multiline comment closing).

I do think adding multiline comment support to ipkg would be nice.

[mattpolzin]

Oh yeah, I misunderstood your comment and misread the example. My bad!

[stephen-smith]

I do think adding multiline comment support to ipkg would be nice.

I tried just moving blockComment and the mutual block above it into .Common from .Source and using it in the rawTokens for .Package, but I got a unification error I couldn't figure out.

But, I think someone a bit more familiar with the codebase should be able to wedge it in without too much problem. Capturing the content of the multiline comment for pretty-printing during debugging might require rewriting blockComment, tho.

[mattpolzin]

@stefan-hoeck this issue is good to get closed if you'd like. Not only was it ultimately an upstream issue but the problem was fixed by https://github.com/idris-lang/Idris2/pull/3386 as well.