[Agda] Multi-line comments in literate Agda files

[Jesper Cockx]

Hi Marko,

I believe the literal Agda mode *only* looks at the parts between the
begin- and end-code markers (in this case ```). This includes begin- and
end-comment markers, so in this case they are ignored. One trick you could
use is to put some text immediately after the first triple backtick, which
will cause Agda to ignore the whole block. E.g.

```ignore
count : ∀ {Γ} → (n : ℕ) → (p : n < length Γ) → Γ ∋ lookup Γ n p
count {_ , _} zero _     =  Z
count {Γ , _} (suc n) (s≤s p)  =  S (count n p)
```

Hope that helps!

-- Jesper

On Fri, Sep 11, 2020 at 8:51 AM Marko Dimjašević <marko at dimjasevic.net>
wrote:

> Dear all,
>
> Is it possible to write multi-line comments in literate Agda files? I have
> a file with a .lagda.md filename extension loaded in the Agda Emacs mode
> (defined in 'agda2-mode.el'). I'm making some changes to the code in it and
> because type-checking takes so much time (when loading a file with C-c C-
> l), I'd like to comment out the part of the file below my changes such that
> I don't waste time on type-checking definitions that are not affecting my
> changes.
>
> I attempted to comment out that part of the file by enclosing it in {- and
> -}, however, that doesn't comment it out. It looks like the first code
> block nullifies the opening multi-line comment delimiter. For example, in
> the following snippet:
>
> {-
> Given the above, we can convert a natural to a corresponding
> de Bruijn index, looking up its type in the context:
> ```
> count : ∀ {Γ} → (n : ℕ) → (p : n < length Γ) → Γ ∋ lookup Γ n p
> count {_ , _} zero _     =  Z
> count {Γ , _} (suc n) (s≤s p)  =  S (count n p)
> ```
> -}
>
>
> the part that start the code block, i.e. ```, ends the comment span and
> start a code block that gets type-checked.
>
> Is this a bug or a feature?
>
> Should I be writing multi-line comments in literate Agda files in some
> other way?
>
>
> --
> Regards,
> Marko Dimjašević <marko at dimjasevic.net>
> https://dimjasevic.net/marko
> Mastodon: https://mamot.fr/@mdimjasevic
> PGP key ID:       056E61A6F3B6C9323049DBF9565EE9641503F0AA
> Learn email self-defense! https://emailselfdefense.fsf.org
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200911/590731df/attachment.html>