Idris2 starts ignoring all Frex sources after a certain point

[ohad]

Sorry for submitting a huge example, but perhaps it is the size of the example that is crucial.

Also, this requires the idris2 version from PR #292 , as I'm using record types with implicit parameters in Coproducts.idr. It's possible that it's the PR #292 that causes the bug, of course, but I'm not sure how.

Steps to Reproduce

Download the attached file jabberwocky.zip and cd to its directory.

$ unzip jabberwocky.zip 
Archive:  jabberwocky.zip
 extracting: Carriers.idr            
  inflating: Data/Nat/Leq.idr        
  inflating: PreorderReasoning.idr   
  inflating: VectReasoning.idr       
  inflating: Views.idr               
  inflating: Signatures.idr          
  inflating: Algebras.idr            
  inflating: Presentations.idr       
  inflating: Util.idr                
  inflating: Models.idr              
  inflating: Free.idr                
  inflating: Monoids/Axioms.idr      
  inflating: Monoids.idr             
  inflating: Coproducts.idr          
  inflating: Powers.idr              
  inflating: CMonoids/Notation.idr   
  inflating: CMonoids/Axioms.idr     
  inflating: CMonoids/Nat.idr        
  inflating: CMonoids/Semiring.idr   
  inflating: CMonoids/Coproducts.idr 
$ idris2 -c --no-banner CMonoids/Coproducts.idr

Expected Behavior

Some kind of syntax error on CMonoids/Coproducts.idr, since it contains nonsense starting on line 128:

$ head -n 136 CMonoids/Coproducts.idr | tail -n $((9))
'Twas brillig, and the slithy toves
      Did gyre and gimble in the wabe:
All mimsy were the borogoves,
      And the mome raths outgrabe.

"Beware the Jabberwock, my son!
      The jaws that bite, the claws that catch!
Beware the Jubjub bird, and shun
      The frumious Bandersnatch!"
$

Observed Behavior

Type-checking succeeds (takes about 30 minutes, but that's expected):

1/20: Building Carriers (Carriers.idr)
2/20: Building Data.Nat.Leq (Data/Nat/Leq.idr)
3/20: Building PreorderReasoning (PreorderReasoning.idr)
4/20: Building VectReasoning (VectReasoning.idr)
5/20: Building Views (Views.idr)
6/20: Building Signatures (Signatures.idr)
7/20: Building Algebras (Algebras.idr)
8/20: Building Presentations (Presentations.idr)
9/20: Building Util (Util.idr)
10/20: Building Models (Models.idr)
11/20: Building Free (Free.idr)
12/20: Building Monoids.Axioms (Monoids/Axioms.idr)
13/20: Building Monoids (Monoids.idr)
14/20: Building Coproducts (Coproducts.idr)
15/20: Building Powers (Powers.idr)
16/20: Building CMonoids.Notation (CMonoids/Notation.idr)
17/20: Building CMonoids.Axioms (CMonoids/Axioms.idr)
18/20: Building CMonoids.Nat (CMonoids/Nat.idr)
19/20: Building CMonoids.Semiring (CMonoids/Semiring.idr)
20/20: Building CMonoids.Coproducts (CMonoids/Coproducts.idr)

[ohad]

Oh, bother. It was the {-- ... --} issue again.

Sorry!

[gallais]

Hopefully #280 will allow you to go back to your preferred comment delimiters.

[ohad]

:D

Thanks. I think it's more an issue of getting used to this, rather than having a preference. I'm not sure where I picked it up, either. It looks like {-- ... --} only appears twice in the Idris book.