Makefile.coq.local: reduce long line warnings in alectryon build

[jdchristensen]

It's not that important, but the alectryon builds spew out long line warnings because of our conventions on not having line breaks in comments, and I think this will get rid of them. Let's see what happens when the CI runs.

[jdchristensen]

No, alectryon didn't recognize the --long-line-threshold argument. It appears in the source code here:

https://github.com/cpitclaudel/alectryon/blob/11e8cdc8395d66858baa7371b6cf8e827ca38f4a/alectryon/cli.py#L840

Do we need to update to a newer alectryon? @JasonGross ?

[jdchristensen]

@Alizter Is it easy to update alectryon? Should we do it? If it's not easy and/or risks breaking things, I'll just close this.

[Alizter]

@jdchristensen I'll see what I can do.

[Alizter]

I had a look and we are using Jason's patches on top of an older version of alectryon in a submodule. The issue that these patches fix is a naming collision with the html files which we appear to be susceptible to. I tried to rebase the patches on a newer version of alectryon but I have no idea what I am doing basically so it didn't work. Our only hope is for @JasonGross to update his fork.

Also FTR the patches are sitting in a PR upstream for alectryon but the discussion seems to have diverged and it didn't end up getting integrated. I haven't been able to understand the full story and what exactly alectryon is missing for us however.

[jdchristensen]

It would be nice if upstream alectryon could be adapted to accommodate our set-up, so we don't need to be stuck with an out-of-date version.

[jdchristensen]

The alectryon PR that @Alizter mentioned is cpitclaudel/alectryon#25

[Alizter]

@jdchristensen Try rebasing this PR now that we've updated alectryon.

[jdchristensen]

It looks like it is working. I only see two long-line warnings so far, for lines that are > 999 characters long. I could increase 999 to 9999, or we could leave those, as they don't clutter the output that much.

[Alizter]

@jdchristensen Let's just make it 99 999.

[jdchristensen]

@JasonGross Now that the long-line warnings are gone, another repeated warning is visible:

/github/workspace/etc/alectryon/alectryon/pygments.py:251: UserWarning: !! Warning: Unexpected token during syntax-highlighting: '₀'
!! Alectryon's lexer isn't perfect: please send us an example.
!! Context:
        (tensor ₀ (a, tensor ₀ (I, b)))%object -->
        (tensor ₀ (tensor ₀

Should we try to get rid of this warning some how?

[Alizter]

It seems the unicode is causing the lexer to choke. Perhaps @cpitclaudel can say more.

[cpitclaudel]

Oh, sorry folks. My Coq notifications filter was too aggressive and I missed this message.

Two things:

• You can use --long-line-threshold=-1 to turn the warning off. I just pushed a commit to document that.

• The other warning comes from the syntax highlighter. I can't wait to get rid of that custom highlighter and replace it with something built into Coq, but until that exists: the problem comes from the fact that ₀ is an "identifier part" in Coq (not a "symmbol" nor an "identifier start"). I couldn't find the exact rules used for symbols in notations, but allowing identifier parts at the beginning of symbols solves the issue, so I've done that.

The fix should be live on Alectryon's master branch. Do you need me to cut a release or do you track master?

[Alizter]

@cpitclaudel We can track master as we use a submodule for alectryon. We currently follow cpitclaudel/alectryon#25 which Jason recently rebased. If you merge that in some form then it will make our lives easier and we can just continue tracking master.

[cpitclaudel]

If you merge that in some form then it will make our lives easier and we can just continue tracking master.

Right, I'm working on this.